research-article

Modular verification of security protocol code by typing

Authors:

Karthikeyan Bhargavan,

Cédric Fournet,

Andrew D. GordonAuthors Info & Claims

ACM SIGPLAN Notices, Volume 45, Issue 1

Pages 445 - 456

https://doi.org/10.1145/1707801.1706350

Published: 17 January 2010 Publication History

Abstract

We propose a method for verifying the security of protocol implementations. Our method is based on declaring and enforcing invariants on the usage of cryptography. We develop cryptographic libraries that embed a logic model of their cryptographic structures and that specify preconditions and postconditions on their functions so as to maintain their invariants. We present a theory to justify the soundness of modular code verification via our method.

We implement the method for protocols coded in F# and verified using F7, our SMT-based typechecker for refinement types, that is, types carrying formulas to record invariants. As illustrated by a series of programming examples, our method can flexibly deal with a range of different cryptographic constructions and protocols.

We evaluate the method on a series of larger case studies of protocol code, previously checked using whole-program analyses based on ProVerif, a leading verifier for cryptographic protocols. Our results indicate that compositional verification by typechecking with refinement types is more scalable than the best domain-specific analysis currently available for cryptographic code.

References

[1]

M. Abadi. Secrecy by typing in security protocols. JACM, 46(5):749--786, 1999.

Digital Library

[2]

M. Bellare and C. Namprempre. Authenticated encryption: Relations among notions and analysis of the generic composition paradigm. J. Cryptology, 21(4), 2008.

Digital Library

[3]

J. Bengtson, K. Bhargavan, C. Fournet, A.D. Gordon, and S. Maffeis. Refinement types for secure implementations. Technical Report MSR-TR-2008-118, Microsoft Research, 2008. See also CSF'08.

Digital Library

[4]

K. Bhargavan, C. Fournet, and A.D. Gordon. Verified reference implementations of WS-Security protocols. In WS-FM'06, LNCS 4184, 2006a.

Digital Library

[5]

K. Bhargavan, C. Fournet, A.D. Gordon, and S. Tse. Verified interoperable implementations of security protocols. In CSFW'06, 2006b.

Digital Library

[6]

K. Bhargavan, C. Fournet, R. Corin, and E. Zalinescu. Cryptographically verified implementations for TLS. In ACM CCS, pages 459--468, 2008a.

Digital Library

[7]

K. Bhargavan, C. Fournet, A.D. Gordon, and N. Swamy. Verified implementations of the Information Card federated identity-management protocol. In ASIACCS'08, pages 123--135, 2008b.

Digital Library

[8]

B. Blanchet. An efficient cryptographic protocol verifier based on Prolog rules. In CSFW'01, pages 82--96, 2001.

Digital Library

[9]

B. Blanchet. A computationally sound mechanized prover for security protocols. In IEEE Symposium on Security and Privacy, 2006.

Digital Library

[10]

I. Cervesato, A.D. Jaggard, A. Scedrov, J.-K. Tsay, and C. Walstad. Breaking and fixing public-key Kerberos. Information and Computation, 206 (2-4):402--424, 2008.

Digital Library

[11]

S. Chaki and A. Datta. ASPIER: An automated framework for verifying security protocol implementations. In CSF'09, 2009.

Digital Library

[12]

E. Cohen. TAPS: A first-order verifier for cryptographic protocols. In 13th IEEE Computer Security Foundations Workshop, pages 144--158, 2000.

Digital Library

[13]

L. de Moura and N. Bjørner. Z3: An efficient SMT solver. In TACAS'08, pages 337--340. Springer, 2008. LNCS 4963.

Digital Library

[14]

D. Dolev and A. Yao. On the security of public key protocols. IEEE Transactions on Information Theory, IT-29(2):198--208, 1983.

Digital Library

[15]

C. Flanagan. Hybrid type checking. In ACM POPL'06, pages 245--256, 2006.

Digital Library

[16]

A.D. Gordon and A.S.A. Jeffrey. Authenticity by typing for security protocols. J. Computer Security, 11(4):451--521, 2003a.

Digital Library

[17]

