Tamarin y demostraciones computacionales
Use Tamarin prover para la reescritura de multiconjuntos y la verificación basada en trazas.
Tamarin y demostraciones computacionales es una lección gratuita de Cryptology Academy en CoddyKit. Esta es la lección 4 de 4. Puedes leer la lección completa abajo gratuitamente — luego la practicas en el navegador con un editor de código integrado y un tutor de IA 24/7. Forma parte de la ruta de aprendizaje de Cryptology Academy, y tu progreso se sincroniza en la web y la app de CoddyKit. El curso de Cryptology Academy incluye 4 lecciones en total.
¿Qué es Tamarin?
Tamarin (ETH Zurich, 2012) es un verificador de protocolos de seguridad basado en la reescritura de multiconjuntos. A diferencia del enfoque de cláusulas de Horn de ProVerif, Tamarin razona sobre trazas de ejecuciones de protocolos mediante un demostrador interactivo.
Tamarin frente a ProVerif
ProVerif: totalmente automatizado, puede indicar "cannot be proved". Tamarin: asistente interactivo de demostración + modo automatizado, admite teorías ecuacionales (XOR, Diffie-Hellman, mapas bilineales). Es más expresivo, pero tiene una curva de aprendizaje más pronunciada.
Reglas de reescritura de multiconjuntos
Tamarin modela los protocolos como reglas de reescritura sobre hechos. Los hechos representan el estado. Una regla [ L ] --[ A ]-> [ R ] consume los hechos del lado izquierdo L, produce los hechos del lado derecho R y registra la acción A en la traza.
Lenguaje de entrada de Tamarin (.spthy)
Un archivo de teoría de Tamarin declara funciones, ecuaciones, reglas y lemas:
/* Diffie-Hellman key exchange */
builtins: diffie-hellman
rule Alice_1:
[ Fr(~a) ] /* fresh random a */
--[ AliceSent($A, $B, 'g'^~a) ]->
[ Alice_St($A, $B, ~a), Out('g'^~a) ]
rule Bob_1:
[ In(ga), Fr(~b) ]
--[ BobReceived($A, $B, ga) ]->
[ Bob_St($A, $B, ~b, ga^~b), Out('g'^~b) ]Especificación de lemas
Los objetivos de seguridad se expresan como lemas sobre trazas:
/* Secrecy: shared secret not known to attacker */
lemma secret_key:
"All A B k #i #j.
AliceKey(A, B, k) @ i &
BobKey(A, B, k) @ j
==> not (Ex #r. K(k) @ r)"
/* Authentication: if Bob has key, Alice sent it */
lemma authentication:
"All A B k #j. BobKey(A, B, k) @ j
==> Ex #i. AliceKey(A, B, k) @ i & i < j"Ejecución de Tamarin
Inicie la GUI interactiva de Tamarin: tamarin-prover interactive my_protocol.spthy. La interfaz del navegador muestra las obligaciones de demostración; usted guía las estrategias automatizadas o aplica pasos manuales en los casos que no terminan.
Solidez computacional
Las demostraciones simbólicas (ProVerif, Tamarin) garantizan la seguridad bajo supuestos de criptografía perfecta. Los teoremas de solidez computacional (Cortier, Backes) permiten elevar las demostraciones simbólicas a seguridad computacional cuando se instancian con primitivas cuya seguridad está demostrada.
F* y HACL*: implementaciones verificadas
F* (Microsoft Research) es un lenguaje de programación orientado a demostraciones. HACL* es una biblioteca criptográfica escrita en F*, con demostraciones verificadas por máquina de su corrección y resistencia a canales laterales. Se utiliza en Firefox NSS y mbedTLS.
EasyCrypt: demostraciones computacionales basadas en juegos
EasyCrypt permite realizar demostraciones de seguridad totalmente computacionales (basadas en juegos) para construcciones criptográficas, no solo para protocolos. La capa de registros de TLS 1.3 y ChaCha20-Poly1305 se han verificado en EasyCrypt.
Impacto práctico
La criptografía verificada formalmente está llegando a producción: NSS (Firefox) utiliza HACL*, AWS usa s2n-tls con aserciones que incluyen demostraciones, y el protocolo Signal se ha verificado en ProVerif y Tamarin. Los métodos formales ya no son únicamente académicos.
Comprobación de conocimientos
¿En qué se diferencia Tamarin de ProVerif al tratar los casos en que falla la automatización?
Resumen de la lección
Tamarin utiliza la reescritura de multiconjuntos y el razonamiento basado en trazas, con una GUI interactiva de demostración. Admite teorías ecuacionales de DH y XOR. Los lemas expresan objetivos de confidencialidad y autenticación. La solidez computacional conecta las demostraciones simbólicas con la seguridad real. HACL* y EasyCrypt amplían la verificación a implementaciones y construcciones.
Preguntas frecuentes
¿La lección «Tamarin y demostraciones computacionales» es gratis?
Sí — el texto completo de «Tamarin y demostraciones computacionales» es gratis para leer aquí en la web. Para practicarla de forma interactiva (editor de código integrado y tutor de IA 24/7) y desbloquear el resto del curso de Cryptology Academy, actualiza a CoddyKit PRO. El curso de Cryptology Academy incluye 4 lecciones en total.
¿Qué aprenderé en «Tamarin y demostraciones computacionales»?
Use Tamarin prover para la reescritura de multiconjuntos y la verificación basada en trazas. Practicas Cryptology Academy con código real que ejecutas directamente en el navegador, y un tutor de IA 24/7 responde tus preguntas mientras trabajas en la lección.
¿Necesito experiencia previa para empezar Cryptology Academy?
No se requiere experiencia previa. Cryptology Academy en CoddyKit está estructurado para principiantes hasta estudiantes avanzados, así que puedes empezar aquí o desde el inicio y avanzar a tu ritmo. Esta es la lección 4 de 4.
¿Cuánto tiempo toma la lección «Tamarin y demostraciones computacionales»?
La mayoría de las lecciones de CoddyKit toman alrededor de 5–10 minutos. Cada una es compacta e interactiva, así que avanzas constantemente y retomas exactamente por donde dejaste en la web y la app.
¿Puedo escribir y ejecutar código en esta lección de Cryptology Academy?
Sí. Cada lección de Cryptology Academy incluye un editor de código integrado, así que escribes y ejecutas código real directamente en tu navegador y obtienes retroalimentación instantánea de IA — sin configuración local necesaria.
Todas las lecciones de este curso
- Por qué las demostraciones informales no bastan
- Modelo de atacante Dolev-Yao y criptografía simbólica
- ProVerif: verificación automatizada de protocolos
- Tamarin y demostraciones computacionales