Verifying authentication properties of C security protocol code using general verifiers

Directly verifying security protocol code could help prevent major security flaws in communication sys-tems. C is usually used when implementing security software (e.g. OpenSSL, cryptlib, PolarSSL...) because it provides control over side-channels, performance, and portability all at once, along with being easy to call from a variety of other languages. But those strengths also make it hard to reason about