@techreport{bengtson2008refinement,
author = {Bengtson, Jesper and Bhargavan, Karthik and Fournet, Cédric and Gordon, Andy and Maffeis, Sergio},
title = {Refinement Types for Secure Implementations},
year = {2008},
month = {June},
abstract = {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 refinement types for expressing pre- and post-conditions within first-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 verification conditions that are passed to an SMT solver. We describe a series of checked examples. This is the first tool to verify authentication properties of cryptographic protocols by typechecking their source code.},
publisher = {IEEE Computer Society},
url = {http://approjects.co.za/?big=en-us/research/publication/refinement-types-for-secure-implementations/},
pages = {17-32},
isbn = {978-0-7695-3182-3},
edition = {20th IEEE Computer Security Foundations Symposium (CSF) 2008},
number = {MSR-TR-2008-118},
note = {20th IEEE Computer Security Foundations Symposium (CSF) 2008},
}