EasyPQC: Verifying Post-Quantum Cryptography

Manuel Barbosa; Gilles Barthe; Xiong Fan; Benjamin Grégoire; Shih Han Hung; Jonathan Katz; Pierre Yves Strub; Xiaodi Wu; Li Zhou

doi:10.1145/3460120.3484567

EasyPQC: Verifying Post-Quantum Cryptography

Manuel Barbosa
, Gilles Barthe
, Xiong Fan
, Benjamin Grégoire
, Shih Han Hung
, Jonathan Katz
, Pierre Yves Strub
, Xiaodi Wu
, Li Zhou

École Polytechnique

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

Abstract

EasyCrypt is a formal verification tool used extensively for formalizing concrete security proofs of cryptographic constructions. However, the EasyCrypt formal logics consider only classical at- tackers, which means that post-quantum security proofs cannot be formalized and machine-checked with this tool. In this paper we prove that a natural extension of the EasyCrypt core logics permits capturing a wide class of post-quantum cryptography proofs, settling a question raised by (Unruh, POPL 2019). Leveraging our positive result, we implement EasyPQC, an extension of EasyCrypt for post-quantum security proofs, and use EasyPQC to verify post- quantum security of three classic constructions: PRF-based MAC, Full Domain Hash and GPV08 identity-based encryption.

Original language	English
Title of host publication	CCS 2021 - Proceedings of the 2021 ACM SIGSAC Conference on Computer and Communications Security
Publisher	Association for Computing Machinery
Pages	2564-2586
Number of pages	23
ISBN (Electronic)	9781450384544
DOIs	https://doi.org/10.1145/3460120.3484567
Publication status	Published - 13 Nov 2021
Event	27th ACM Annual Conference on Computer and Communication Security, CCS 2021 - Virtual, Online, Korea, Republic of Duration: 15 Nov 2021 → 19 Nov 2021

Publication series

Name	Proceedings of the ACM Conference on Computer and Communications Security
ISSN (Print)	1543-7221

Conference

Conference	27th ACM Annual Conference on Computer and Communication Security, CCS 2021
Country/Territory	Korea, Republic of
City	Virtual, Online
Period	15/11/21 → 19/11/21

Keywords

formal verification
post-quantum cryptography

Access to Document

10.1145/3460120.3484567

Cite this

Barbosa, M., Barthe, G., Fan, X., Grégoire, B., Hung, S. H., Katz, J., Strub, P. Y., Wu, X., & Zhou, L. (2021). EasyPQC: Verifying Post-Quantum Cryptography. In CCS 2021 - Proceedings of the 2021 ACM SIGSAC Conference on Computer and Communications Security (pp. 2564-2586). (Proceedings of the ACM Conference on Computer and Communications Security). Association for Computing Machinery. https://doi.org/10.1145/3460120.3484567

@inproceedings{62551ab71d864953864b39373792446d,

title = "EasyPQC: Verifying Post-Quantum Cryptography",

abstract = "EasyCrypt is a formal verification tool used extensively for formalizing concrete security proofs of cryptographic constructions. However, the EasyCrypt formal logics consider only classical at- tackers, which means that post-quantum security proofs cannot be formalized and machine-checked with this tool. In this paper we prove that a natural extension of the EasyCrypt core logics permits capturing a wide class of post-quantum cryptography proofs, settling a question raised by (Unruh, POPL 2019). Leveraging our positive result, we implement EasyPQC, an extension of EasyCrypt for post-quantum security proofs, and use EasyPQC to verify post- quantum security of three classic constructions: PRF-based MAC, Full Domain Hash and GPV08 identity-based encryption.",

keywords = "formal verification, post-quantum cryptography",

author = "Manuel Barbosa and Gilles Barthe and Xiong Fan and Benjamin Gr{\'e}goire and Hung, \{Shih Han\} and Jonathan Katz and Strub, \{Pierre Yves\} and Xiaodi Wu and Li Zhou",

note = "Publisher Copyright: {\textcopyright} 2021 ACM.; 27th ACM Annual Conference on Computer and Communication Security, CCS 2021 ; Conference date: 15-11-2021 Through 19-11-2021",

year = "2021",

month = nov,

day = "13",

doi = "10.1145/3460120.3484567",

language = "English",

series = "Proceedings of the ACM Conference on Computer and Communications Security",

publisher = "Association for Computing Machinery",

pages = "2564--2586",

booktitle = "CCS 2021 - Proceedings of the 2021 ACM SIGSAC Conference on Computer and Communications Security",

}

