Modular verification of security protocol code by typing

We propose a method for verifying the security of protocol implementations. Our method is based on declaring and enforcing invariants on the usage of cryptography. To this end, we develop cryptographic libraries that embed a logic model of their cryptographic structures, and specify pre- and post-conditions on their functions so as to maintain their invariants. We present a theory to justify the soundness of modular code verification via our method. We implement the method for protocols coded in F# and verified using F7, our SMT-based typechecker for refinement types, that is, types including formulas to record invariants. As illustrated by a series of programming examples, our method can flexibly deal with a range of different cryptographic constructions and protocols. We evaluate the method on a series of larger case studies of protocol code, previously checked using a whole-program analysis based on ProVerif, a leading verifier for cryptographic protocols. Our results indicate that compositional verification by typechecking with refinement types is more scalable than the best domain-specific analysis currently available for cryptographic code.