Typechecking Higher-Order Security Libraries

Typechecking Higher-Order Security Libraries,10.1007/978-3-642-17164-2_5,Karthikeyan Bhargavan,Cédric Fournet,Nataliya Guts

Typechecking Higher-Order Security Libraries   (Citations: 4)
BibTex | RIS | RefWorks Download
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 post-conditions. 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 security libraries and protocols.
Cumulative Annual
View Publication
The following links allow you to view full publications. These links are maintained by other sources not affiliated with Microsoft Academic Search.
    • ...We extend the type system, implementation, and cryptographic libraries developed in earlier work [3, 6]. Additional details, including source code and the full version of this paper, are available online [7]...
    • ...The full interface is available online [7]...
    • ...(The full interface for public-key signature functions is available online [7].) Hence, the type of the judge is:...

    Karthikeyan Bhargavanet al. Typechecking Higher-Order Security Libraries

Sort by: