Résumé:
Cet exposé se compose de deux parties:
1) Assistants à la demonstration: théorie et pratique.
Dans cette première
partie, je présenterais différentes pistes pour réduire l'écart entre preuves
formelles et preuves informelles. Théorie: en utilisant de la déduction modulo
réécriture. Pratique: comment implémenter la déduction modulo dans Coq ?
Comment améliorer l'ergonomie de Coq ?
2) Sécurité: certification de protocoles cryptographiques pour le commerce
électronique.
Dans cette seconde partie, je présenterais un résultat de
confidentialité indépendant d'un protocole donné et son application à
différents protocoles d'authentification et un protocole pour le commerce
électronique. Tous ces résultats ont été démontrés dans Isabelle et constituent
une bibliothèque
de théorèmes applicables à d'autres protocoles.
Retour au sommaire / Back to schedule