The formal verifiation of security properties of a cryptographic protocol is a diffcult, albeit very important task as more and more sensible resources are added to public networks. This paper is focused on model checking; when adopting this approach to the problem, one challenge is to represent the intruder’s knowledge in an effective way. We present an intruder’s knowledge representation strategy that supports the full term language of spi calculus and does not pose arti.- cial restrictions, such as atomicity or limited maximum size, to language elements. In addition, our approach leads to practical implementation because the knowledge representation is incrementally computable and is easily amenable to work with various term representation languages.

A new knowledge representation strategy for cryptographic protocol analysis / CIBRARIO BERTOLOTTI, I; Durante, L; Sisto, Riccardo; Valenzano, A.. - 2619:(2003), pp. 284-298. ((Intervento presentato al convegno 9th International Conference, TACAS 2003 Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2003 tenutosi a Warsaw (PL) nel April 7–11, 2003 [10.1007/3-540-36577-X_21].

A new knowledge representation strategy for cryptographic protocol analysis

SISTO, Riccardo;
2003

Abstract

The formal verifiation of security properties of a cryptographic protocol is a diffcult, albeit very important task as more and more sensible resources are added to public networks. This paper is focused on model checking; when adopting this approach to the problem, one challenge is to represent the intruder’s knowledge in an effective way. We present an intruder’s knowledge representation strategy that supports the full term language of spi calculus and does not pose arti.- cial restrictions, such as atomicity or limited maximum size, to language elements. In addition, our approach leads to practical implementation because the knowledge representation is incrementally computable and is easily amenable to work with various term representation languages.
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/1418139
 Attenzione

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