Quali sono i metodi formali per analizzare il protocollo di autenticazione

4

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?

    
posta MBK 30.09.2015 - 08:08
fonte

0 risposte