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

The following files may correspond to an older version of CryptoVerif; up-to-date files are included in the CryptoVerif distribution: files examples/obasic/OEKE.ocv and examples/basic/signedDH.pcv.

For CryptoVerif version 1.14 (CSF'12 and ePrint 2012/173v1)

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).

For CryptoVerif version 2.06 (ePrint 2012/173v2)

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).