Recibí una revisión de mi diario en la que propuse el tipo de protocolos de autenticación WOOlim o nspk. Demostramos la fuerza de nuestro protocolo con métodos formales rigurosos que utilizan el análisis de función de rango y CSP, y probamos la fuerza contra ataques conocidos con ejemplos, pero el revisor nos pidió que mostráramos la fuerza con experimentos o simulaciones.
¿No es suficiente probar la fortaleza con un análisis formal? ¿Y qué tipo de herramientas se pueden utilizar para simular el protocolo de autenticación? Implementé mi esquema en una herramienta de análisis de protocolo de seguridad automatizada, SCYTHER, pero es un tipo de herramienta que, de hecho, demuestra las afirmaciones del protocolo con un análisis formal, no podemos considerarlo una simulación.