Symbolic Methods in Computational Cryptography Proofs

Gilles Barthe, Benjamin Grégoire, Charlie Jacomme, Steve Kremer, and Pierre-Yves Strub. Symbolic Methods in Computational Cryptography Proofs. In Proceedings of the 32nd IEEE Computer Security Foundations Symposium (CSF'19), pp. 136–151, IEEE Computer Society Press, Hoboken, NJ, USA, June 2019.
doi:10.1109/CSF.2019.00017

Download

[PDF] [PDF (long version)] [HTML] 

Abstract

Code-based game-playing is a popular methodology for proving security of cryptographic constructions and side-channel countermeasures. This methodology relies on treating cryptographic proofs as an instance of relational program verification (between probabilistic programs), and decomposing the latter into a series of elementary relational program verification steps. In this paper, we develop principled methods for proving such elementary steps for probabilistic programs that operate over finite fields and related algebraic structures. We focus on three essential properties: program equivalence, information flow, and uniformity. We give characterizations of these properties based on deducibility and other notions from symbolic cryptography. We use (sometimes improve) tools from symbolic cryptography to obtain decision procedures or sound proof methods for program equivalence, information flow, and uniformity. Finally, we evaluate our approach using examples drawn from provable security and from side-channel analysis - for the latter, we focus on the masking countermeasure against differential power analysis. A partial implementation of our approach is integrated in EasyCrypt, a proof assistant for provable security, and in MaskVerif, a fully automated prover for masked implementations.

BibTeX

@inproceedings{BGJKS-csf19,
  abstract =	 {Code-based game-playing is a popular methodology for
                  proving security of cryptographic constructions and
                  side-channel countermeasures. This methodology
                  relies on treating cryptographic proofs as an
                  instance of relational program verification (between
                  probabilistic programs), and decomposing the latter
                  into a series of elementary relational program
                  verification steps. In this paper, we develop
                  principled methods for proving such elementary steps
                  for probabilistic programs that operate over finite
                  fields and related algebraic structures. We focus on
                  three essential properties: program equivalence,
                  information flow, and uniformity. We give
                  characterizations of these properties based on
                  deducibility and other notions from symbolic
                  cryptography. We use (sometimes improve) tools from
                  symbolic cryptography to obtain decision procedures
                  or sound proof methods for program equivalence,
                  information flow, and uniformity. Finally, we
                  evaluate our approach using examples drawn from
                  provable security and from side-channel analysis -
                  for the latter, we focus on the masking
                  countermeasure against differential power
                  analysis. A partial implementation of our approach
                  is integrated in EasyCrypt, a proof assistant for
                  provable security, and in MaskVerif, a fully
                  automated prover for masked implementations.  },
  address =	 {Hoboken, NJ, USA},
  author =	 {Barthe, Gilles and Gr{\'e}goire, Benjamin and
                  Jacomme, Charlie and Kremer, Steve and Strub,
                  Pierre-Yves },
  booktitle =	 {{P}roceedings of the 32nd IEEE Computer Security
                  Foundations Symposium (CSF'19)},
  month =	 jun,
  pages =	 {136--151},
  publisher =	 {{IEEE} Computer Society Press},
  title =	 {Symbolic Methods in Computational Cryptography
                  Proofs},
  year =	 2019,
  acronym =	 {{CSF}'19},
  nmonth =	 6,
  doi =		 {10.1109/CSF.2019.00017},
  url =		 {https://ieeexplore.ieee.org/document/8823706},
                  ={https://ieeexplore.ieee.org/stamp/stamp.jsp?tp=&arnumber=8823706},
}