Verifying cryptographic protocol implementations that use industrial cryptographic APIs

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 veri^Ler 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. Compared to the state of our work in March 2016, as described in TR CW694, we have significantly overhauled our approach, in order to remove a number of unsoundnesses as well as lift a number of limitations.