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

RÉSUMÉ: 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. ABSTRACT: Analysis of security protocols which exhibit both probabilistic and non-deterministic behavior require an object called scheduler to solve all non-determinism in the model for evaluating probabilistic properties. In the context of analysis of security protocols running into an hostile environment, it's quite natural to consider the scheduler to be under control of the adversary having full control of all the communications network. This assumption gives the adversary an unreasonably strong power of the fact that certain choices result from internal actions which must remain invisible to the attacker. We propose a method for limiting the power of the schedulers based on an observational equivalence relation defined on the actions set of the protocol modeled as Markov decision process (MDP) by defining two levels of scheduling. A (static) internal or cooperative scheduler resolves uniformly the non-determinism over observationally equivalent actions and the remaining non-determinism in the model is resolved by external or adversarial schedulers which model partial capabilities of the adversary during the security analysis of the protocol. We then implement our method in PRISM model checker by using algorithms based on symbolic data structures and by preserving basic functionalities of PRISM. Finally we illustrate our idea by applying the method on David Chaum's dining cryptographers protocol and Michael Rabin's probabilistic contract signing protocol. Keywords: Security protocol, probabilistic system, non-determinism, scheduler, Markov decision process, probabilistic model checking, decision diagram