Limited Entropy Dot Com Not so random thoughts on security featured by Eloi Sanfèlix

Verificación de protocolos criptográficos: Introducción

Como ya debéis saber todos los que me soleis leer, una de las asignaturas que he cursado este cuatrimestre en la TU Eindhoven se llama Verification of security protocols. Cuando posteé el modelo del protocolo de establecimiento de TLS, que era el trabajo con más peso de la asignatura (sobre un 20%), voy a intentar explicar un poco cómo verificar las propiedades de los protocolos criptográficos.

En este primer post introduciremos las principales propiedades de los protocolos y el modelo que usamos. En el próximo post veremos rápidamente cómo definir protocolos mediante narraciones informales, la sintaxis del lenguaje spi-calculus para modelado de protocolos criptográficos, y la generalización utilizada en ProVerif. Después de esto, vendrá un post sobre cómo modelar las propiedades básicas en spi y ordenar consultas en ProVerif. Finalmente, despiezaremos en un último post una parte del modelo de TLS, sin implementar ningún mensaje opcional ni
resumen de sesiones.

Objetivos de los protocolos criptográficos

La siguiente lista muestra unos cuantos objetivos básicos en sistemas de seguridad:

• Confidencialidad: Este objetivo se traduce en que un atacante no pueda obtener información sobre ciertos datos del protocolo. Existen dos nociones, la estandar que simplemente implica que no se puede obtener el contenido de los mensajes, y otra más fuerte ( non-interference ) que implica que no se puede deducir nada sobre los mensajes, ni siquiera si dos mensajes mandados tienen el mismo contenido.

• Autenticación: Trata de asegurar que el origen del mensaje es realmente quien dice ser ( autenticación de origen). También existe autenticación de usuario, verificando que un usuario es quien dice ser.

• Integridad: Asegura que los datos no han sido modificado

• No repudio: Asegura que el origen de los datos no pueda negar que los haya enviado ( no repudio de origen) o el destino no pueda negar que los haya recibido ( no repudio de destino ).

Existen otras metas, pero estas dan una idea del tipo de objetivos que puede tener un protocolo de seguridad. Por supuesto cada protocolo está pensado para una situación concreta y puede que tenga algunos de estos objetivos o no.

Modelo black box ( Dolev-Yao )

Para poder verificar las propiedades de un protocolo formalmente, necesitamos modelar dicho protocolo de alguna forma. En nuestro caso usaremos el modelo Dolev-Yao. Este modelo asume que la criptografía es perfecta y que el atacante puede interceptar, modificar o eliminar cualquier mensaje transmitido. Es decir, el atacante controla completamente el canal de comunicación.

La criptografía idealizada que asume este modelo tiene como consecuencia que sin la clave no se puede obtener ninguna información al respecto del contenido, ni tampoco modificarlo. Por tanto la integridad de los mensajes está asegurada... aunque no su origen. Además, las claves son imposibles de adivinar o extraer del texto cifrado y los números aleatorios y los hashes son perfectos.

Por tanto, mediante este modelo solo podremos encontrar fallos independientes de la criptografía. Fallos del protocolo en sí, en la lógica o en la interpretación de mensajes cifrados con la misma clave pero distintos formatos, etc

De momento lo dejamos aquí, el próximo post como he dicho al principio, narraciones informales, spi-calculus y spi-calculus genérico de ProVerif.