EasyPQC: Verifying Post-Quantum Cryptography

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

Others:: Instituto de Engenharia de Sistemas e Computadores (INESC); Faculdade de Ciências da Universidade do Porto (FCUP) ; Universidade do Porto = University of Porto; Max Planck Institute for Security and Privacy [Bochum] (MPI Security and Privacy); Algorand Foundation; Sûreté du logiciel et Preuves Mathématiques Formalisées (STAMP) ; Inria Sophia Antipolis - Méditerranée (CRISAM) ; Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria); University of Texas at Austin [Austin]; Department of Electrical and Computer Engineering [Univ. of Maryland] (ECE - University of Maryland); Département d'informatique de l'École polytechnique (X-DEP-INFO) ; École polytechnique (X)

Description

EasyCrypt is a formal verification tool used extensively for formalizing concrete security proofs of cryptographic constructions. However, the EasyCrypt formal logics consider only classical attackers, 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 postquantum security of three classic constructions: PRF-based MAC, Full Domain Hash and GPV08 identity-based encryption.

Abstract

International audience

EasyPQC: Verifying Post-Quantum Cryptography

Description

Abstract

Additional details