Computational verification of C protocol implementations by symbolic execution

Mihhail Aizatulin, Andrew D. Gordon, Jan Jürjens

Research output: Chapter in Book/Report/Conference proceedingConference contribution


We verify cryptographic protocols coded in C for correspondence properties with respect to the computational model of cryptography. The first step uses symbolic execution to extract a process calculus model from a C implementation of the protocol. The new contribution is the second step in which we translate the extracted model to a CryptoVerif protocol description, such that successful verification with CryptoVerif implies the security of the original C implementation. We implement our method and apply it to verify several protocols out of reach of previous work in the symbolic model (using ProVerif), either due to the use of XOR and Diffie-Hellman commitments, or due to the lack of an appropriate computational soundness result. We analyse only a single execution path, so our tool is limited to code following a fixed protocol narration. This is the first security analysis of C code to target a verifier for the computational model. We successfully verify over 3000 LOC. One example (about 1000 LOC) is independently written and currently in testing phase for industrial deployment; during its analysis we uncovered a vulnerability now fixed by its author.
Original languageEnglish
Title of host publicationthe ACM Conference on Computer and Communications Security, CCS'12, Raleigh, NC, USA, October 16-18, 2012
Number of pages12
Publication statusPublished - 2012


Dive into the research topics of 'Computational verification of C protocol implementations by symbolic execution'. Together they form a unique fingerprint.

Cite this