research-article

Towards automated proofs for asymmetric encryption schemes in the random oracle model

Authors:

Judicaël Courant,

Marion Daubignard,

Pascal Lafourcade,

Yassine LakhnechAuthors Info & Claims

CCS '08: Proceedings of the 15th ACM conference on Computer and communications security

Pages 371 - 380

https://doi.org/10.1145/1455770.1455817

Published: 27 October 2008 Publication History

Abstract

Chosen-ciphertext security is by now a standard security property for asymmetric encryption. Many generic constructions for building secure cryptosystems from primitives with lower level of security have been proposed. Providing security proofs has also become standard practice. There is, however, a lack of automated verification procedures that analyze such cryptosystems and provide security proofs. This paper presents an automated procedure for analyzing generic asymmetric encryption schemes in the random oracle model. It has been applied to several examples of encryption schemes among which the construction of Bellare-Rogaway 1993, of Pointcheval at PKC'2000 and REACT.

References

[1]

G. Barthe, J. Cederquist, and S. Tarento. A Machine-Checked Formalization of the Generic Model and the Random Oracle Model. In D. Basin and M. Rusinowitch, editors, Proceedings of IJCAR'04, volume 3097 of LNCS, pages 385--399, 2004.

[2]

Gilles Barthe, Bejamin Gregoire, Romain Janvier, and Santiago Zanella Beguelin. A framework for language-based cryptographic proofs. In 2nd Informal ACM SIGPLAN Workshop on Mechanizing Metatheory, Oct 2007.

[3]

Gilles Barthe and Sabrina Tarento. A machine-checked formalization of the random oracle model. In Jean-Christophe Filliatre, Christine Paulin-Mohring, and Benjamin Werner, editors, Proceedings of TYPES'04, volume 3839 of Lecture Notes in Computer Science, pages 33--49. Springer, 2004.

[4]

Mihir Bellare, Anand Desai, David Pointcheval, and Phillip Rogaway. Relations among notions of security for public-key encryption schemes. In CRYPTO '98: Proceedings of the 18th Annual International Cryptology Conference on Advances in Cryptology, pages 26--45, London, UK, 1998. Springer-Verlag.

Digital Library

[5]

Mihir Bellare and Phillip Rogaway. Random oracles are practical: a paradigm for designing efficient protocols. In CCS '93: Proceedings of the 1st ACM conference on Computer and communications security, pages 62--73, New York, USA, November 1993 ACM.

Digital Library

[6]

Mihir Bellare and Phillip Rogaway. Optimal asymmetric encryption. In Alfredo De Santis, editor, EUROCRYPT, volume 950 of Lecture Notes in Computer Science, pages 92--111. Springer, 1994.

[7]

Mihir Bellare and Phillip Rogaway. Code-based game-playing proofs and the security of triple encryption. Cryptology ePrint Archive, Report 2004/331, 2004. http://eprint.iacr.org/.

[8]

Bruno Blanchet. A computationally sound mechanized prover for security protocols. In S&P, pages 140--154. IEEE Computer Society, 2006.

Digital Library

[9]

Bruno Blanchet and David Pointcheval. Automated security proofs with sequences of games. In Cynthia Dwork, editor, CRYPTO, volume 4117 of Lecture Notes in Computer Science, pages 537--554. Springer, 2006.

[10]

Ricardo Corin and Jerry den Hartog. A probabilistic hoare-style logic for game-based cryptographic proofs. In Michele Bugliesi, Bart Preneel, Vladimiro Sassone, and Ingo Wegener, editors, ICALP (2), volume 4052 of Lecture Notes in Computer Science, pages 252--263. Springer, 2006.

[11]

Ivan Damgard. Towards practical public key systems secure against chosen ciphertext attacks. In CRYPTO '91: Proceedings of the 11th Annual International Cryptology Conference on Advances in Cryptology, pages 445--456, London, UK, 1992. Springer-Verlag.

Digital Library

[12]

Anupam Datta, Ante Derek, John C. Mitchell, and Bogdan Warinschi. Computationally sound compositional logic for key exchange protocols. In CSFW, pages 321--334, 2006.

Digital Library

[13]

