Ho progettato un protocollo di autenticazione per le applicazioni di produzione dei consumatori, che aggiunge le funzionalità di Kerberos e Tesla.
Per verificare la forza del protocollo ho preso in considerazione diversi attacchi ben noti come la sessione parallela, la riproduzione, il binding e l'incapsulamento. Questi attacchi richiedono di impersonare un consumatore o un produttore. Il nostro protocollo rileva con successo tali attacchi (in base agli scenari considerati). Tuttavia, non sono fiducioso su tale analisi; Voglio usare un metodo formale per dimostrare la forza del protocollo.
Ho preso in considerazione l'utilizzo di un approccio logico, come i metodi BAN, GNY o CKT5, ma su alcuni forum di discussione ho scoperto che i metodi logici sono considerati deboli per verificare la forza del protocollo. Quali sono i pro e i contro per tali metodi e quali altri metodi formali esistono per analizzare un tale sistema?