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.. - STAMPA. - 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
CIBRARIO BERTOLOTTI I;DURANTE L;SISTO, Riccardo;VALENZANO A.
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 | Dimensione | Formato | |
---|---|---|---|
3-540-36577-X_21.pdf
non disponibili
Tipologia:
2a Post-print versione editoriale / Version of Record
Licenza:
Non Pubblico - Accesso privato/ristretto
Dimensione
754.75 kB
Formato
Adobe PDF
|
754.75 kB | Adobe PDF | Visualizza/Apri Richiedi una copia |
Pubblicazioni consigliate
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
https://hdl.handle.net/11583/1418139