U. Feige, A. Fiat, and A. Shamir. Zero-knowledge proofs of identity. J. Cryptol., 1(2):77--94, 1988.

Digital Library

[14]

Eiichiro Fujisaki and Tatsuaki Okamoto. How to enhance the security of public-key encryption at minimum cost. In PKC '99: Proceedings of the Second International Workshop on Practice and Theory in Public Key Cryptography, pages 53--68, London, UK, 1999. Springer-Verlag.

Digital Library

[15]

Shai Halevi. A plausible approach to computer-aided cryptographic proofs. http://theory.lcs.mit.edu/ shaih/pubs.html, 2005.

[16]

David Nowak. A framework for game-based security proofs. In ICICS, pages 319--333, 2007.

Digital Library

[17]

Tatsuaki Okamoto and David Pointcheval. React: Rapid enhanced-security asymmetric cryptosystem transform. In CT-RSA 2001: Proceedings of the 2001 Conference on Topics in Cryptology, pages 159--175, London, UK, 2001. Springer-Verlag.

Digital Library

[18]

David Pointcheval. Chosen-ciphertext security for any one-way cryptosystem. In PKC '00: Proceedings of the Third International Workshop on Practice and Theory in Public Key Cryptography, pages 129--146, London, UK, 2000. Springer-Verlag.

Digital Library

[19]

Victor Shoup. Oaep reconsidered. J. Cryptology, 15(4):223--249, 2002.

Digital Library

[20]

Victor Shoup. Sequences of games: a tool for taming complexity in security proofs, 2004. http://eprint.iacr.org/2004/332.

[21]

David Soldera, Jennifer Seberry, and Chengxin Qu. The analysis of zheng-seberry scheme. In Lynn Margaret Batten and Jennifer Seberry, editors, ACISP, volume 2384 of Lecture Notes in Computer Science, pages 159--168. Springer, 2002.

Digital Library

[22]

Sabrina Tarento. Machine-checked security proofs of cryptographic signature schemes. In Sabrina De Capitani di Vimercati, Paul F. Syverson, and Dieter Gollmann, editors, Computer Security -- ESORICS 2005, volume 3679 of Lecture Notes in Computer Science, pages 140--158. Springer, 2005.

Digital Library

[23]

Yuliang Zheng and Jennifer Seberry. Immunizing public key cryptosystems against chosen ciphertext attacks. IEEE Journal on Selected Areas in Communications, 11(5):715--724, 1993.

Digital Library

Cited By

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
Rakotonirina IAmbrona MAguirre ABarthe GSuga YSakurai KDing XSako K(2022)Symbolic Synthesis of Indifferentiability AttacksProceedings of the 2022 ACM on Asia Conference on Computer and Communications Security10.1145/3488932.3497759(667-681)Online publication date: 30-May-2022
https://dl.acm.org/doi/10.1145/3488932.3497759
Barthe GFan XGancher JGrégoire BJacomme CShi ELie DMannan MBackes MWang X(2018)Symbolic Proofs for Lattice-Based CryptographyProceedings of the 2018 ACM SIGSAC Conference on Computer and Communications Security10.1145/3243734.3243825(538-555)Online publication date: 15-Oct-2018
https://dl.acm.org/doi/10.1145/3243734.3243825
Show More Cited By

Index Terms

Towards automated proofs for asymmetric encryption schemes in the random oracle model
1. Security and privacy
  1. Cryptography
    1. Public key (asymmetric) techniques
      1. Public key encryption
2. Theory of computation
  1. Semantics and reasoning
    1. Program reasoning
      1. Pre- and post-conditions

Recommendations

Improved convertible authenticated encryption scheme with provable security

Convertible authenticated encryption (CAE) schemes allow a signer to produce an authenticated ciphertext such that only a designated recipient can decrypt it and verify the recovered signature. The conversion property further enables the designated ...
Automated Proofs for Asymmetric Encryption

Many generic constructions for building secure cryptosystems from primitives with lower level of security have been proposed. Providing security proofs has also become standard practice. There is, however, a lack of automated verification procedures ...
A Provably Secure Proxy Signature Scheme in Certificateless Cryptography

