Modelado y verificación de protocolos de seguridad con el cálculo Pi aplicado y ProVerif

Título original:

Modeling and Verifying Security Protocols with the Applied Pi Calculus and ProVerif

Contenido del libro:

La verificación de protocolos de seguridad ha sido un área de investigación activa desde la década de 1990. Este tema es interesante por varias razones.

Los protocolos de seguridad son omnipresentes: se utilizan en el comercio electrónico, las redes inalámbricas, las tarjetas de crédito y el voto electrónico, entre otros. El diseño de protocolos de seguridad es notoriamente propenso a errores. Además, estos errores pueden tener graves consecuencias.

De ahí que la verificación formal o prueba de protocolos sea especialmente deseable.

Este estudio se centra en la verificación de especificaciones de protocolos en el modelo simbólico. Aunque bastante abstracto, este nivel de verificación es pertinente en la práctica, ya que permite descubrir numerosos ataques.

ProVerif es un verificador automático de protocolos simbólicos. Admite una amplia gama de primitivas criptográficas, definidas por reglas de reescritura o por ecuaciones. Puede demostrar varias propiedades de seguridad: secreto, autenticación y equivalencias de procesos, para un espacio de mensajes ilimitado y un número ilimitado de sesiones.

Toma como entrada una descripción del protocolo a verificar en un dialecto del cálculo pi aplicado, una extensión del cálculo pi con criptografía. Traduce automáticamente esta descripción del protocolo en cláusulas Horn y determina si se cumplen las propiedades de seguridad deseadas mediante la resolución de estas cláusulas. Este estudio presenta una visión general de la investigación sobre ProVerif y es el texto más completo disponible sobre el tema.