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

Verificación de protocolos criptográfico: modelando objetivos

Seguimos con la serie de verificación de protocolos, después de los anteriores:

• Introducción
• Modelado (I)
• Modelado (II)

Ahora nos toca ver cómo completamos nuestros modelos mediante la inclusión de los objetivos del protocolo en ellos. En spi-calculus, para modelar el objetivo de confidencialidad simplemente usamos aserciones ( secrecy assertions en inglés ). Las aserciones son mecanismos que no modifican el flujo del modelo ( no influyen en la semántica operacional ) y simplemente indican que un agente espera que un determinado valor se mantenga secreto. Por ejemplo, podríamos escribir:

Pa = new s; ( secret(s) | out net {s}kab)
Pb= inp net x; decrypt x is {s}kab; secret(s)

De esta forma, se especifica que ambos agentes creen que s es un secreto.

Por otra parte, para especificar opciones de autenticidad nos valemos de aserciones de correspondencia ( correspondence assertions ). Esto simplemente significa que el agente que inicia la autenticación iniciará la aserción de correspondencia con unos parámetros, y el que la acaba la finalizará. Para que todo vaya bien, si existe una finalización debería haber existido antes una inicialización con los mismos parámetros.

Espero que se vea mejor con este ejemplo tomado de los apuntes de Cristian Haacks como una narración informal:

A begins! Send (A, m, B)
A ? S : A, {B, m}kas
S ? B : {A, m}kbs
B ends Send (A, m, B)

Así pues, decimos que es seguro si no existe la posibilidad de que se ejecute el B ends Send(A,m,B) sin que antes e haya ejecutado un A begins! Send(A,m,B). Para acabar, el ! indica que esta aserción se repite indefinidas veces, es decir que un evento begin puede corresponderse con un end repetidas veces. Un ejemplo de esto sería una firma digital, puesto que la firma se puede comprobar muchas veces y siempre será válida. Sin embargo, a veces interesa que solo se de una vez, para garantizar la frescura de la información y evitar replay attacks.

Para ello, se usan eventos inyectivos, que se modelan sin el ! y simplemente un begin puede corresponderse con un end, y nunca más. Para conseguir esto, los protocolos hacen uso de números de secuencia, nonces (number used once), timestamps o similares.

Realmente hay un poco más de chica por aquí detrás con cómo se propagan estos eventos por los canales y demás, pero vamos a dejarlo en que se considera seguro si esto ocurre, ya que en caso contrario significaría que el atacante puede forzar a B a ejecutar un end Send(A,m,B) sin que realmente A haya mandado el mensaje B, lo cual viola la autenticación.

También hay un poco más de teoría respecto a Spi-calculus y procesos seguros respecto a confidencialidad, que especifica qué procesos se pueden denominar así. Intuitivamente, son aquellos procesos en los que no existe ninguna manera de llegar a algo que escriba un secreto en un canal público mediante la semántica operacional de spi-calculus.

Ahora bien, después de este rollo, cómo nos lo montamos con ProVerif para especificar estas propiedades? Pues es bastante sencillo:

Las metas de confidencialidad, simplemente se especifican en la zona de declaraciones con una query tal que así:

query attacker: s.

Donde s es el valor que queremos que sea secreto. El problema es que ProVerif usa macros y los nombres son globales, así que si creamos dos nombres iguales en distintos procesos y hacemos una query, irá para los dos. Además, si usamos variables para las queries, siempre dará que el atacante puede obtenerlo mientras que no es necesariamente cierto.

Para este caso, lo que podemos hacer es generar un flag único y pedir a ProVerif que nos diga si el flag puede obtenerse. Por ejemplo, imaginemos la variable M que ha sido obtenida mediante tras leer de la red. Si queremos que sea secreta, deberíamos hacer algo como:

query attacker: M.
process (*otro_proceso*)|(in(net,M))

Pero entonces ProVerif nos dirá que el atacante puede obtener M, ya que es una variable. Lo que haríamos sería:

query attacker:flagM.
process (*otro_proceso*)|(in(net,M);out(M,flagM);)

En este caso, si el atacante puede conocer M podrá leer del canal M, con lo que podrá obtener el flag y la query fallará. Si no, no podrá obtener el flag y no fallará.

Por otra parte, las aserciones de correspondencia se transforman en eventos, y podemos especificar que un evento debe estar precedido por otro. Un ejemplo sacado de mis códigos de ProVerif sería:

query evinj : endSendToInit(x,y,z) ==> evinj : beginSendToInit(x,y,z).
query evinj : endSendToResp(x,y,z) ==> evinj : beginSendToResp(x,y,z).
query evinj : endAckToInit(x,y,z) ==> evinj : beginAckToInit(x,y,z).
query evinj : endAckToResp(x,y,z) ==> evinj : beginAckToResp(x,y,z).

Aquí estamos diciendo que el evento endSendToInit(x,y,z) debe estar precedido por el evento beginSendToInit(x,y,z), y lo mismo para el resto de eventos. La palabra clave evinj indica que se trata de una correspondencia inyectiva, es decir uno a uno. Si usaramos ev en su lugar se trataría de correspondencia no inyectiva, muchos a uno.

Por último, comentar que es posible especificar en ProVerif la propiedad de no interferencia ( non-interference ), que significa que un atacante no será capaz de distinguir una ejecución del protocolo de otra cambiando los valores de las variables de las que deseamos preservar dicha propiedad.

Dicho más sencillo: que no se puede obtener ninguna información de las variables, ni siquiera si son iguales o distintas de una ejecución a la otra. Por ejemplo, esto no cumpliría dicha propiedad:

P(x) = out(net,{x}k);

Puesto que si {x1}k es igual a {x2}k, entonces x1 es igual a x2. Para resolverlo usaríamos cifrado no determinístico, que simplemente añade una parte aleatoria al mensaje. Algo así:

P(x) = new n; out(net,{(x,n)}k);

De esta forma, como n es aleatorio y presumiblemente diferente cada vez, que el texto cifrado sea igual no implica que el contenido lo sea.

Para especificar esta propiedad, en ProVerif escribiremos por ejemplo:

noninterf x1,x2.

Y luego modelaremos dos procesos en paralelo, uno con x1 y otro con x2. Tras ejecutar ProVerif (que ya veremos cómo se hace en otro post) nos dirá si se puede distinguir entre ellos o no.

Esto es todo de momento... sigo dandoos el coñazo con teoría que puede que no se entienda mucho :oops:, pero en el próximo post explicaré cómo ejecutar ProVerif y un pequeño ejemplo con varias cosas juntas, y después en el siguiente analizaremos el modelo de TLS que puse hace un tiempo.

Si alguien está leyendo esto, que comente si se entiende más o menos o algo 🙂 ( Y quien lo esté leyendo es todo un campeón xD)