In security protocols, message exchange between the intruder and honest participants induces a form of state explosion which makes protocol models infinite.We propose a general method for automatic analysis of security protocols based on the notion of frame, essentially a rewrite system plus a set of distinguished terms called messages. Frames are intended to model generic crypto-systems. Based on frames, we introduce a process language akin to Abadi and Fournet’s applied pi. For this language, we define a symbolic operational semantics that relies on unification and provides finite and effective protocol models. Next, we give a method to carry out trace analysis directly on the symbolic model. We spell out a regularity condition on the underlying frame, which guarantees completeness of our method for the considered class of properties, including secrecy and various forms of authentication. We show how to instantiate our method to some of the most common crypto-systems, including shared- and public-key encryption, hashing and Diffie–Hellman key exchange.

A method for symbolic analysis of security protocols / M. BOREALE; MARIA GRAZIA BUSCEMI. - In: THEORETICAL COMPUTER SCIENCE. - ISSN 0304-3975. - STAMPA. - 338(1-3):(2005), pp. 393-425. [10.1016/j.tcs.2005.03.044]

A method for symbolic analysis of security protocols

BOREALE, MICHELE;
2005

Abstract

In security protocols, message exchange between the intruder and honest participants induces a form of state explosion which makes protocol models infinite.We propose a general method for automatic analysis of security protocols based on the notion of frame, essentially a rewrite system plus a set of distinguished terms called messages. Frames are intended to model generic crypto-systems. Based on frames, we introduce a process language akin to Abadi and Fournet’s applied pi. For this language, we define a symbolic operational semantics that relies on unification and provides finite and effective protocol models. Next, we give a method to carry out trace analysis directly on the symbolic model. We spell out a regularity condition on the underlying frame, which guarantees completeness of our method for the considered class of properties, including secrecy and various forms of authentication. We show how to instantiate our method to some of the most common crypto-systems, including shared- and public-key encryption, hashing and Diffie–Hellman key exchange.
2005
338(1-3)
393
425
M. BOREALE; MARIA GRAZIA BUSCEMI
File in questo prodotto:
File Dimensione Formato  
TCS05.pdf

Accesso chiuso

Tipologia: Versione finale referata (Postprint, Accepted manuscript)
Licenza: Tutti i diritti riservati
Dimensione 421.3 kB
Formato Adobe PDF
421.3 kB Adobe PDF   Richiedi una copia

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

Utilizza questo identificatore per citare o creare un link a questa risorsa: https://hdl.handle.net/2158/202109
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 11
  • ???jsp.display-item.citation.isi??? 5
social impact