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.
|Title of host publication||Proceedings of the 21st IEEE Computer Security Foundations Symposium, CSF 2008, Pittsburgh, Pennsylvania, 23-25 June 2008|
|Publisher||Institute of Electrical and Electronics Engineers (IEEE)|
|Number of pages||16|
|Publication status||Published - Jun 2008|