Automatically Verified Mechanized Proof of One-Encryption Key Exchange

The long version of the paper, available as Cryptology ePrint Archive, Report 2012/173

The CryptoVerif tool

OEKE

The CryptoVerif model of OEKE

The library of cryptographic primitives: Full library The excerpt used for OEKE

The CryptoVerif output, obtained by the command

./cryptoverif OEKE.ocv
(assuming the CryptoVerif model has been saved under the name OEKE.ocv in the CryptoVerif directory).

Signed Diffie-Hellman protocol

The CryptoVerif model of the signed Diffie-Hellman protocol.

The CryptoVerif output, obtained by the command

./cryptoverif signedDH.ocv
(assuming the CryptoVerif model has been saved under the name signedDH.ocv in the CryptoVerif directory).