CryptoVerif: a Computationally-Sound Security Protocol Verifier (Initial Version with Communications on Channels)

Bruno Blanchet

This document presents the security protocol verifier CryptoVerif.CryptoVerif does not rely on the symbolic, Dolev-Yao model, but on the computational model. It can verify secrecy,…