research-article

Modular code-based cryptographic verification

Authors:

Cédric Fournet,

Markulf Kohlweiss,

Pierre-Yves StrubAuthors Info & Claims

CCS '11: Proceedings of the 18th ACM conference on Computer and communications security

Pages 341 - 350

https://doi.org/10.1145/2046707.2046746

Published: 17 October 2011 Publication History

Abstract

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 the underlying cryptographic primitives, expressed in symbolic models. Cryptographers usually reason on security assumptions using lower level, computational models that precisely account for the complexity and success probability of attacks. These models are more realistic, but they are harder to formalize and automate. We present the first modular automated program verification method based on standard cryptographic assumptions. We show how to verify ideal functionalities and protocols written in ML by typing them against new cryptographic interfaces using F7, a refinement type checker coupled with an SMT-solver. We develop a probabilistic core calculus for F7 and formalize its type safety in Coq.

We build typed module and interfaces for MACs, signatures, and encryptions, and establish their authenticity and secrecy properties. We relate their ideal functionalities and concrete implementations, using game-based program transformations behind typed interfaces. We illustrate our method on a series of protocol implementations.

References

[1]

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

Digital Library

[2]

M. Abadi and B. Blanchet. Analyzing security protocols with secrecy types and logic programs. JACM, 52 (1), 2005.

Digital Library

[3]

M. Abadi and P. Rogaway. Reconciling two views of cryptography (the computational soundness of formal encryption). Journal of Cryptology, 15 (2), 2002.

Digital Library

[4]

M. Backes, B. Pfitzmann, and M. Waidner. Symmetric authentication in a simulatable Dolev-Yao-style cryptographic library. Int. J. Inf. Sec., 4 (3), 2005.

[5]

M. Backes, B. Pfitzmann, and M. Waidner. The reactive simulatability (RSIM) framework for asynchronous systems. Inf. Comput., 205 (12), 2007.

Digital Library

[6]

M. Backes, M. Dürmuth, D. Hofheinz, and R. Küsters. Conditional reactive simulatability. Int. J. Inf. Sec., 7 (2), 2008.

Digital Library

[7]

M. Backes, D. Hofheiz, and D. Unruh. CoSP: A general framework for computational soundness proofs. In ACM CCS 09. Conference on Computer and Communications Security, 2009.

Digital Library

[8]

M. Backes, M. Maffei, and D. Unruh. Computational sound verification of source code. In ACM CCS 09 13th Conference on Computer and Communications Security, 2010.

Digital Library

[9]

G. Barthe, B. Grégoire, S. Heraud, and S. Z. Béguelin. Formal certification of ElGamal encryption. In FAST 2008, 2008.

[10]

easycrypt2011G. Barthe, B. Gregoire, S. Heraud, and S. Zanella Béguelin. Computer-aided security proofs for the working cryptographer. In Advances in Cryptology -- CRYPTO 2011, 2011.

Digital Library

[11]

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

Digital Library

[12]

M. Bellare and P. Rogaway. Introduction to modern cryptography. In UCSD CSE 207 Course Notes, 2005.

[13]

M. Bellare and P. Rogaway. The security of triple encryption and a framework for code-based game-playing proofs. In Advances in Cryptology -- EUROCRYPT 2006, 2006.

Digital Library

[14]

M. Bellare, R. Canetti, and H. Krawczyk. Keying hash functions for message authentication. In Advances in Cryptology -- CRYPTO '96, 1996.

Digital Library

[15]

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

Digital Library

[16]

K. Bhargavan, C. Fournet, R. Corin, and E. Zalinescu. Cryptographically verified implementations for TLS. In ACM CCS 09 Conference on Computer and Communications Security, 2008.

Digital Library

[17]

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

Digital Library

[18]

K. Bhargavan, R. Corin, P.-M. Dénielou, C. Fournet, and J. Leifer. Cryptographic protocol synthesis and verification for multiparty sessions. In CSF 2009 IEEE Computer Security Foundations Symposium, 2009.

