Title :
Automated Proofs for Diffie-Hellman-Based Key Exchanges
Author :
Ngo, Long ; Boyd, Colin ; Nieto, Juan González
Author_Institution :
Inf. Security Inst., Queensland Univ. Of Technol., Brisbane, QLD, Australia
Abstract :
We present an automated verification method for security of Diffie-Hellman-based key exchange protocols. The method includes a Hoare-style logic and syntactic checking. The method is applied to protocols in a simplified version of the Bellare-Rogaway-Pointcheval model (2000). The security of the protocol in the complete model can be established automatically by a modular proof technique of Kudla and Paterson (2005).
Keywords :
cryptographic protocols; Diffie-Hellman-based key exchange protocol; Hoare-style logic checking; automated verification method; modular proof technique; syntactic checking; Computational modeling; Computer languages; Cryptography; DH-HEMTs; Protocols; Syntactics; Diffie-Hellman; automated; key exchange; modular;
Conference_Titel :
Computer Security Foundations Symposium (CSF), 2011 IEEE 24th
Conference_Location :
Cernay-la-Ville
Print_ISBN :
978-1-61284-644-6
DOI :
10.1109/CSF.2011.11
