We methodically expand protocol narrations into terms of a process algebra in order to specify some of the checks that need to be made in a protocol. We then apply static analysis technology to develop an automatic validation procedure for protocols. Finally, we demonstrate that these techniques suffice to identify several authentication flaws in symmetric and asymmetric key protocols such as Needham–Schroeder symmetric key, Otway–Rees, Yahalom, Andrew Secure RPC, Needham–Schroeder asymmetric key, and Beller–Chang–Yacobi MSR.

Static Validation of Security Protocols

BODEI, CHIARA;DEGANO, PIERPAOLO;
2005-01-01

Abstract

We methodically expand protocol narrations into terms of a process algebra in order to specify some of the checks that need to be made in a protocol. We then apply static analysis technology to develop an automatic validation procedure for protocols. Finally, we demonstrate that these techniques suffice to identify several authentication flaws in symmetric and asymmetric key protocols such as Needham–Schroeder symmetric key, Otway–Rees, Yahalom, Andrew Secure RPC, Needham–Schroeder asymmetric key, and Beller–Chang–Yacobi MSR.
2005
Bodei, Chiara; Buchholtz, M.; Degano, Pierpaolo; Nielson, F.; RIIS NIELSON, H.
File in questo prodotto:
File Dimensione Formato  
JCS'05.pdf

non disponibili

Tipologia: Versione finale editoriale
Licenza: Importato da Ugov Ricerca - Accesso privato/ristretto
Dimensione 309.7 kB
Formato Adobe PDF
309.7 kB Adobe PDF   Visualizza/Apri   Richiedi una copia

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11568/181132
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 97
  • ???jsp.display-item.citation.isi??? ND
social impact