Digital Library

[19]

K. Bhargavan, C. Fournet, and A. D. Gordon. Modular verification of security protocol code by typing. In POPL 2010 Annual ACM Symposium on Principles of Programming Languages, 2010.

Digital Library

[20]

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

Digital Library

[21]

B. Blanchet, M. Abadi, and C. Fournet. Automated verification of selected equivalences for security protocols. JLAP, 75 (1), 2008.

[22]

R. Canetti. Universally composable security: A new paradigm for cryptographic protocols. In FOCS, 2001.

Digital Library

[23]

S. Chaki and A. Datta. ASPIER: An automated framework for verifying security protocol implementations. In CSF 2009 IEEE Computer Security Foundations Symposium, 2009.

Digital Library

[24]

N. A. Danielsson. Lightweight semiformal time complexity analysis for purely functional data structures. In POPL 2008 Annual ACM Symposium on Principles of Programming Languages, 2008.

Digital Library

[25]

A. Datta, A. Derek, J. C. Mitchell, V. Shmatikov, and M. Turuani. Probabilistic polynomial-time semantics for a protocol security logic. In ICALP 2005 International Colloquium on Automata, Languages and Programming, 2005.

Digital Library

[26]

A. Datta, A. Derek, J. C. Mitchell, and A. Roy. Protocol composition logic (PCL). Electr. Notes Theor. Comput. Sci., 172, 2007.

Digital Library

[27]

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

[28]

ens, and Naumann}francois2011F. Dupressoir, A. D. Gordon, J. Jürjens, and D. A. Naumann. Guiding a general-purpose C verifier to prove cryptographic protocols. In CSF 2011 IEEE Computer Security Foundations Symposium, 2011.

Digital Library

[29]

N. A. Durgin, J. C. Mitchell, and D. Pavlovic. A compositional logic for proving security properties of protocols. JCS, 11 (4), 2003.

Digital Library

[30]

C. Fournet, K. Bhargavan, and A. Gordon. Cryptographic verification of protocol implementations by typechecking. In FOSAD, 2011.

[31]

S. Goldwasser, S. Micali, and R. Rivest. A digital signature scheme secure against adaptive chosen-message attack. SIAM Journal on Computing, 17 (2), 1988.

Digital Library

[32]

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

Digital Library

[33]

S. Halevi. A plausible approach to computer-aided cryptographic proofs. Cryptology ePrint Archive, Report 2005/181, 2005.

[34]

D. Hofheinz, D. Unruh, and J. Müller-Quade. Polynomial runtime and composability. Cryptology ePrint Archive, Report 2009/023, 2009.

[35]

B. M. Kapron and S. A. Cook. A new characterization of type 2 feasibility. SIAM Journal on Computing, 25, 1996.

Digital Library

[36]

H. Krawczyk, M. Bellare, and R. Canetti. HMAC: Keyed-hashing for message authentication, 1997. RFC 2104.

Digital Library

[37]

R. Küsters. Simulation-based security with inexhaustible interactive Turing machines. In CSFW 2006 IEEE Computer Security Foundations Workshop, 2006.

Digital Library

[38]

R. Küsters and M. Tuengerthal. Universally composable symmetric encryption. In CSF, 2009.

Digital Library

[39]

P. Laud. Semantics and program analysis of computationally secure information flow. In ESOP 2001 European Symposium on Programming, volume 2028, Apr. 2001.

Digital Library

[40]

P. Laud. Secrecy types for a simulatable cryptographic library. In ACM CCS 09 Conference on Computer and Communications Security, 2005.

Digital Library

[41]

P. Laud. On the computational soundness of cryptographically-masked flows. In POPL 2008 Annual ACM Symposium on Principles of Programming Languages, 2008.

Digital Library

[42]

J. H. Morris, Jr. Protection in programming languages. Communications of the Association for Computing Machinery, 16 (1), 1973.

Digital Library

[43]

