Automated proofs for Diffie–Hellman–based key exchanges
Contribuinte(s) |
Backes, Michael Zdancewic, Steve |
---|---|
Data(s) |
27/06/2011
|
Resumo |
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). |
Formato |
application/pdf |
Identificador | |
Publicador |
IEEE |
Relação |
http://eprints.qut.edu.au/42550/1/Automated_proofs_for_Diffie-Hellman-base_key_exchanges.pdf Ngo, Long, Boyd, Colin, & Gonzalez Nieto, Juan M. (2011) Automated proofs for Diffie–Hellman–based key exchanges. In Backes, Michael & Zdancewic, Steve (Eds.) 2011 IEEE 24th Computer Security Foundations Symposium (CSF 2011), IEEE, Abbaye des Vaux-de-Cernay, Cernay-la-Ville, pp. 51-65. |
Direitos |
Copyright 2011 IEEE This work has been submitted to the IEEE for possible publication. Copyright may be transferred without notice, after which this version may no longer be accessible |
Fonte |
Faculty of Science and Technology; Information Security Institute |
Palavras-Chave | #080303 Computer System Security #Diffie Hellman key exchange #automated #proof #Hoare logic |
Tipo |
Conference Paper |