Verification des systemes de securite probabilistes: Restriction de l'attaquant

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 a 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 pre- serving 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.