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

19Jul/088

Verificación de protocolos criptográfico: modelando objetivos

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

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)

Posted by Eloi Sanfèlix

Comments (8) Trackbacks (0)
  1. Hola telemático!

    Buscando información sobre ProVerif me topé con tu blog.
    Y he de decirte q me he leído todos los posts q pusiste sobre el tema! de hecho me he leído alguno q has puesto después y así me he enterado de que ya eres Ingeniero de Telecomunicación. Enhorabuena!

    Bueno, el caso es que lo que escribiste sobre me ha parecido muy interesante y aunque hay alguna cosilla q no he pillado del todo, lo peor es q me he quedado con la intriga. En el último que escribiste el 19 de julio, decías q explicarías como ejecutar ProVerif y pondrías algún ejemplo…

    Te escribo para preguntarte si todavía sigues con la intención de hacerlo; es más, quiero animarte a q lo hagas. Yo tb soy ingeniera de telecomunicaciones (terminé la carrera hace tiempo) y en este momento estoy haciendo la tesis. Me he bajado el ProVerif para hacer pruebas de verificaciones de protocolos. Lo he probado con los ejemplos que trae, pero al ver la salida he flipado un poco. Sólo alcanzo a entender cuándo se ha detectado algún ataque, pero todo lo demás… Igual con eso me es suficiente, pero si el resto describe cómo es el ataque descubierto, me interesaría entenderlo.

    Como ya estarás trabajando, me imagino q no tendrás mucho tiempo… en fin, q si no vas a poner nada más sobre el tema, podrías indicar por lo menos algunos links de documentación “entendible” q conozcas?

    Muchas gracias por todo 😉

  2. Hola 🙂

    Bueno, primero… gracias por la enhorabuena jeje

    Y luego, pedir disculpas por no seguir con la serie de ProVerif (aunque esto sea solo mio, claro xD). Tengo medio post escrito en los borradores desde Julio, lo que pasa que entre unas cosas y otras lo he ido dejando.

    También porque parece como que no se entiende mucho toda la teoría aburrida que he soltado en estos posts, pero por otra parte porque he estado algo liado y no me apetecía mucho ponerme con ello. A ver si pronto lo hago y sigo explicandolo, que con ejemplos es cuando se ve un poco más el potencial de ProVerif.

    En cuanto a documentación, tengo la de Christian Haacks de la asignatura que dimos en Eindhoven, está en http://cs.ru.nl/~chaack/teaching/2IF02-Spring08/ . Si quieres también te podría mandar al correo mis soluciones en appiled pi calculus para los ejercicios que ibamos haciendo, aunque algunas tienen errores.

    De todas formas, qué entradas le das al ProVerif? En Pi o en cláusulas de Horn? Y cuales son las salidas? Es que la salida es un poco críptica y hay que seguir la traza… a veces no es 100% obvio qué es lo que está pasando xD

  3. Hola!

    Vaya esta ha sido la primera vez que escribía en un blog, y no me esperaba una contestación tan rápida! De hecho no sabía si me llegaría un mail de aviso, o tenía q mirar en la web… parece mentira!

    Bueno, lo primero, a mí me parece que te explicas muy bien. Igual es pq al estar haciendo la tesis he tenido q leer cosas realmente duras… así q algo escrito por alguien con una perspectiva parecida a la mía es muy de agradecer.

    Acabo de mirar un poco por encima el link q me has indicado, y está muy bien! No sé de dónde, pero el assigment 8 ya me lo había bajado, así q ahora podré completarlo con el resto q me faltaban. Los iré mirando poco a poco… A! y tus soluciones me serían de gran ayuda! Muchas veces este tipo de ejercicios colgados en la red no sirven de mucho si no tienes las soluciones, o algo q te oriente de cómo pueden ser.

    En realidad todavía no he empezado a utilizar el ProVerif con el protocolo q quiero verificar; el esfuerzo de ponerlo en pi calculus es muy grande, así q prefiero comprobar primero el potencial del ProVerif, ver que entiendo cómo funciona y entonces ponerme a ello. Por ahora he decidido meterle pi, ya q me parece más fácil y he encontrado artículos q lo utilizan con protocolos parecidos al mío… He hecho pruebas con los ejemplos q vienen en el paquete (en la carpeta examples/piboth), bastante bien explicados, pero lo q no llego a entender son los ataques que encuentra… ni siquiera si realmente los describe… Vamos, que no consigo interpretar la salida. Y si no lo consigo, no me servirá de nada 🙁

    Otra pregunta: en la TU de Munich han desarrollado otro sw, el Viki, que sirve para verificar protocolos tb, pero utilizando UMLsec, una extensión de UML. Has oído hablar sobre él?

  4. Hola otra vez!

    Acabo de explorar en profundidad el link, y he visto que las soluciones están disponibles, así q no hace falta q te tomes el trabajo de enviarme lo de clase. Intentaré arreglármelas con eso. Si no puedo, volveré a pedirte sopitas…

    Muchas gracias por todo!

  5. Hola!

    He estado revisando los ejercicios del curso, y tengo bastantes dudas… Pero empezaré por lo más urgente:

    No llego a entender cómo se modela la presencia de un agente comprometido. Por lo que he visto, se declara primero su nombre como free (normalmente, free spy). ¿Para qué? Si se sabe el nombre del agente q funciona como espía, qué sentido tiene?

    Para modelar si el espía puede conocer un secreto, se crea su flag y se sacan por el canal del secreto ese flag. Pero antes de hacerlo, se comprueba q el agente en cuestión no es el espía en sí (if Aspy). Aquí ya me pierdo…

    Y al modelar el proceso espía, he visto q suele hacer público sus dos pares de claves para. Tampoco lo entiendo…

    Muchas gracias por tu tiempo

  6. Hola de nuevo,

    A ver si me sé explicar 🙄

    El hecho de utilizar un nombre para el agente comprometido, y luego utilizar condicionales en la descripción del protocolo se basa en que así no obtendremos falsos positivos.

    Imagina que tenemos un protocolo de key exchange y se establece una clave de sesión con un atacante. Entonces es obvio que esa clave de sesión no será segura puesto que la hemos establecido con el atacante. Pero eso no significa que el protocolo sea inseguro de por sí, ya que por el acceso del agente comprometido a esa clave (en teoría secreta entre él y otro agente legítimo) no implica que pueda acceder a otras claves compartidas entre agentes legítimos.

    Insertamos los condicionales para evitar ese tipo de problemas, y centrarnos en lo que realmente nos interesa que es saber si un atacante interno podría acceder a las claves compartidas entre otros agentes.

    Por otra parte, el hecho de publicar todos los secretos que conoce el atacante interno, es porque así el motor lógico de ProVerif puede usarlos. De esta forma, ProVerif se comportará como un atacante interno puesto que sabrá una clave privada; a partir de ahí, podrá establecer claves de sesión con agentes válidos y podrá derivar si es posible obtener las claves compartidas entre dos agentes válidos.

    No sé si me he explicado bien o no… de todas formas, si quieres te mando un mail y lo podemos hablar por IM algún día que coincidamos.

    Saludos

  7. Hola de nuevo!

    Creo q entendí tu explicación anterior, gracias!

    Ahora estoy sumergida en el último ejercicio del curso, el del procolo de e-voting, y tengo otra vez dudas con el espía. Creo q las dos primeras preguntas del ejercicio las entiendo; se modela el espía como un posible votante pero no registrado, y se comprueba si puede conocer los votos (a) o por lo menos distinguir q son diferentes (b).

    En la tercera pregunta, la (c), se demuestra que el espía no puede llegar a emitir un voto q vaya a ser contado por Collector. Para ello, se modifica el proceso del Collector haciendo q si se encuentra con un voto de cierto valor (challengeVote) publique el valor de un secreto suyo. Bueno, pues esto es lo q no llego a entender. Dónde se modela que el espía emita el voto con ese valor “challengeVote”? Además, por qué enviaría el espía un voto “challengeVote” si su objetivo es colar un voto válido?

    Tal vez sea mejor q hagamos lo q proponías, mandarme un mail y hablarlo por IM… la verdad es q no le he hecho nunca, así q necesitaré instrucciones. Tienes acceso a mi dirección de e-mail?

  8. To work with pre made resources or not? That is a question that creative people asks themselves from time to time. Even if you’re a talented artist, sometimes the deadlines are just too brief, or that spark of inspiration did not affect yet. Awkward, there are many of solutions available. In the ocean of pre-made graphic and designs that one may down load and use for his needs, one author sticks out. A fast growing Scarab13 Design Resource Website is a template nirvana, packed with custom, exclusive documents (all designed by Scarab13), where literally anyone can find something they require. Via Photoshop tutorials, backgrounds, activities, brushes – to some more advanced posters, catalogues, mock-ups and banners – it’s all here and able to download. Because one of the most popular Envato authors, Scarab13 has mastered the fine art of designing creative data (in all topics/genres), data files that are complex in their technical execution, but very simple in their usage, being geared toward users who may or may have not know about Photoshop; thus are user friendly & modify and tweak in minutes, giving you with some very professional and beautiful designs for Print, Web, Cell, TV, and all other outlets. (also related: downloadsoho. com, scaryposter. com, creativeartmarket. com)

    http://scarab13.com/ps_actions


Leave a comment

No trackbacks yet.