Skip to Main content Skip to Navigation
Journal articles

Refinement types for secure implementations

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.
Complete list of metadata

Cited literature [95 references]  Display  Hide  Download

https://hal.inria.fr/hal-01294973
Contributor : Bhargavan Karthikeyan <>
Submitted on : Monday, April 4, 2016 - 2:27:33 PM
Last modification on : Monday, November 16, 2020 - 3:26:06 PM
Long-term archiving on: : Tuesday, July 5, 2016 - 1:51:20 PM

File

refinement-types-for-secure-im...
Files produced by the author(s)

Identifiers

Citation

Jesper Bengtson, Karthikeyan Bhargavan, Cédric Fournet, Andrew D. Gordon, Sergio Maffeis. Refinement types for secure implementations. ACM Transactions on Programming Languages and Systems (TOPLAS), ACM, 2011, 33 (2), ⟨10.1145/1890028.1890031⟩. ⟨hal-01294973⟩

Share

Metrics

Record views

123

Files downloads

424