L2.5 SAFECAST : Spécification du système global - Intégration des services de sécurité au protocole de gestion de clés -

L'objectif de ce document est specifier l'architecture de securite utilisee dans SAFECAST integrant a la fois les differents services de securite et la distribution de cles afin de pouvoir verifier les protocoles utilises par des outils de verification automatiques. Il s'agit de protocoles de gestion de cles dans des PMRs se basant sur des certificats. Dans le chapitre 5, nous definissons ces protocoles dans une specification assez generale afin qu'elle puisse etre utilisee pour la verification dans divers outils offrant differentes techniques. Dans le chapitre 6, nous proposons une description de ce protocole dans le langage de specification de haut niveau HLPS (High Level Protocol Specification Language) afin d'utiliser l'outil de verification AVSIPA. Dans le chapitre 7, nous proposons une description de ces protocoles dans le langage de specification UML (Unified Modeling Language) 2.0 afin d'utiliser l'outil de verification TURTLE.