C. Rackoff and D. R. Simon. Non-interactive zero-knowledge proof of knowledge and chosen ciphertext attack. In Advances in Cryptology -- CRYPTO'91, 1991.

Digital Library

[44]

J. C. Reynolds. Types, abstraction and parametric polymorphism. In IFIP Congress, 1983.

[45]

A. Roy, A. Datta, A. Derek, and J. C. Mitchell. Inductive trace properties for computational security. JCS, 18 (6), 2010.

Digital Library

[46]

The Coq Development Team. The Coq Proof Assistant Reference Manual -- Version V8.3, 2011.

Cited By

Borkowski MVazou NJhala R(2024)Mechanizing Refinement TypesProceedings of the ACM on Programming Languages10.1145/36329128:POPL(2099-2128)Online publication date: 5-Jan-2024
https://dl.acm.org/doi/10.1145/3632912
Bhargavan KBichhawat AHosseyni PKüsters RPruiksma KSchmitz GWaldmann CWürtele T(2024)Layered Symbolic Security Analysis in $$\textsf {DY}^\star $$Computer Security – ESORICS 202310.1007/978-3-031-51479-1_1(3-21)Online publication date: 12-Jan-2024
https://doi.org/10.1007/978-3-031-51479-1_1
Haselwarter PRivas EVan Muylder AWinterhalter TAbate CSidorenco NHriţcu CMaillard KSpitters B(2023)SSProve: A Foundational Framework for Modular Cryptographic Proofs in CoqACM Transactions on Programming Languages and Systems10.1145/359473545:3(1-61)Online publication date: 20-Jul-2023
https://dl.acm.org/doi/10.1145/3594735
Show More Cited By

Index Terms

Modular code-based cryptographic verification
1. Security and privacy
2. Theory of computation
  1. Semantics and reasoning
    1. Program reasoning
      1. Program specifications

Recommendations

Public-Key encryption from ID-Based encryption without one-time signature
OTM'06: Proceedings of the 2006 international conference on On the Move to Meaningful Internet Systems: AWeSOMe, CAMS, COMINF, IS, KSinBIT, MIOS-CIAO, MONET - Volume Part I

Design a secure public key encryption scheme and its security proof are one of the main interests in cryptography In 2004, Canetti, Halevi and Katz [8] constructed a public key encryption (PKE) from a selective identity-based encryption scheme with a ...
A novel identity-based strong designated verifier signature scheme

Unlike ordinary digital signatures, a designated verifier signature scheme makes it possible for a signer to convince a designated verifier that she has signed a message in such a way that the designated verifier cannot transfer the signature to a third ...
An efficient ID-based cryptographic encryption based on discrete logarithm problem and integer factorization problem

ID-based encryption (identity-based) is a very useful tool in cryptography. It has many potential applications. The security of traditional ID-based encryption scheme wholly depends on the security of secret keys. Exposure of secret keys requires ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

CCS '11: Proceedings of the 18th ACM conference on Computer and communications security

October 2011

742 pages

ISBN:9781450309486

DOI:10.1145/2046707

General Chair:
Yan Chen
Northwestern University, USA
,
Program Chairs:
George Danezis
Microsoft Research Cambridge, UK
,
Vitaly Shmatikov
University of Texas at Austin, USA

Copyright © 2011 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]

Sponsors

SIGSAC: ACM Special Interest Group on Security, Audit, and Control

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 17 October 2011

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article

Conference

CCS'11

Sponsor:

SIGSAC

CCS'11: the ACM Conference on Computer and Communications Security

October 17 - 21, 2011

Illinois, Chicago, USA

Acceptance Rates

CCS '11 Paper Acceptance Rate 60 of 429 submissions, 14%;

Overall Acceptance Rate 1,261 of 6,999 submissions, 18%

Upcoming Conference

CCS '24

Sponsor:
sigsac

ACM SIGSAC Conference on Computer and Communications Security

October 14 - 18, 2024

Salt Lake City , UT , USA

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

