Evènement pour le groupe Modélisation et Verification

Date 2013-04-25  11:30-12:30
TitreAutomatic 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, so-called 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. 
OrateurPascal Lafourcade 

Aucun document lié à cet événement.

Retour à l'index