FICHE MODULE SI5 / M2 ISI

TITRE : Vérification et sécurité


DUREE  : 8 semaines (évaluation comprise)

RESPONSABLE  : Benjamin Grégoire
QUALITE/CV : Benjamin Grégoire est chercheur INRIA dans le projet EVEREST à Sophia Antipolis. Il travaille depuis 2002 sur la compilation et les assistants de preuve et applique ses travaux aux programmes certifiés. Il est l'auteur de plus de douze articles.

AUTRES INTERVENANTS ACADEMIQUES : Tamara Rezk

OBJECTIFS : Former le étudiants à la sécurité prouvée dans le modèle de Dolev-Yao et les initier aux applications comme les programmes certifiés (proof-carying code).

CONTENU: 

  1. Introduction générale aux assistants de preuve
  2. Vérification automatique de protocoles cryptographiques: modèle de Dolev-Yao
  3. Correction du modèle de Dolev-Yao vis-à-vis du modèle calculatoire
  4. Preuves cryptographiques par les jeux
  5. Fundamental lemma and coins fixing
  6. Logique relationnelle probabiliste
  7. Mise en application : preuve de OAEP

PREREQUIS :

BIBLIOGRAPHIE :

  1. V. Shoup. Sequences of games: a tool for taming complexity in security proofs. Cryptology ePrint Archive, Report 2004/332. November 2004. [.pdf <http://eprint.iacr.org/2004/332.pdf>]
  2. M. Bellare and P. Rogaway. The security of triple encryption and a framework for code-based game-playing proofs. /Advances in Cryptology/ Eurocrypt 2006, LNCS 4004, Springer, pp. 409-426, 2006. [.pdf <http://eprint.iacr.org/2004/331.pdf>]
  3. S. Halevi. A plausible approach to computer-aided cryptographic proofs. Cryptology ePrint Archive, Report 2005/181. June 2005. [.pdf <http://eprint.iacr.org/2005/181.pdf>]

SUPPORT de COURS :

 

Site Web du Cours

Polycopié du cours

Copie des transparents

Support de cours

 X

 

 X

 

MODE D’EVALUATION :

 

Présentation Orale

Ecrit en temps limtié

Livraison sur Site Web

Production Logicielle

 

 

 

Rédaction d’un mémoire

 

 

 

Examen

 X

 

 

AUTRES INFORMATIONS :

PARCOURS

Sans intérêt

Peu d’intérêt

Beaucoup d’intérêt

Indispensable

SSR : Système, Sécurité et Réseaux

 

 

 X

 

CID : Connaissance, Information, Décision

 X

 

 

 

IAM : Informatique Ambiante et Mobile

 

 X

 

 
VIM : Vision, Image et Multimédia  X      
Ambiant Computing, Grid Computing and Network Computing    X    
Business Management and Information technology        
Système d’information        
Intéraction homme-machines        

Les quatre premiers parcours correspondent à des spécialités habilitées, les quatres suivant correspondent à un affichage interne et à une possibilité de suivre cet ensemble de cours.