Lienabilité des e-passports

Cette séance de cours porte sur la rupture de l'indissociabilité de la norme de l'OACI 9303 pour les e-passports en utilisant la bisimilarity. Il commence par une introduction aux règles de calcul 7 et de réduction, suivie par la modélisation de BAC avec le calcul # et les implications de la vérification MAC. La séance de cours explore ensuite l'indissociabilité du BAC en utilisant l'équivalence des programmes de calcul T, l'équivalence des traces et des exemples illustrant l'équivalence des traces. Il s'inscrit dans l'indissociabilité du BAC en termes d'équivalence des traces et discute d'une attaque contre la mise en œuvre du Royaume-Uni. La conclusion souligne l'utilisation du calcul T pour la modélisation des protocoles cryptographiques et l'officialisation des propriétés de sécurité, en mettant l'accent sur les vulnérabilités des e-Passports à diverses attaques et la nécessité de nouveaux protocoles.