A.D. Gordon and A.S.A. Jeffrey. Types and effects for asymmetric cryptographic protocols. J. Computer Security, 12(3/4):435--484, 2003b.

Digital Library

[18]

J. Goubault-Larrecq and F. Parrennes. Cryptographic protocol analysis on real C code. In VMCAI'05, pages 363--379, 2005.

Digital Library

[19]

C. Gunter. Semantics of programming languages. MIT Press, 1992.

Digital Library

[20]

E. Kleiner and A.W. Roscoe. On the relationship between web services security and traditional protocols. In MFPS XXI, 2005.

[21]

G. Lowe. Breaking and fixing the Needham-Schroeder public-key protocol using FDR. In TACAS, pages 147--166, 1996. LNCS 1055.

Digital Library

[22]

J.H. Morris, Jr. Protection in programming languages. Commun. ACM, 16 (1):15--21, 1973.

Digital Library

[23]

R. Needham and M. Schroeder. Using encryption for authentication in large networks of computers. Commun. ACM, 21(12):993--999, 1978.

Digital Library

[24]

L. Paulson. The inductive approach to verifying cryptographic protocols. J. Computer Security, 6:85--128, 1998.

[25]

L.C. Paulson. Logic and proof. Cambridge University lecture notes, 2008.

[26]

G.D. Plotkin. Denotational semantics with partial functions. Unpublished lecture notes, CSLI, Stanford University, July 1985.

[27]

P. Rondon, M. Kawaguchi, and R. Jhala. Liquid types. In ACM PLDI'08, pages 159--169, 2008.

Digital Library

Cited By

Tawiah KAsampana Asosega KAnsah RAppiah SOtoo DAponye ITinbil TAddai I(2023)Confirmed Malaria Cases in Children under Five Years: The Influence of Suspected Cases, Tested Cases, and Climatic ConditionsHealth & Social Care in the Community10.1155/2023/84693722023(1-8)Online publication date: 23-Jun-2023
https://doi.org/10.1155/2023/8469372
Jiang KBao YWang SLiu ZZhang TYin HStavrou ACremers CShi E(2022)Cache Refinement Type for Side-Channel Detection of Cryptographic SoftwareProceedings of the 2022 ACM SIGSAC Conference on Computer and Communications Security10.1145/3548606.3560672(1583-1597)Online publication date: 7-Nov-2022
https://dl.acm.org/doi/10.1145/3548606.3560672
Bhargavan KBichhawat ADo QHosseyni PKüsters RSchmitz GWürtele T(2021)A Tutorial-Style Introduction to $$\textsf {DY}^\star $$Protocols, Strands, and Logic10.1007/978-3-030-91631-2_4(77-97)Online publication date: 19-Nov-2021
https://doi.org/10.1007/978-3-030-91631-2_4
Show More Cited By

Index Terms

Modular verification of security protocol code by typing
1. Theory of computation
  1. Semantics and reasoning
    1. Program reasoning
      1. Program specifications

Recommendations

Modular code-based cryptographic verification
CCS '11: Proceedings of the 18th ACM conference on Computer and communications security

Type systems are effective tools for verifying the security of cryptographic programs. They provide automation, modularity and scalability, and have been applied to large security protocols. However, they traditionally rely on abstract assumptions on ...
Modular verification of security protocol code by typing
POPL '10: Proceedings of the 37th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages

We propose a method for verifying the security of protocol implementations. Our method is based on declaring and enforcing invariants on the usage of cryptography. We develop cryptographic libraries that embed a logic model of their cryptographic ...
Cryptographic verification by typing for a sample protocol implementation
Foundations of security analysis and design VI

Type systems are effective tools for verifying the security of cryptographic protocols and implementations. They provide automation, modularity and scalability, and have been applied to large protocols. In this tutorial, we illustrate the use of types ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM SIGPLAN Notices

ACM SIGPLAN Notices Volume 45, Issue 1

POPL '10

January 2010

500 pages

ISSN:0362-1340

EISSN:1558-1160

DOI:10.1145/1707801

Issue’s Table of Contents

POPL '10: Proceedings of the 37th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages
January 2010
520 pages
ISBN:9781605584799
DOI:10.1145/1706299
General Chair:
Manuel Hermenegildo
IMDEA-Software and T.U. of Madrid, Spain
,
Program Chair:
Jens Palsberg
UCLA, University of California, Los Angeles

