Vérification des systèmes de sécurité probabilistes : restriction de l'attaquant

L'analyse des protocoles de sécurité présentant un comportement probabiliste et non déterministe nécessite, afin d'évaluer les propriétés probabilistes, l'introduction d'un objet appelé ordonnanceur résolvant tout le non déterminisme existant dans le modèle. La sécurité des protocoles étant évaluée dans un environnement hostile, il est tout naturel que l'ordonnanceur soit considéré sous le contrôle de l'adversaire ayant le contrôle complet de tout le réseau de communications. Cette considération confère généralement une puissance trop forte à l'adversaire du fait que certains choix résultent des actions internes devant rester invisibles à l'adversaire. Nous proposons une méthode de restriction des ordonnanceurs basée sur la relation d'équivalence observationnelle définie sur l'ensemble des actions du protocole modélisé sous-forme de processus de décision markovien (MDP) en définissant deux niveaux d'ordonnancement. L'ordonnanceur interne ou coopératif résout à l'avance le non déterminisme entre les actions observationnellement équivalentes avec une distribution de probabilités uniforme et le reste du non déterminisme dans le modèle est résolu par les ordonnanceurs externes modélisant ceux considérés sous le contrôle de l'attaquant lors de l'analyse du protocole. Nous implémentons ensuite cette méthode dans le model checker PRISM en utilisant des algorithmes basés sur les structures de données symboliques tout en préservant les fonctionnalités initiales de PRISM. Enfin, nous illustrons notre méthode par des études de cas de protocoles de sécurité, le protocole de dîner de cryptographes de David Chaum et le protocole de signature de contrat de Michael Rabin. Mots-clés : Protocole de sécurité, système probabiliste, non déterminisme, ordonnanceur, processus de décision markovien, model checking probabiliste, diagramme de décision.