research-article

Formal certification of code-based cryptographic proofs

Authors:

Benjamin Grégoire,

Santiago Zanella BéguelinAuthors Info & Claims

ACM SIGPLAN Notices, Volume 44, Issue 1

Pages 90 - 101

https://doi.org/10.1145/1594834.1480894

Published: 21 January 2009 Publication History

Abstract

As cryptographic proofs have become essentially unverifiable, cryptographers have argued in favor of developing techniques that help tame the complexity of their proofs. Game-based techniques provide a popular approach in which proofs are structured as sequences of games and in which proof steps establish the validity of transitions between successive games. Code-based techniques form an instance of this approach that takes a code-centric view of games, and that relies on programming language theory to justify proof steps. While code-based techniques contribute to formalize the security statements precisely and to carry out proofs systematically, typical proofs are so long and involved that formal verification is necessary to achieve a high degree of confidence. We present Certicrypt, a framework that enables the machine-checked construction and verification of code-based proofs. Certicrypt is built upon the general-purpose proof assistant Coq, and draws on many areas, including probability, complexity, algebra, and semantics of programming languages. Certicrypt provides certified tools to reason about the equivalence of probabilistic programs, including a relational Hoare logic, a theory of observational equivalence, verified program transformations, and game-based techniques such as reasoning about failure events. The usefulness of Certicrypt is demonstrated through various examples, including a proof of semantic security of OAEP (with a bound that improves upon existing published results), and a proof of existential unforgeability of FDH signatures. Our work provides a first yet significant step towards Halevi's ambitious programme of providing tool support for cryptographic proofs.

References

[1]

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

Digital Library

[2]

R. Affeldt, M. Tanaka, and N. Marti. Formal proof of provable security by game-playing in a proof assistant. In Proceedings of security by game-playing in a proof assistant. In Proceedings of Lecture Notes in Computer Science, pages 151--168. Springer, 2007.

Digital Library

[3]

T. Amtoft, S. Bandhakavi, and A. Banerjee. A logic for information flow in object-oriented programs. In Proceedings of the 33rd ACM Symposium on Principles of Programming Languages, pages 91--102. ACM Press, 2006.

Digital Library

[4]

P. Audebaud and C. Paulin-Mohring. Proofs of randomized algorithms in Coq. Science of Computer Programming, 2008.

Digital Library

[5]

M. Backes and P. Laud. Computationally sound secrecy proofs by mechanized flow analysis. In Proceedings of the 13th ACM Conference on Computer and Communications Security, pages 370--379. ACM Press, 2006.

Digital Library

[6]

G. Barthe, J. Cederquist, and S. Tarento. A machine-checked formalization of the generic model and the random oracle model. In 2nd International Joint Conference on Automated Reasoning, pages 385--399. Springer-Verlag, 2004.

[7]

M. Bellare and P. Rogaway. Optimal asymmetric encryption -- How to encrypt with RSA. In Advances in Cryptology - EUROCRYPT'94, volume 950 of Lecture Notes in Computer Science, pages 92--111. Springer-Verlag, 1995.

[8]

M. Bellare and P. Rogaway. The security of triple encryption and a framework for code-based game-playing proofs. In Advances in Cryptology -- EUROCRYPT'06, volume 4004 of Lecture Notes in Computer Science, pages 409--426, 2006.

Digital Library

[9]

N. Benton. Simple relational correctness proofs for static analyses and program transformations. In Proceedings of the 31th ACM Symposium on Principles of Programming Languages, pages 14--25. ACM Press, 2004.

Digital Library

[10]

Y. Bertot, B. Gregoire, and X. Leroy. A structured approach to proving compiler optimizations based on dataflow analysis. In International Workshop on Types for Proofs and Programs, volume 3839 of LNCS, pages 66--81. Springer-Verlag, 2006.

Digital Library

[11]

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

Digital Library

[12]

B. Blanchet and D. Pointcheval. Automated security proofs with protocols. In IEEE Symposium on Security and Privacy, pages 140--154, 2006. volume 4117 of Lecture Notes in Computer Science, pages 537--554. Springer-Verlag, 2006.

Digital Library

[13]

R. Canetti, O. Goldreich, and S. Halevi. The random oracle methodology, revisited. J. ACM, 51(4):557--594, 2004.

Digital Library

[14]

R. Corin and J. den Hartog. A probabilistic Hoare-style logic for game-based cryptographic proofs. In Proceedings of the 33rd International Colloquium on Automata, Languages and Programming, volume 4052 of LNCS, pages 252--263, 2006.

Digital Library

[15]

J.-S. Coron. On the exact security of Full Domain Hash. In Advances in Cryptology, volume 1880 of Lecture Notes in Computer Science, pages 229--235. Springer-Verlag, 2000.

Digital Library

[16]

J. Courant, M. Daubignard, C. Ene, P. Lafourcade, and Y. Lakhnech. Towards automated proofs for asymmetric encryption in the random oracle model. In Computer and Communications Security. ACM Press, 2008.

