
Evènement pour le groupe Modélisation et Verification
Date  20130425 11:3012:30 
Titre  Automatic security proof of cryptographic primitives: public encryption, symmetric encryption modes, MAC 
Résumé  Our aim is to develop a formal method in order to prove cryptographic primitives. We consider cryptographic primitives as small programs, usually it is just few lines of code. In the last century Tony Hoare provided mechanisms in order to prove that a program is correct, socalled Hoare logic.
Our approach consists in the three following steps:
Modeling properties that studied primitives have to ensure by proposing some invariants.
Defining the language which represent the small set of commands used to construct a primitives at the good abstract level.
Proving Logics rules, that allows us to generate and propagate invariants according to the commands executed in the program.
Once the language fixed, the invariants developed and the rules of the Hoare Logic established, we can verify a primitive. Using this approach we have developed three logics to prove security of several public encryption schemes, symmetric encryption modes and also several MAC. 
Lieu  076 
Orateur  Pascal Lafourcade 
Email  Pascal.Lafourcade@imag.fr 
Url  VERIMAG 
Aucun document lié à cet événement. RetourRetour à l'index
 