Typechecking Higher-Order Security Libraries

9 years 8 months ago
Typechecking Higher-Order Security Libraries
Abstract. We propose a flexible method for verifying the security of ML programs that use cryptography and recursive data structures. Our main applications are X.509 certificate chains, secure logs for multi-party games, and XML digital signatures. These applications are beyond the reach of automated cryptographic verifiers such as ProVerif, since they require some form of induction. They can be verified using refinement types (that is, types with embedded logical formulas, tracking security events). However, this entails replicating higher-order library functions and annotating each instance with its own logical pre- and postconditions. Instead, we equip higher-order functions with precise, yet reusable types that can refer to the pre- and post-conditions of their functional arguments, using generic logical predicates. 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 se...
Karthikeyan Bhargavan, Cédric Fournet, Nata
Added 05 Dec 2010
Updated 05 Dec 2010
Type Conference
Year 2010
Authors Karthikeyan Bhargavan, Cédric Fournet, Nataliya Guts
Comments (0)