Work Package 1 - Obtaining symbolic guarantees.
Sapic+: protocol verifiers of the world, unite!
Symbolic security protocol verifiers have reached a high degree of automation and maturity. Today, experts can model real-world protocols, but this often requirqes model-specific encodings and deep insight into the strengths and weaknesses of each of those tools. Sapic+ is a protocol verification platform, designed by Cheval, Jacomme, Kremer and Künnemann, that lifts this burden and permits choosing the right tool for the job, at any development stage. It provides automated translations from Sapic+ to Tamarin, ProVerif and DeepSec. We prove each part of these translations sound. A user can thus, with a single Sapic+ file, verify reachability and equivalence properties on the specified protocol, either using ProVerif, Tamarin or DeepSec. Moreover, the soundness of the translation allows to directly assume results proven by another tool which allows to exploit the respective strengths of each tool. We demonstrate our approach by analyzing various existing models. This includes, among others, a large case study of the 5G authentication protocols, previously analyzed in Tamarin. Encoding this model in Sapic+ we demonstrate the effectiveness of our approach. The Sapic+ platform is completely integrated in, and distributed with the open source Tamarin prover [https://tamarin-prover.github.io/].
Symbolic protocol verification generally abstracts probabilities away, considering computations that succeed only with negligible probability, such as guessing random numbers or breaking an encryption scheme, as impossible. This abstraction, sometimes referred to as the perfect cryptography assumption, has shown very useful as it simplifies automation of the analysis. However, probabilities may also appear in the control flow where they are generally not negligible. In this paper we consider a framework for symbolic protocol analysis with a probabilistic choice operator: the probabilistic applied pi calculus. We define and explore the relationships between several behavioral equivalences. In particular we show the need to require randomized schedulers – indeed we exhibit a counter-example to one of the main results in a previous work that relied on non-randomized ones. As in other frameworks that mix both non-deterministic and probabilistic choices, schedulers may sometimes be unrealistically powerful. We therefore consider two subclasses of processes that avoid this problem. When considering purely non-deterministic protocols, as is done in classical symbolic verification, we show that a probabilistic adversary has—maybe surprisingly—a strictly superior distinguishing power for may testing, which, when the number of sessions is bounded, we show to coincide with purely possibilistic similarity.
Finally, we consider fully probabilistic protocols and show that trace equivalence corresponds to a notion of may testing with purely probabilistic attackers. We also briefly discuss complexity and automation for these subclasses when the number of sessions is bounded.