Digital Library

[17]

E. Fujisaki, T. Okamoto, D. Pointcheval, and J. Stern. RSA-OAEP is secure under the RSA assumption. Journal of Cryptology, 17(2):81--104, 2004.

Digital Library

[18]

S. Goldwasser and S. Micali. Probabilistic encryption. J. Comput. Syst. Sci., 28(2):270--299, 1984. S. Halevi. A plausible approach to computer-aided cryptographic proofs. Cryptology ePrint Archive, Report 2005/181, 2005.

[19]

J. Hurd, A. McIver, and C. Morgan. Probabilistic guarded commands mechanized in HOL. Theor. Comput. Sci., 346(1):96--112, 2005.

Digital Library

[20]

B. Jonsson, K. G. Larsen, and W. Yi. Probabilistic extensions of process algebras. In Handbook of Process Algebra, pages 685--711. Elsevier, 2001.

[21]

D. Kozen. Semantics of probabilistic programs. J. Comput. Syst. Sci., 22:328--350, 1981.

[22]

P. Laud. Semantics and program analysis of computationally secure information flow. In European Symposium on Programming, volume 2028 of Lecture Notes in Computer Science, pages 77--91. Springer-Verlag, 2001.

Digital Library

[23]

X. Leroy. Formal certification of a compiler back-end, or: programming a compiler with a proof assistant. In Proceedings of the 33rd ACM Symposium Principles of Programming Languages, pages 42--54. ACM Press, 2006.

Digital Library

[24]

C. Meadows. Formal methods for cryptographic protocol analysis: Emerging issues and trends. IEEE Journal on Selected Areas in Communications, 21(1):44--54, 2003.

Digital Library

[25]

D. Nowak. A framework for game-based security proofs. In Information and Communications Security, volume 4861, pages 319--333. Springer-Verlag, 2007.

Digital Library

[26]

N. Ramsey and A. Pfeffer. Stochastic lambda calculus and monads of probability distributions. In Proceedings of the 29th ACM Symposium on Principles of Programming Languages, pages 154--165. ACM Press, 2002.

Digital Library

[27]

A. Roy, A. Datta, A. Derek, and J. C. Mitchell. Inductive proofs of computational secrecy. In European Symposium On Research In Computer Security, volume 4734 of Lecture Notes in Computer Science, pages 219--234. Springer-Verlag, 2007.

Digital Library

[28]

A. Sabelfeld and D. Sands. A per model of secure information flow in sequential programs. Higher-Order and Symbolic Computation, 14(1):59--91, 2001.

Digital Library

[29]

V. Shoup. OAEP reconsidered. In Advances in Cryptology -- CRYPTO'01, volume 2139 of Lecture Notes in Computer Science, pages 239--259. Springer-Verlag, 2001.

Digital Library

[30]

V. Shoup. Sequences of games: a tool for taming complexity in security proofs. Cryptology ePrint Archive, Report 2004/332, 2004.

[31]

C. Sprenger and D. Basin. Cryptographically-sound protocol-model abstractions. In Proceedings of CSF'08, pages 115--129. IEEE Computer Society, 2008.

Digital Library

[32]

J. Stern. Why provable security matters? In Advances in Cryptology -- EUROCRYPT'03, volume 2656 of Lecture Notes in Computer Science. Springer-Verlag, 2003.

Digital Library

[33]

The Coq development team. The Coq Proof Assistant Reference Manual v8.1, 2006. Available at http://coq.inria.fr

Cited By

Baelde DFontaine CKoutsos AScerri GVignon T(2024)A Probabilistic Logic for Concrete Security2024 IEEE 37th Computer Security Foundations Symposium (CSF)10.1109/CSF61375.2024.00046(324-339)Online publication date: 8-Jul-2024
https://doi.org/10.1109/CSF61375.2024.00046
Xu YLi ZDong NKuchta VHou ZLiu D(2024)Formal Verification Techniques for Post-quantum Cryptography: A Systematic ReviewEngineering of Complex Computer Systems10.1007/978-3-031-66456-4_19(346-366)Online publication date: 29-Sep-2024
https://doi.org/10.1007/978-3-031-66456-4_19
Linvill KKaki GWustrow E(2023)Verifying Indistinguishability of Privacy-Preserving ProtocolsProceedings of the ACM on Programming Languages10.1145/36228497:OOPSLA2(1442-1469)Online publication date: 16-Oct-2023
https://dl.acm.org/doi/10.1145/3622849
Show More Cited By

Index Terms

Formal certification of code-based cryptographic proofs
1. Software and its engineering
  1. Software notations and tools
    1. Compilers
    2. Formal language definitions
2. Theory of computation

Recommendations

Formal certification of code-based cryptographic proofs
POPL '09: Proceedings of the 36th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages

