Verifying cryptographic protocols: a symbolic model for cryptographic APIs for C

We propose 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.