Title
A Probabilistic Applied Pi-calculus


Abstract

Angelo Troina

Università di Torino, Italy

We propose an extension of the Applied Pi-calculus by introducing nondeterministic and probabilistic choice operators. The semantics of the resulting model, in which probability and nondeterminism are combined, is given by Segala's Probabilistic Automata driven by schedulers which resolve the nondeterministic choice among the probability distributions over target states. Notions of static and observational equivalence are given for the enriched calculus. In order to model the possible interaction of a process with its surrounding environment a labeled semantics is given together with a notion of weak bisimulation which is shown to coincide with the observational equivalence. The use of an equational theory, inherited from the Applied Pi-Calculus, allows to naturally model cryptographic primitives, and to apply the framework in the context of security protocol analysis. A study of the 1-out-of-2 oblivious transfer protocol is given. Finally, we prove that results in the probabilistic framework are preserved in a purely nondeterministic setting.

(joint work with Jean Goubault-Larrecq and Catuscia Palamidessi)