June 23, 2008 to June 25, 2008
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/CSF.2008.27
We present the design and implementation of a typechecker for verifying security properties of the source code of cryptographic protocols and access control mechanisms. The underlying type theory is a λ-calculus equipped with reﬁnement types for expressing pre- and post-conditions within ﬁrst-order logic. We derive formal cryptographic primitives and represent active adversaries within the type theory. Well-typed programs enjoy assertion-based security properties, with respect to a realistic threat model including key compromise. The implementation amounts to an enhanced typechecker for the general purpose functional language F#; typechecking generates veriﬁcation conditions that are passed to an SMT solver. We describe a series of checked examples. This is the ﬁrst tool to verify authentication properties of cryptographic protocols by typechecking their source code.
Jesper Bengtson, Karthikeyan Bhargavan, C?dric Fournet, Andrew D. Gordon, Sergio Maffeis, "Refinement Types for Secure Implementations", CSF, 2008, 2012 IEEE 25th Computer Security Foundations Symposium, 2012 IEEE 25th Computer Security Foundations Symposium 2008, pp. 17-32, doi:10.1109/CSF.2008.27