Verifying cryptographic protocols. Applying the symbolic model to cryptographic APIs for C

In this technical report we describe an approach for verifying cryptographic protocol implementations written in C. We statically prove the correctness of these implementations with the general purpose verifier VeriFast. More concretely we prove: memory safety, the absence of explicit and implicit information leaks, and functional correctness which includes protocol integrity. Our invariant-based approach requires an extension of the symbolic model of cryptography in order to work for protocol implementations in C written against an existing cryptographic API.