Les automates temporisés comme outil de vérification des protocoles de sécurité

Les automates temporisés sont une extension de l'approche de la théorie des automates pour la modélisation des systèmes en temps réel qui introduit le temps dans les automates classiques. Depuis qu'il a été proposé pour la première fois au début des années 90, il est devenu un domaine de recherche important et a été largement étudié tant dans le contexte des langages formels que dans celui de la modélisation et de la vérification des systèmes en temps réel. Les automates temporisés utilisent une modélisation dense du temps, permettant une vérification efficace des modèles de systèmes sensibles au temps dont le bon fonctionnement dépend des propriétés de temporisation. L'un de ces domaines d'application est la vérification des protocoles de sécurité. Ce livre se concentre sur le modèle des automates temporisés et l'utilise comme un outil de vérification des protocoles de sécurité. Comme étude de cas, le protocole d'authentification répétée de Neuman-Stubblebine est modélisé et vérifié en utilisant les propriétés sensibles au temps du modèle. Les défauts du protocole sont analysés et il est commenté sur les avantages et les défis du modèle.