CertiCrypt swMATH ID: 9443 Software Authors: Barthe, Gilles; Grégoire, Benjamin; Zanella Béguelin, Santiago Description: Programming language techniques for cryptographic proofs. CertiCrypt is a general framework to certify the security of cryptographic primitives in the Coq proof assistant. CertiCrypt adopts the code-based paradigm, in which the statement of security, and the hypotheses under which it is proved, are expressed using probabilistic programs. It provides a set of programming language tools (observational equivalence, relational Hoare logic, semantics-preserving program transformations) to assist in constructing proofs. Earlier publications of CertiCrypt provide an overview of its architecture and main components, and describe its application to signature and encryption schemes. This paper describes programming language techniques that arise specifically in cryptographic proofs. The techniques have been developed to complete a formal proof of IND-CCA security of the OAEP padding scheme. In this paper, we illustrate their usefulness for showing the PRP/PRF Switching Lemma, a fundamental cryptographic result that bounds the probability of an adversary to distinguish a family of pseudorandom functions from a family of pseudorandom permutations. Homepage: http://certicrypt.gforge.inria.fr/ Dependencies: Coq Related Software: Coq; Coq/SSReflect; EasyCrypt; kepler98; seL4 Cited in: 5 Publications Standard Articles 1 Publication describing the Software, including 1 Publication in zbMATH Year Formal certification of code-based cryptographic proofs. Zbl 1315.68081Barthe, Gilles; Grégoire, Benjamin; Zanella Béguelin, Santiago 2009 all top 5 Cited by 8 Authors 4 Barthe, Gilles 4 Zanella Béguelin, Santiago 3 Grégoire, Benjamin 1 Bagnall, Alexander 1 Lakhnech, Yassine 1 Merten, Samuel 1 Olmedo, Federico 1 Stewart, Gordon Cited in 1 Serial 1 Journal of Formalized Reasoning Cited in 4 Fields 4 Information and communication theory, circuits (94-XX) 3 Computer science (68-XX) 1 Mathematical logic and foundations (03-XX) 1 Game theory, economics, finance, and other social and behavioral sciences (91-XX) Citations by Year