Actualités
  Période
semaine
ou mois
aucune période


  Thèmes:
Thèses
Colloques
Autres
Groupes
Tous les thèmes

   
  Liens:
Voir les thèses

Voir les colloques

Voir les autres événements

Voir la page des groupes

Accéder à l'intranet

Intitulé:   
Automatic security proof of cryptographic primitives: public encryption, symmetric encryption modes, MAC
du 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. 
Lieu076 
OrateurPascal Lafourcade 
EmailPascal.Lafourcade@imag.fr 
UrlVERIMAG 



Aucun document lié à cet événement.

Retour
Retour à l'index