CTL
8 juin 2010 - 15h00
Equivalence de trace pour les processus cryptographiques
par Yannick Chevalier de IRIT équipe LILAC
Résumé : L'étude de propriétés fines des protocoles cryptographiques, telles que
l'anonymat ou la non-répudiation, demande la vérification d'une propriété
d'équivalence observationnelle entre deux instances d'un protocole ou
entre deux protocoles différents. Pour les processus finis, cette propriété
se ramène à l'étude de l'équivalence des traces de deux processus pour
un observateur. Lorsque l'intrus ne peut pas intervenir dans les échanges
de messages entre participants honnêtes, cette équivalence est appelée
équivalence statique, et a été amplement étudiée. Je présenterai une
procédure décidant l'équivalence observationnelle des traces de deux
processus cryptographiques lorsque l'intrus peut intervenir durant la
phase de communication entre participants honnêtes.
CHANGEMENT D'HORAIRE
