Abstract

Consider the problem of verifying security properties of a cryptographic protocol coded in C. We propose an automatic solution that needs neither a pre-existing protocol description nor manual inspection of source code. First, symbolically execute the C program to obtain symbolic expressions for the network message sent by the protocol. Second, apply algebraic rewriting to obtain a process calculus description. Third, run an existing protocol analyzer (ProVerif) to prove security properties or find attacks. We formalize our algorithm and appeal to existing results for ProVerif to establish computational soundness. We analyze only a single execution path, so our results are limited to protocols with no significant branching. The results in this paper provide the first computationally sound verification of weak secrecy and authentication for (single execution paths of) C code.