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

Verificación de protocolos criptográficos: Modelado (II)

Continuamos en este post con las técnicas de modelado de protocolos criptográficos. Ahora sí vamos a adentrarnos en el mundo de ProVerif viendo la sintaxis que usa para definir los protocolos.

Un archivo fuente de ProVerif puede estar en spi-calculus o mediante cláusulas de Horn. Nosotros solo vamos a ver spi-calculus entre otras cosas porque yo de cláusulas de Horn ni idea 🙄 . Los archivos fuente .pi tienen varias partes que vamos a ver por separado:

Declaración de nombres

Generalmente al inicio del código se declaran los nombres que se van a usar en el modelo. Esto suele incluir los canales de comunicación públicos, identificadores de usuario, tags para los mensajes, etc.

La sintaxis es sencilla: [private] free nombre. declararía nombre, donde el atributo opcional private indica que solo se puede usar si está explícitamente escrito en el modelo. Es decir, el atacante no tendrá acceso a dicho nombre si anteponemos la palabra private en su declaración.

Constructores y reglas de reducción

Estos son un mecanismo genérico para modelar operaciones como cifrado/descifrado, hashes, derivación de claves a partir del identificador de agente y otros. Básicamente, definimos un constructor como una función de varias variables, y una regla de reducción para poder deshacer lo que hizo el constructor.

La sintaxis es como sigue:

fun constructor/n.
reduc destruct(construct(...),...) = ... .

Con un ejemplo queda claro enseguida. Lo siguiente sería para definir cifrado/descifrado de forma simétrica:

fun encrypt/2
reduc decrypt(encrypt(x,y),y) = x.

Como se puede ver, definimos un constructor con 2 parámetros, y definimos un destructor de forma que si aplicamos decrypt(c,y) donde c ha sido construido como encrypt(x,y), entonces devuelve x. Es decir, y en este caso sería la clave, y x el mensaje a cifrar.

Para un hash, simplemente definiríamos un constructor con 1 único mensaje y sin definir un destructor. De esta forma tenemos una función no invertible perfecta y sin colisiones.

Macros de procesos

Se pueden definir macros de procesos para hacer el código más legible. La sintaxis es:

let proceso = <codigo_del_proceso>.

De esta forma, podemos definir los distintos roles del protocolo en macros separadas y luego juntarlas en el proceso principal.

Proceso principal

Finalmente, el proceso principal se define de la siguiente forma:

process
...

Donde en ... podemos referirnos a los procesos creados mediante macros por su nombre, y ProVerif los sustituirá directamente ahí, de forma textual. No se debe pensar en ellos en forma de funciones, sino simplemente que se reemplazará cualquier aparición de su nombre por el contenido definido en la macro.

Consultas

Además, ProVerif permite especificar consultas, que normalmente ponemos después de las declaraciones de nombres. Esto nos permite verificar si se cumplen los objetivos del protocolo, pero lo veremos en otro post cuando veamos cómo modelar los objetivos.

Diferencias con spi-calculus

Existen algunas diferencias con spi-calculus en la sintaxis, por ejemplo en la forma de escribir/leer a/de un canal de comunicación, la forma de dividir tuplas y algunas cosillas más. Lo mejor es que veamos un ejemplo del protocolo que pusimos en el post anterior para aclarar todo.

Ejemplo

Veamos cómo modelar en ProVerif el protocolo simple del post anterior. La narración informal del protocolo era tal que así:

A->B: (M,A)
B->A: N
A->B: {| #(M,B,N) |}sA
En primer lugar, generaremos los nombres de usuario, el canal de comunicación y los constructores:

free net, A,B,Sign.
fun hash/1.
fun pencrypt(x,enc(y)).
reduc pdecrypt(pencrypt(x,enc(y)),dec(y)).

Como se puede adivinar, pencrypt/pdecrypt definen la criptografía de clave pública que usaremos, donde enc() y dec() identifican la parte de cifrado y la parte de descifrado de un par de claves.

Seguidamente, veremos el proceso A y B:

let procA = new m;out(net,(m,A));in(net,n);out(net,pencrypt((m,n,B),enc(kpa) ).
let procB = in(net,(m,=A));new n;out(net,n);in(net,signed); let (=m,=n,=B) = pdecrypt(signed,dec(kpa)) in 0.

En este caso, he asumido que kpa es el par de claves de A y lo he usado directamente en los procesos, aunque aun no lo hemos generado. Como se puede ver, es mucho menos engorroso que spi-calculus directamente, puesto que permite especificar coincidencias en los mensajes leídos del canal, leer directamente varios valores sin tener que hacer primero el inp y luego el split, etcétera.

Finalmente, nos falta definir el proceso que los junte:

process
new kpa; ( procA | procB )

Con esto tendríamos modelado el protocolo, aunque no habría ningún objetivo especificado y realmente ProVerif no hará nada.

En los próximos posts veremos cómo modelar los objetivos y cómo leer la salida de ProVerif, que es capaz incluso de dar ataques en algunas ocasiones.