52
Total Citations
View Citations
439
Total Downloads

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

Reflects downloads up to 26 Sep 2024

Other Metrics

View Author Metrics

Citations

Cited By

Borkowski MVazou NJhala R(2024)Mechanizing Refinement TypesProceedings of the ACM on Programming Languages10.1145/36329128:POPL(2099-2128)Online publication date: 5-Jan-2024
https://dl.acm.org/doi/10.1145/3632912
Bhargavan KBichhawat AHosseyni PKüsters RPruiksma KSchmitz GWaldmann CWürtele T(2024)Layered Symbolic Security Analysis in $$\textsf {DY}^\star $$Computer Security – ESORICS 202310.1007/978-3-031-51479-1_1(3-21)Online publication date: 12-Jan-2024
https://doi.org/10.1007/978-3-031-51479-1_1
Haselwarter PRivas EVan Muylder AWinterhalter TAbate CSidorenco NHriţcu CMaillard KSpitters B(2023)SSProve: A Foundational Framework for Modular Cryptographic Proofs in CoqACM Transactions on Programming Languages and Systems10.1145/359473545:3(1-61)Online publication date: 20-Jul-2023
https://dl.acm.org/doi/10.1145/3594735
Gancher JGibson SSingh PDharanikota SParno B(2023)Owl: Compositional Verification of Security Protocols via an Information-Flow Type System2023 IEEE Symposium on Security and Privacy (SP)10.1109/SP46215.2023.10179477(1130-1147)Online publication date: May-2023
https://doi.org/10.1109/SP46215.2023.10179477
Ho SProtzenko JBichhawat ABhargavan K(2022)Noise: A Library of Verified High-Performance Secure Channel Protocol Implementations2022 IEEE Symposium on Security and Privacy (SP)10.1109/SP46214.2022.9833621(107-124)Online publication date: May-2022
https://doi.org/10.1109/SP46214.2022.9833621
Dupressoir FKohbrok KOechsner S(2022)Bringing State-Separating Proofs to EasyCrypt A Security Proof for Cryptobox2022 IEEE 35th Computer Security Foundations Symposium (CSF)10.1109/CSF54842.2022.9919671(227-242)Online publication date: Aug-2022
https://doi.org/10.1109/CSF54842.2022.9919671
Bhargavan KBichhawat ADo QHosseyni PKüsters RSchmitz GWürtele TKim YKim JVigna GShi E(2021)An In-Depth Symbolic Security Analysis of the ACME StandardProceedings of the 2021 ACM SIGSAC Conference on Computer and Communications Security10.1145/3460120.3484588(2601-2617)Online publication date: 12-Nov-2021
https://dl.acm.org/doi/10.1145/3460120.3484588
Delignat-Lavaud AFournet CParno BProtzenko JRamananandro TBosamiya JLallemand JRakotonirina IZhou Y(2021)A Security Model and Fully Verified Implementation for the IETF QUIC Record Layer2021 IEEE Symposium on Security and Privacy (SP)10.1109/SP40001.2021.00039(1162-1178)Online publication date: May-2021
https://doi.org/10.1109/SP40001.2021.00039
Karim IHussain SBertino E(2021)ProChecker: An Automated Security and Privacy Analysis Framework for 4G LTE Protocol Implementations2021 IEEE 41st International Conference on Distributed Computing Systems (ICDCS)10.1109/ICDCS51616.2021.00079(773-785)Online publication date: Jul-2021
https://doi.org/10.1109/ICDCS51616.2021.00079
Bhargavan KBichhawat ADo QHosseyni PKüsters RSchmitz GWürtele T(2021)$\text{DY}^{\star}$: A Modular Symbolic Verification Framework for Executable Cryptographic Protocol Code2021 IEEE European Symposium on Security and Privacy (EuroS&P)10.1109/EuroSP51992.2021.00042(523-542)Online publication date: Sep-2021
https://doi.org/10.1109/EuroSP51992.2021.00042
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 Table of Contents