Estoy interesado en cómo se puede verificar una implementación de un protocolo de seguridad de forma correcta y completa.
El proyecto AVISPA ( enlace ) se puede usar para verificar el protocolo. Supongo que en teoría, también podría utilizar el lenguaje de modelado AVISPA para generar una implementación.
Debería ser posible tomar una implementación y probar que es una implementación correcta y completa de un protocolo. ¿Hay algún sistema actualmente disponible para hacer esto? ¿Hay alguna investigación activa en esta área?