TA4SP
Vérifier automatiquement les protocoles de sécurité

Avant de décrire plus avant la méthode utilisée dans TA4SP, il faut savoir que si l'on ne borne pas le nombre de sessions d'un protocole pouvant s'exécuter en parallèle, savoir si ce protocole est sensible aux attaques de type man in the middle est indécidable, c'est-à-dire qu'il n'est pas possible de réaliser un programme qui prend en entrée la description d'un protocole de sécurité et qui donne à chaque fois une analyse de ce protocole. Pour revenir à un cas décidable, c'est-à-dire réalisable à tous les coups par une machine, il est nécessaire de faire certaines restrictions ou hypothèses. La plus courante est de borner le nombre de sessions du protocole pouvant s'exécuter en parallèle, généralement à deux ou trois. Cela se justifie a posteriori par le fait que presque toutes les failles connues sur...