Modular code-based cryptographic verification

Cédric Fournet, Markulf Kohlweiss, Pierre-Yves Strub

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


Type systems are effective tools for verifying the security of cryptographic programs. They provide automation, modularity and scalability, and have been applied to large security protocols. However, they traditionally rely on abstract assumptions on the underlying cryptographic primitives, expressed in symbolic models. Cryptographers usually reason on security assumptions using lower level, computational models that precisely account for the complexity and success probability of attacks. These models are more realistic, but they are harder to formalize and automate. We present the first modular automated program verification method based on standard cryptographic assumptions. We show how to verify ideal functionalities and protocols written in ML by typing them against new cryptographic interfaces using F7, a refinement type checker coupled with an SMT-solver. We develop a probabilistic core calculus for F7 and formalize its type safety in Coq.

We build typed module and interfaces for MACs, signatures, and encryptions, and establish their authenticity and secrecy properties. We relate their ideal functionalities and concrete implementations, using game-based program transformations behind typed interfaces. We illustrate our method on a series of protocol implementations
Original languageEnglish
Title of host publicationProceedings of the 18th ACM Conference on Computer and Communications Security, CCS 2011, Chicago, Illinois, USA, October 17-21, 2011
Number of pages10
ISBN (Electronic)978-1-4503-0948-6
Publication statusPublished - 2011
Event18th ACM Conference on Computer and Communications Security - Swissôtel Chicago, Chicago, IL, United States
Duration: 17 Oct 201121 Oct 2011


Conference18th ACM Conference on Computer and Communications Security
Abbreviated titleACM CCS 2011
Country/TerritoryUnited States
CityChicago, IL
Internet address


Dive into the research topics of 'Modular code-based cryptographic verification'. Together they form a unique fingerprint.

Cite this