|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|
|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, 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. |
|Orateur||Pascal Lafourcade |
Aucun document lié à cet événement.RetourRetour à l'index