Many formal techniques for the verification of cryptographic protocols rely on the abstract definition of cryptographic primitives, such as shared, private, and public key encryption. This approach prevents the analysis of those protocols that explicitly use commutative and associative algebraic operators to build their messages such as, for example, the Diffie-Hellman key-exchange protocol. This paper investigates the possibility of handling operators which exhibit special properties by considering a stand-alone extension to the way most known popular techniques handle messages exchanged during the protocol sessions. Such an extension makes the new operators tractable by automatic model checking techniques. The properties examined in this paper are commutativity and associativity.
Introducing Commutative and Associative Operators in Cryptographic Protocol Analysis / CIBRARIO BERTOLOTTI, I; Durante, L; Sisto, Riccardo; Valenzano, A.. - STAMPA. - 2767:(2003), pp. 224-239. (Intervento presentato al convegno 23rd IFIP WG 6.1 International Conference on Formal Techniques for Networked and Distributed Systems (FORTE 2003) tenutosi a Berlin (DE) nel September 29 – October 2 2003) [10.1007/978-3-540-39979-7_15].
Introducing Commutative and Associative Operators in Cryptographic Protocol Analysis
CIBRARIO BERTOLOTTI I;DURANTE L;SISTO, Riccardo;VALENZANO A.
2003
Abstract
Many formal techniques for the verification of cryptographic protocols rely on the abstract definition of cryptographic primitives, such as shared, private, and public key encryption. This approach prevents the analysis of those protocols that explicitly use commutative and associative algebraic operators to build their messages such as, for example, the Diffie-Hellman key-exchange protocol. This paper investigates the possibility of handling operators which exhibit special properties by considering a stand-alone extension to the way most known popular techniques handle messages exchanged during the protocol sessions. Such an extension makes the new operators tractable by automatic model checking techniques. The properties examined in this paper are commutativity and associativity.File | Dimensione | Formato | |
---|---|---|---|
978-3-540-39979-7_15.pdf
non disponibili
Tipologia:
2a Post-print versione editoriale / Version of Record
Licenza:
Non Pubblico - Accesso privato/ristretto
Dimensione
227.83 kB
Formato
Adobe PDF
|
227.83 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/1418141