Guiding a general-purpose C verifier to prove cryptographic protocols

Abstract
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 alg

This publication has 0 references indexed in Scilit: