TLS Handshake protocol en ProVerif
Como dije cuando comenté el protocolo de establecimiento de sesión de TLS, en la asignatura Verification of security protocols nos mandaron modelar y analizar la seguridad del mismo mediante la herramienta automatizada ProVerif.
Esta semana nos han devuelto las soluciones y como está bastante completa, con la única pega de que modelamos una única continuación de cada sesión en lugar de (potencialmente) infinitas, la he subido para quien le pueda interesar. Modificar eso es sencillísimo y solo es añadir un signo de exclamación (replicación infinita del proceso) delante del comando que mete el identificador de sesión en un canal privado a modo de base de datos tanto en el cliente como en el servidor.
Es posible que más adelante escriba una serie de posts sobre cómo funciona ProVerif, o suba un documento que probablemente me haga para mi propio uso antes del examen de esta asignatura, a modo resumen de todo lo dado.
El modelo, aquí. Lo hice conjuntamente con un compañero, pero ha dado permiso para publicarlo en la web del profesor con nuestros nombres y aquí no creo que tenga ningún problema 🙂
La sintaxis es algo compleja si no se conoce, si estáis interesados podéis consultar la web de la asignatura, donde además hay otras dos soluciones; otra opción es esperar a que ponga algún ejemplo explicado más adelante.
Si alguien está interesado que lo diga en los comentarios y así lo tendré presente :P.
June 11th, 2008 - 19:48
¡A mí me mola! 😉
June 11th, 2008 - 20:40
Recibido 😉
June 12th, 2008 - 15:04
El link del modelo no está bien. Me parece interesante! 🙂
June 13th, 2008 - 00:55
Uhm, sorry, se me fue la olla… Era .vosp y no .pi como acostumbramos a guardarlo. Es así xq el profesor los renombra y yo mantuve la misma extensión que él usa.
Ahora ya debería ir…
PD: Partyyyy! Me voy a sobar que ya es hora…