Diseñé un protocolo de autenticación para aplicaciones productoras para el consumidor, que prohíbe las características de Kerberos y Tesla.
Para comprobar la fuerza del protocolo, consideré diferentes ataques bien conocidos como sesión paralela, reproducción, vinculación y encapsulación. Estos ataques requieren hacerse pasar por un Consumidor o Productor. Nuestro protocolo detecta con éxito dichos ataques (según los escenarios considerados). Sin embargo, no confío en tal análisis; Quiero usar un método formal para probar la fuerza del protocolo.
Consideré el uso de un enfoque lógico, como los métodos BAN, GNY o CKT5, pero en algunos foros de discusión encontré que los métodos lógicos se consideran débiles para verificar la fuerza del protocolo. ¿Cuáles son los pros y los contras de tales métodos y qué otros métodos formales existen para analizar dicho sistema?