Copyright © 2010 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 17 January 2010

Published in SIGPLAN Volume 45, Issue 1

Check for updates

Author Tags

Qualifiers

Research-article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

92
Total Citations
View Citations
648
Total Downloads

Downloads (Last 12 months)12
Downloads (Last 6 weeks)1

Reflects downloads up to 28 Sep 2024

Other Metrics

View Author Metrics

Citations

Cited By

Tawiah KAsampana Asosega KAnsah RAppiah SOtoo DAponye ITinbil TAddai I(2023)Confirmed Malaria Cases in Children under Five Years: The Influence of Suspected Cases, Tested Cases, and Climatic ConditionsHealth & Social Care in the Community10.1155/2023/84693722023(1-8)Online publication date: 23-Jun-2023
https://doi.org/10.1155/2023/8469372
Jiang KBao YWang SLiu ZZhang TYin HStavrou ACremers CShi E(2022)Cache Refinement Type for Side-Channel Detection of Cryptographic SoftwareProceedings of the 2022 ACM SIGSAC Conference on Computer and Communications Security10.1145/3548606.3560672(1583-1597)Online publication date: 7-Nov-2022
https://dl.acm.org/doi/10.1145/3548606.3560672
Bhargavan KBichhawat ADo QHosseyni PKüsters RSchmitz GWürtele T(2021)A Tutorial-Style Introduction to $$\textsf {DY}^\star $$Protocols, Strands, and Logic10.1007/978-3-030-91631-2_4(77-97)Online publication date: 19-Nov-2021
https://doi.org/10.1007/978-3-030-91631-2_4
Barthe GBetarte GCampo JLuna CPichardie D(2020)System-Level Non-interference of Constant-Time Cryptography. Part II: Verified Static Analysis and Stealth MemoryJournal of Automated Reasoning10.1007/s10817-020-09548-xOnline publication date: 17-Feb-2020
https://doi.org/10.1007/s10817-020-09548-x
Cassel DHuang YJia L(2019)Uncovering Information Flow Policy Violations in C Programs (Extended Abstract)Computer Security – ESORICS 201910.1007/978-3-030-29962-0_2(26-46)Online publication date: 23-Sep-2019
https://dl.acm.org/doi/10.1007/978-3-030-29962-0_2
Sassaman LPatterson MBratus SLocasto M(2013)Security Applications of Formal Language TheoryIEEE Systems Journal10.1109/JSYST.2012.22220007:3(489-500)Online publication date: Sep-2013
https://doi.org/10.1109/JSYST.2012.2222000
Bugliesi MCalzavara SEigner FMaffei M(2013)Logical foundations of secure resource management in protocol implementationsProceedings of the Second international conference on Principles of Security and Trust10.1007/978-3-642-36830-1_6(105-125)Online publication date: 16-Mar-2013
https://dl.acm.org/doi/10.1007/978-3-642-36830-1_6
Bocchi LDemangeon RYoshida N(2012)A Multiparty Multi-session LogicRevised Selected Papers of the 7th International Symposium on Trustworthy Global Computing - Volume 819110.1007/978-3-642-41157-1_7(97-111)Online publication date: 7-Sep-2012
https://dl.acm.org/doi/10.1007/978-3-642-41157-1_7
Aizatulin MDupressoir FGordon AJürjens J(2011)Verifying cryptographic code in cProceedings of the 8th international conference on Formal Aspects of Security and Trust10.1007/978-3-642-29420-4_1(1-20)Online publication date: 12-Sep-2011
https://dl.acm.org/doi/10.1007/978-3-642-29420-4_1
de Ruiter JPoll E(2011)Formal analysis of the EMV protocol suiteProceedings of the 2011 international conference on Theory of Security and Applications10.1007/978-3-642-27375-9_7(113-129)Online publication date: 31-Mar-2011
https://dl.acm.org/doi/10.1007/978-3-642-27375-9_7
Show More Cited By

View Options

Get Access

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Media

Figures

Other

Tables

View Issue’s Table of Contents