A proxy signature scheme enables an original signer to delegate its signing capability to a proxy signer and then the proxy signer can sign a message on behalf of the original signer. Recently, in order to eliminate the use of certificates in certified ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

CCS '08: Proceedings of the 15th ACM conference on Computer and communications security

October 2008

590 pages

ISBN:9781595938107

DOI:10.1145/1455770

General Chair:
Peng Ning
North Carolina State University, USA
,
Program Chairs:
Paul Syverson
Naval Research Laboratory, USA
,
Somesh Jha
University of Wisconsin, USA

Copyright © 2008 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

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 27 October 2008

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article

Conference

CCS08

Sponsor:

CCS08: 15th ACM Conference on Computer and Communications Security 2008

October 27 - 31, 2008

Virginia, Alexandria, USA

Acceptance Rates

CCS '08 Paper Acceptance Rate 51 of 280 submissions, 18%;

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

29
Total Citations
View Citations
497
Total Downloads

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

Reflects downloads up to 26 Sep 2024

Other Metrics

View Author Metrics

Citations

Cited By

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
Rakotonirina IAmbrona MAguirre ABarthe GSuga YSakurai KDing XSako K(2022)Symbolic Synthesis of Indifferentiability AttacksProceedings of the 2022 ACM on Asia Conference on Computer and Communications Security10.1145/3488932.3497759(667-681)Online publication date: 30-May-2022
https://dl.acm.org/doi/10.1145/3488932.3497759
Barthe GFan XGancher JGrégoire BJacomme CShi ELie DMannan MBackes MWang X(2018)Symbolic Proofs for Lattice-Based CryptographyProceedings of the 2018 ACM SIGSAC Conference on Computer and Communications Security10.1145/3243734.3243825(538-555)Online publication date: 15-Oct-2018
https://dl.acm.org/doi/10.1145/3243734.3243825
Gagné MLafourcade PLakhnech YSafavi-Naini R(2016)Automated Proofs of Block Cipher Modes of OperationJournal of Automated Reasoning10.1007/s10817-015-9341-556:1(49-94)Online publication date: 1-Jan-2016
https://dl.acm.org/doi/10.1007/s10817-015-9341-5
Barthe GGrégoire BSchmidt BRay ILi NKruegel C(2015)Automated Proofs of Pairing-Based CryptographyProceedings of the 22nd ACM SIGSAC Conference on Computer and Communications Security10.1145/2810103.2813697(1156-1168)Online publication date: 12-Oct-2015
https://dl.acm.org/doi/10.1145/2810103.2813697
Nowak DZhang Y(2015)Formal security proofs with minimal fussInformation and Computation10.1016/j.ic.2014.10.008241:C(96-113)Online publication date: 1-Apr-2015
https://dl.acm.org/doi/10.1016/j.ic.2014.10.008
Malozemoff AKatz JGreen M(2014)Automated Analysis and Synthesis of Block-Cipher Modes of OperationProceedings of the 2014 IEEE 27th Computer Security Foundations Symposium10.1109/CSF.2014.18(140-152)Online publication date: 19-Jul-2014
https://dl.acm.org/doi/10.1109/CSF.2014.18
Barthe GCrespo JGrégoire BKunz CLakhnech YSchmidt BZanella-Béguelin SSadeghi AGligor VYung M(2013)Fully automated analysis of padding-based encryption in the computational modelProceedings of the 2013 ACM SIGSAC conference on Computer & communications security10.1145/2508859.2516663(1247-1260)Online publication date: 4-Nov-2013
https://dl.acm.org/doi/10.1145/2508859.2516663
Gagné MLafourcade PLakhnech Y(2013)Automated Security Proofs for Almost-Universal Hash for MAC VerificationComputer Security – ESORICS 201310.1007/978-3-642-40203-6_17(291-308)Online publication date: 2013
https://doi.org/10.1007/978-3-642-40203-6_17
Barthe GPointcheval DZanella Béguelin SYu TDanezis GGligor V(2012)Verified security of redundancy-free encryption from Rabin and RSAProceedings of the 2012 ACM conference on Computer and communications security10.1145/2382196.2382272(724-735)Online publication date: 16-Oct-2012
https://dl.acm.org/doi/10.1145/2382196.2382272
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