Modular verification of security protocol code by typing

Karthikeyan Bhargavan, Cédric Fournet, Andrew D. Gordon

Research output: Chapter in Book/Report/Conference proceedingConference contribution


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. We develop cryptographic libraries that embed a logic model of their cryptographic structures and that specify preconditions and postconditions 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 carrying 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 whole-program analyses 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.
Original languageEnglish
Title of host publicationProceedings of the 37th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages
Place of PublicationNew York, NY, USA
Number of pages12
ISBN (Print)978-1-60558-479-9
Publication statusPublished - 2010


  • f7, refinement type


Dive into the research topics of 'Modular verification of security protocol code by typing'. Together they form a unique fingerprint.

Cite this