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.
2003
978-3-540-20175-5
File in questo prodotto:
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.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11583/1418141