Automated proofs for Diffie–Hellman–based key exchanges


Autoria(s): Ngo, Long; Boyd, Colin; Gonzalez Nieto, Juan M.
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

http://eprints.qut.edu.au/42550/

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