Campus Event Calendar
Event Entry
New for: D2, D3
What and Who
Automated Construction of Machine-Checked Cryptographic Proofs
Santiago Zanella Béguelin
IMDEA Software Institute, Madrid
SWS Colloquium
Santiago Zanella Béguelin obtained his degree in Computer Science from
Universidad Nacional de Rosario, Argentina in 2006, and his
Ph.D. under the supervision of Gilles Barthe on the formal
certification of game-based cryptographic proofs from Ecole Nationale
Supérieure des Mines de Paris in 2010. He is currently a Postdoctoral
Research Fellow at the IMDEA Software Institute, Madrid, Spain
AG 1, AG 2, AG 3, AG 4, AG 5, SWS, RG1, MMCI
Expert Audience
English
Note: We use this to send email in the morning.
Date, Time and Location
Tuesday, 15 March 2011
14:00
60 Minutes
E1 4
024
Saarbrücken
Abstract
The game-based approach is an established methodology for structuring
security proofs of cryptographic schemes. Its essence lies in giving
precise mathematical descriptions of the interaction between an
adversary and an oracle system---such descriptions are referred to as
games---and to organize proofs as sequences of games, starting from a
game that represents a security goal, and proceeding by successive
transformations to games that represent security
assumptions. Game-based proofs can be rigorously formalized by
representing games as probabilistic programs and relying on
programming language techniques to justify proof steps. In this talk I
will describe two tools that follow this approach: CertiCrypt and
EasyCrypt.
* CertiCrypt is built upon the general-purpose proof assistant Coq and
provides certified mechanisms to reason about probabilistic
programs, including a relational Hoare logic, a theory of
observational equivalence, verified program transformations, and
ad-hoc techniques, such as reasoning about failure
events. CertiCrypt has been notably applied to verify security
proofs of OAEP and FDH.
* EasyCrypt is an automated tool written in OCaml that builds upon SMT
solvers to synthesize machine-checked proofs from proof sketches,
which include the full sequence of games, relational logic judgments
and claims relating the probability of events in successive
games. Relational judgments are proved using a verification
condition generator that yields proof obligations that can be
discharged by SMT solvers. To verify claims about probability, we
implement a mechanism that combines some elementary rules to
directly compute bounds on the probability of events with rules to
derive probability (in)equalities from relational judgments. Most
components of EasyCrypt are proof-producing, so that proofs built by
EasyCrypt can be exported to CertiCrypt and verified using Coq,
assuming proof obligations discharged by SMT solvers are
valid. EasyCrypt has been notably used to verify the security of the
Cramer-Shoup cryptosystem.
If time permits, the talk will feature a demo of the use of EasyCrypt
to build a proof, export it to CertiCrypt and verify it using Coq.
Contact
Brigitta Hansen
0681 - 9325691
--email hidden
passcode not visible
logged in users only
Brigitta Hansen, 03/11/2011 11:11 -- Created document.