Métodos formales y seguridad en la Red

PorJosé A. Alonso

Hoy publica “El País” el artículo España, blanco de más de cuarenta ciberataques. El artículo es un reportaje sobre “la guerra de los ciberespías” a raíz del ataque a Google. Además cuenta las iniciativas españolas para aumentar la seguridad.

Desde sus inicios los métodos formales se han aplicado a aumentar la seguridad de los sistemas críticos y, más generalmente, a la ingeniería de la seguridad. Dado el uso de la Red, sus programas y servicios se están convirtiendo en sistemas críticos y, por tanto, en campo de aplicación de los métodos formales. Muestra del interés de los sistemas de Red para los métodos formales son la realización de tesis como las siguientes

  1. Axiomatic Semantics Verification of a Secure Web Server (P.E. Black, 1998)
  2. The Analysis of Cryptographic APIs Using The Theorem Prover Otter (P. Youn, 2004).
  3. Automated Analysis of Security APIs (A.H. Lin, 2005).
  4. Using a PVS Embedding of CSP to Verify Authentication Protocols (B. Dutertre y S. Schneider, 1997).
  5. Proving Properties of Security Protocols by Induction (L.C. Paulson, 1997).
  6. AnZenMail: A secure and certified e-mail system (E. Shibayama y als. 2002).
  7. Formalization and Verification of a Mail Server in Coq (R. Affeldt y N. Kobayashi, 2003).
  8. Robbing the bank with a theorem prover (C.P. Youn y als. 2005).
  9. A Tool for Managing Security Policies in Organisations (A.V. Álvarez, R. Monroy, J. Vázquez, 2006).
  10. Defending the Bank with a Proof Assistant (J. Courant y J.F. Monin, 2006).
  11. Modeling partial attacks with Alloy (A. Lin, M. Bond y J. Clulow, 2007).
  12. Formal Analysis of PKCS# 11 (S. Delaune, S. Kremer y G. Steel, 2008).
  13. Formal Support to Security Protocol Development: A Survey (J.C. López Pimentel y R. Monroy, 2008).

Además, hay series de congresos específicos como

  1. ARSPA-WITS’10 (Joint Workshop on Automated Reasoning for Security Protocol Analysis and Issues in the Theory of Security) que se celebrará en Paphos (Chipre) el 27 de Marzo.
  2. WWV2010 (6th International Workshop on Automated Specification and Verification of Web Systems) que se celebrará en Viena el 30 de Julio y se pueden mandar artículos hasta el 12 de Abril.