Barbosa, M, Barthe, G, Fan, X, Grégoire, B, Hung, SH, Katz, J, Strub, PY, Wu, X & Zhou, L 2021, EasyPQC: Verifying Post-Quantum Cryptography. in CCS 2021 - Proceedings of the 2021 ACM SIGSAC Conference on Computer and Communications Security. Proceedings of the ACM Conference on Computer and Communications Security, Association for Computing Machinery, pp. 2564-2586, 27th ACM Annual Conference on Computer and Communication Security, CCS 2021, Virtual, Online, Korea, Republic of, 15/11/21. https://doi.org/10.1145/3460120.3484567

EasyPQC: Verifying Post-Quantum Cryptography. / Barbosa, Manuel; Barthe, Gilles; Fan, Xiong et al.
CCS 2021 - Proceedings of the 2021 ACM SIGSAC Conference on Computer and Communications Security. Association for Computing Machinery, 2021. p. 2564-2586 (Proceedings of the ACM Conference on Computer and Communications Security).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

TY - GEN

T1 - EasyPQC

T2 - 27th ACM Annual Conference on Computer and Communication Security, CCS 2021

AU - Barbosa, Manuel

AU - Barthe, Gilles

AU - Fan, Xiong

AU - Grégoire, Benjamin

AU - Hung, Shih Han

AU - Katz, Jonathan

AU - Strub, Pierre Yves

AU - Wu, Xiaodi

AU - Zhou, Li

PY - 2021/11/13

Y1 - 2021/11/13

N2 - EasyCrypt is a formal verification tool used extensively for formalizing concrete security proofs of cryptographic constructions. However, the EasyCrypt formal logics consider only classical at- tackers, which means that post-quantum security proofs cannot be formalized and machine-checked with this tool. In this paper we prove that a natural extension of the EasyCrypt core logics permits capturing a wide class of post-quantum cryptography proofs, settling a question raised by (Unruh, POPL 2019). Leveraging our positive result, we implement EasyPQC, an extension of EasyCrypt for post-quantum security proofs, and use EasyPQC to verify post- quantum security of three classic constructions: PRF-based MAC, Full Domain Hash and GPV08 identity-based encryption.

AB - EasyCrypt is a formal verification tool used extensively for formalizing concrete security proofs of cryptographic constructions. However, the EasyCrypt formal logics consider only classical at- tackers, which means that post-quantum security proofs cannot be formalized and machine-checked with this tool. In this paper we prove that a natural extension of the EasyCrypt core logics permits capturing a wide class of post-quantum cryptography proofs, settling a question raised by (Unruh, POPL 2019). Leveraging our positive result, we implement EasyPQC, an extension of EasyCrypt for post-quantum security proofs, and use EasyPQC to verify post- quantum security of three classic constructions: PRF-based MAC, Full Domain Hash and GPV08 identity-based encryption.

KW - formal verification

KW - post-quantum cryptography

UR - https://www.scopus.com/pages/publications/85119366017

U2 - 10.1145/3460120.3484567

DO - 10.1145/3460120.3484567

M3 - Conference contribution

AN - SCOPUS:85119366017

T3 - Proceedings of the ACM Conference on Computer and Communications Security

SP - 2564

EP - 2586

BT - CCS 2021 - Proceedings of the 2021 ACM SIGSAC Conference on Computer and Communications Security

PB - Association for Computing Machinery

Y2 - 15 November 2021 through 19 November 2021

ER -

Barbosa M, Barthe G, Fan X, Grégoire B, Hung SH, Katz J et al. EasyPQC: Verifying Post-Quantum Cryptography. In CCS 2021 - Proceedings of the 2021 ACM SIGSAC Conference on Computer and Communications Security. Association for Computing Machinery. 2021. p. 2564-2586. (Proceedings of the ACM Conference on Computer and Communications Security). doi: 10.1145/3460120.3484567

EasyPQC: Verifying Post-Quantum Cryptography

Abstract

Publication series

Conference

Keywords

Access to Document

Other files and links

Fingerprint

Cite this