Towards automating code-based game-based cryptographic proofs
Gilles Barthe, Benjamin Grégoire, Daniel S. Hedin, Sylvain Heraud, Santiago Zanella · 2010
CertiCrypt [1] is a general framework built on top on the Coq proof assistant to certify the security of cryptographic primitives. It has been used to verify the exact security of encryption schemes such as OAEP and signature schemes such as FDH. CertiCrypt adopts the code-based game-based paradigm of Bellare and Rogaway, in which the security statement, and the hypotheses under which it is proved, are expressed using probabilistic programs. Consequently, many proof steps involve establishing observational equivalence between two programs, or a relational Hoare statement. At present these statements are established formally using an equational theory for observational equivalence or a relational Hoare logic. The talk will report on using standard verification methods (generating verification conditions and sending them to an automatic tool) for establishing these statements automatically. The long-term goal of this work is to increase the automation of CertiCrypt, to the point that the user can submit a proof sketch of a code-based game-based cryptographic proof, consisting of a sequence of games, and relational invariants, and that CertiCrypt can automatically complete the proof sketch.