Imperial College London
Portrait Picture

DrSergioMaffeis

Faculty of Engineering, Department of Computing

Senior Lecturer
 
 
 
//

Contact

 

+44 (0)20 7594 8390sergio.maffeis Website

 
 
//

Location

 

441Huxley BuildingSouth Kensington Campus

//

Summary

 

Publications

Citation

BibTex format

@inproceedings{Maffeis:2008:10.1109/CSF.2008.27,
author = {Maffeis, S and Gordon, A and Fournet, C and Bhargavan, K and Bengtson, J},
doi = {10.1109/CSF.2008.27},
pages = {17--32},
publisher = {IEEE Computer Society},
title = {Refinement Types for Secure Implementations},
url = {http://dx.doi.org/10.1109/CSF.2008.27},
year = {2008}
}
Download

RIS format (EndNote, RefMan)

TY  - CPAPER
AB  - 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 lambda-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.
AU  - Maffeis,S
AU  - Gordon,A
AU  - Fournet,C
AU  - Bhargavan,K
AU  - Bengtson,J
DO  - 10.1109/CSF.2008.27
EP  - 32
PB  - IEEE Computer Society
PY  - 2008///
SP  - 17
TI  - Refinement Types for Secure Implementations
UR  - http://dx.doi.org/10.1109/CSF.2008.27
UR  - http://hdl.handle.net/10044/1/5707
ER  -
Download