This paper explores the use of Spin for the verification of cryptographic protocol security properties. A general method is proposed to build a Promela model of the protocol and of the intruder capabilities. The method is illustrated showing the modeling of a classical case study, i.e. the Needham-Schroeder Public Key Authentication Protocol. Using the model so built, Spin can find a known attack on the protocol, and it correctly validates the fixed version of the protocol.

Using SPIN to Verify Security Properties of Cryptographic Protocols / Maggi, Paolo; Sisto, Riccardo. - STAMPA. - 2318:(2002), pp. 187-204. (Intervento presentato al convegno 9th International SPIN Workshop tenutosi a Grenoble (FR) nel April 11–13, 2002) [10.1007/3-540-46017-9_14].

Using SPIN to Verify Security Properties of Cryptographic Protocols

MAGGI, PAOLO;SISTO, Riccardo
2002

Abstract

This paper explores the use of Spin for the verification of cryptographic protocol security properties. A general method is proposed to build a Promela model of the protocol and of the intruder capabilities. The method is illustrated showing the modeling of a classical case study, i.e. the Needham-Schroeder Public Key Authentication Protocol. Using the model so built, Spin can find a known attack on the protocol, and it correctly validates the fixed version of the protocol.
File in questo prodotto:
Non ci sono file associati a questo prodotto.
Pubblicazioni consigliate

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/11583/1418128
 Attenzione

Attenzione! I dati visualizzati non sono stati sottoposti a validazione da parte dell'ateneo