  We describe how to verify security properties of C code for cryptographic
protocols by using a general-purpose verifier. We prove security theorems in
the symbolic model of cryptography. Our techniques include: use of ghost state
to attach formal algebraic terms to concrete byte arrays and to detect
collisions when two distinct terms map to the same byte array; decoration of a
crypto API with contracts based on symbolic terms; and expression of the
attacker model in terms of C programs. We rely on the general-purpose verifier
VCC; we guide VCC to prove security simply by writing suitable header files and
annotations in implementation files, rather than by changing VCC itself. We
formalize the symbolic model in Coq in order to justify the addition of axioms
to VCC.