As cryptographic proofs have become essentially unverifiable, cryptographers have argued in favor of developing techniques that help tame the complexity of their proofs. Game-based techniques provide a popular approach in which proofs are structured as ...
Formally Certifying the Security of Digital Signature Schemes
SP '09: Proceedings of the 2009 30th IEEE Symposium on Security and Privacy

We present two machine-checked proofs of the existentialunforgeability under adaptive chosen-message attacks of the FullDomain Hash signature scheme. These proofs formalize the originalargument of Bellare and Rogaway, and an optimal reduction by ...
MoSeL: a general, extensible modal framework for interactive proofs in separation logic

A number of tools have been developed for carrying out separation-logic proofs mechanically using an interactive proof assistant. One of the most advanced such tools is the Iris Proof Mode (IPM) for Coq, which offers a rich set of tactics for making ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM SIGPLAN Notices

ACM SIGPLAN Notices Volume 44, Issue 1

POPL '09

January 2009

453 pages

ISSN:0362-1340

EISSN:1558-1160

DOI:10.1145/1594834

Issue’s Table of Contents

POPL '09: Proceedings of the 36th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages
January 2009
464 pages
ISBN:9781605583792
DOI:10.1145/1480881
General Chair:
Zhong Shao
Yale University, USA
,
Program Chair:
Benjamin C. Pierce
University of Pennsylvania, USA

Copyright © 2009 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: 21 January 2009

Published in SIGPLAN Volume 44, Issue 1

Check for updates

Author Tags

Qualifiers

Research-article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

231
Total Citations
View Citations
1,092
Total Downloads

Downloads (Last 12 months)120
Downloads (Last 6 weeks)10

Reflects downloads up to 28 Sep 2024

Other Metrics

View Author Metrics

Citations

Cited By

Baelde DFontaine CKoutsos AScerri GVignon T(2024)A Probabilistic Logic for Concrete Security2024 IEEE 37th Computer Security Foundations Symposium (CSF)10.1109/CSF61375.2024.00046(324-339)Online publication date: 8-Jul-2024
https://doi.org/10.1109/CSF61375.2024.00046
Xu YLi ZDong NKuchta VHou ZLiu D(2024)Formal Verification Techniques for Post-quantum Cryptography: A Systematic ReviewEngineering of Complex Computer Systems10.1007/978-3-031-66456-4_19(346-366)Online publication date: 29-Sep-2024
https://doi.org/10.1007/978-3-031-66456-4_19
Linvill KKaki GWustrow E(2023)Verifying Indistinguishability of Privacy-Preserving ProtocolsProceedings of the ACM on Programming Languages10.1145/36228497:OOPSLA2(1442-1469)Online publication date: 16-Oct-2023
https://dl.acm.org/doi/10.1145/3622849
Feng SChen MSu HKaminski BKatoen JZhan N(2023)Lower Bounds for Possibly Divergent Probabilistic ProgramsProceedings of the ACM on Programming Languages10.1145/35860517:OOPSLA1(696-726)Online publication date: 6-Apr-2023
https://doi.org/10.1145/3586051
Jiang KChait-Roth DDeStefano ZWalfish MWies T(2023)Less is more: refinement proofs for probabilistic proofs2023 IEEE Symposium on Security and Privacy (SP)10.1109/SP46215.2023.10179393(1112-1129)Online publication date: May-2023
https://doi.org/10.1109/SP46215.2023.10179393
Dickerson RYe QZhang MDelaware B(2022)RHLE: Modular Deductive Verification of Relational PropertiesProgramming Languages and Systems10.1007/978-3-031-21037-2_4(67-87)Online publication date: 5-Dec-2022
https://dl.acm.org/doi/10.1007/978-3-031-21037-2_4
Chen MKatoen JKlinkenberg LWinkler T(2022)Does a Program Yield the Right Distribution?Computer Aided Verification10.1007/978-3-031-13185-1_5(79-101)Online publication date: 7-Aug-2022
https://dl.acm.org/doi/10.1007/978-3-031-13185-1_5
Barthe GJacomme CKremer S(2021)Universal Equivalence and Majority of Probabilistic Programs over Finite FieldsACM Transactions on Computational Logic10.1145/348706323:1(1-42)Online publication date: 22-Nov-2021
https://dl.acm.org/doi/10.1145/3487063
Aguirre ABarthe GGaboardi MGarg DKatsumata SSato T(2021)Higher-order probabilistic adversarial computations: categorical semantics and program logicsProceedings of the ACM on Programming Languages10.1145/34735985:ICFP(1-30)Online publication date: 22-Aug-2021
https://doi.org/10.1145/3473598
Barbosa MBarthe GFan XGrégoire BHung SKatz JStrub PWu XZhou LKim YKim JVigna GShi E(2021)EasyPQC: Verifying Post-Quantum CryptographyProceedings of the 2021 ACM SIGSAC Conference on Computer and Communications Security10.1145/3460120.3484567(2564-2586)Online publication date: 12-Nov-2021
https://dl.acm.org/doi/10.1145/3460120.3484567
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