Ho ricevuto una recensione per il mio giornale in cui abbiamo proposto i protocolli di autenticazione WOOlim o nspk. Abbiamo dimostrato la forza del nostro protocollo con metodi formali rigorosi utilizzando CSP e analisi della funzione di rango, oltre a dimostrare la forza contro gli attacchi noti con esempi, ma il revisore ci ha chiesto di mostrare la forza con esperimenti o simulazioni.
Non è sufficiente dimostrare la forza con l'analisi formale? E che tipo di strumenti possono essere utilizzati per simulare il protocollo di autenticazione? Ho implementato il mio schema in uno strumento di analisi del protocollo di sicurezza automatizzato, SCYTHER, ma è un tipo di strumento che in effetti dimostra il reclamo del protocollo con analisi formale, non possiamo considerarlo una simulazione.