DocumentCode
2867590
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
fYear
2011
fDate
27-29 June 2011
Firstpage
51
Lastpage
65
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;
fLanguage
English
Publisher
ieee
Conference_Titel
Computer Security Foundations Symposium (CSF), 2011 IEEE 24th
Conference_Location
Cernay-la-Ville
ISSN
1940-1434
Print_ISBN
978-1-61284-644-6
Type
conf
DOI
10.1109/CSF.2011.11
Filename
5992154
Link To Document