Pre- and Post-conditions for Security Typechecking

We verify implementations of cryptographic protocols that manipulate recursive data structures, such as lists. Our main applications are X.509 certificate chains and XML digital signatures. These applications are beyond the reach of automated provers such as ProVerif, since they require some form of induction. They can be verified using the F7 refinement typechecker, at the cost of annotating each data-processing function with logical formulas embedded in its type. However, this entails the duplication of many library functions, so that each instance can be given its own type. We propose a more flexible method for verifying ML programs that use cryptography and recursion. We annotate standard library functions (such as list processing functions) with precise, yet reusable types that refer to the pre- and post-conditions of their functional arguments, using generic logical predicates. We use these predicates both to specify higher-order functions and to track security events in programs and cryptographic libraries. We implement our method by extending the F7 typechecker with automated support for these predicates. We evaluate our approach experimentally by verifying a series of security libraries and protocols.