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

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

En este segundo post vamos a ver lenguajes para el modelado de protocolos criptográficos. Con la ayuda de estos lenguajes, seremos capaces de crear un modelo del protocolo para analizarlo mediante ProVerif.

Empezamos con una manera informal de definir protocolos, seguimos con spi-calculus, y finalmente vemos la sintaxis concreta de ProVerif. En el siguiente post tocará ver cómo modelamos los objetivos de los que hablamos en el post anterior, y en el último veremos paso por paso un modelo concreto.

Narraciones informales

Veamos primero como narrar de forma informal los protocolos criptográficos. En primer lugar, necesitamos una serie de primitivas para definir los mensajes:

• Tuplas: (m1,m2,...,mn)
• Cifrado simétrico: { M }k
• Cifrado asimétrico: {| M |}pk
• Hashes: #( )

Además de esto, necesitamos nonces, que son números de un sólo uso que (en nuestro modelo) son imposibles de adivinar, y claves, que también asumimos inadivinables.

Con esto, podemos por ejemplo modelar el siguiente protocolo:

A->B: (M,A)
B->A: N
A->B: {| #(M,B,N) |}sA

Donde sA es la clave privada de A para realizar firmas criptográficas y N es un nonce que B genera para que la firma de A sea válida solo una vez. En caso de no usar ese nonce, la firma podría haber sido mandada por un atacante ( replay atack ). Imagina este protocolo:

A->B: (M,A)
B->A: Sign
A->B: {| #(M,B) |}sA

En lugar de un nonce, B solo pide la firma de A. En este caso, un atacante podría reenvíar lo mismo más tarde...y por ejemplo B es tu banco y M un mensaje "pagame 1.000.000$" ya la hemos liado 😉

Creo que con esto quedan claras las narraciones informales, que nos definir un protocolo pero dejan muchos detalles implícitos: comprobaciones al recibir los mensajes, número de agentes en el protocolo, quién y cuándo se generan los mensajes (M,N en este caso), etcetera.

Así pues, necesitamos de un formalismo para definir mejor los protocolos de forma que todo quede tan explícito como sea posible: spi-calculus.

Spi-calculus

El lenguaje spi-calculus está definido por una serie de mensajes, procesos que se pueden componer en serie o en paralelo y una semántica operacional que define cómo evolucionan dichos procesos. Por ejemplo, si se tiene un proceso que escribe en un canal dado, y se tiene otro que lee de dicho canal en paralelo en la variable x, entonces la semántica operacional nos dice que en un paso se puede ir de esta construcción a una en la que sustituiremos todos los valores de la variable x detrás de la lectura del canal en el segundo proceso por el valor escrito por el primero.

No voy a explicar aquí todo el spi-calculus, simplemente os dejo este link a un resumen del mismo, y ahora pongo un ejemplo porque el parrafo anterior queda bastante confuso. El siguiente fragmento de código sería el equivalente al protocolo anterior:

Pinit(a,b,sa)= new m; out net (m,a); inp net x; if x=Sign then out net {| #(m,b) |}
Presp(b,a,pa)=inp net x; split x is (m,a); out net Sign; inp net x; decrypt x is {| z |}pa^-1; if z = #(m,b) stop
Pprotocolo = new a;new b;new kpa; new kpb; !Pinit(a,b,enc(kpa)) | !Pinit(b,a,enc(kpb)) | !Presp(b,a,dec(kpa)) | !Presp(a,b,dec(kpb))

De esta forma, tenemos que Pinit es un proceso que genera un mensaje, lo manda a la red, espera a recibir Sign y manda a la red una firma sobre el hash de (m,b). Presp realiza la otra parte del protocolo, y Pprotocolo une todo dando los parámetros adecuados para que pueda haber infinitas sesiones donde ambos agentes a y b puedan funcionar tanto de iniciador como de receptor.

Echando un ojo a la semántica operacional, se puede ver que yendo paso a paso podemos ejecutar el protocolo gracias a spi-calculus. Espero que con este ejemplo y el documento con el resumen de la sintaxis y la semántica se medio entienda, aunque realmente no vamos a usar spi-calculus como tal sino una versión modificada que paso a explicar en otro post ya que se está haciendo demasiado largo y queda un poquito sobre el lenguaje usado por ProVerif.

Sé que este post ha podido quedar demasiado teórico y muy resumido, pero lo interesante está por llegar. En el próximo modelaremos el mismo protocolo mediante ProVerif, pero sin añadir objetivos de seguridad al mismo. Después veremos cómo modelar los objetivos y los añadiremos al modelo, para poder comprobar su seguridad.