SAPIC - A Stateful Applied Pi Calculus

Sapic is a tool that translates protocols from a high-level protocol description language akin to the applied pi calculus into multiset rewrite rules, that can then be be analysed using the Tamarin Prover. Its aim is the analysis of protocol that include state, for example Hardware Security Tokens communicating with a possibly malicious user, or protocols that rely on databases. It has been succesfully applied on several case studies including the Yubikey authentication protocol.

The code of our prototype along with the examples is available here

Abstract

Security APIs, key servers and protocols that need to keep the status of transactions, require to maintain a global, non-monotonic state, e.g., in the form of a database or register. However, most existing automated verification tools do not support the analysis of such stateful security protocols - sometimes because of fundamental reasons, such as the encoding of the protocol as Horn clauses, which are inherently monotonic. An exception is the recent tamarin prover which allows specifying protocols as multiset rewrite (MSR) rules, a formalism expressive enough to encode state. As multiset rewriting is a "low-level" specification language with no direct support for concurrent message passing, encoding protocols correctly is a difficult and error-prone process.
We propose a process calculus which is a variant of the applied pi calculus with constructs for manipulation of a global state by processes running in parallel. We show that this language can be translated to MSR rules whilst preserving all security properties expressible in a dedicated first-order logic for security properties. The translation has been implemented in a prototype tool which useqs the tamarin prover as a backend. We apply the tool to several case studies among which a simplified fragment of PKCS#11, the Yubikey security token, and an optimistic contract signing protocol.

Examples

Frequently Asked Questions

  1. How does this protocol description language relate to the applied pi calculus?

    Our calculus is a variant of the applied pi calculus. In addition to the usual operators for concurrency, replication, communication and name creation, it offers several constructs for reading and updating an explicit global state. We offer a construct for accessing a global state which is a map from terms (keys) to other terms (values). There is a lookup operator that is able to recognize the absence of a matching key in the store. We have primitives for locking and unlocking. There is a construct that gives access to the underlying multiset rewriting calculus.

  2. Is this translation sound?

    Yes, it is sound, as well as complete. The same holds for the tamarin prover's constraint solving algorithm.

  3. What is the advantage of this transformation? You could just encode the protocol as multiset rewrite rules.

    Technically, this is true: Any protocol that we are able to analyze can be directly analyzed by the tamarin prover as we use it as a backend.
    An important disadvantage is that the representation of protocols as multiset rewrite rules is very low level and far away from actual protocol implementations, making it very difficult to model a protocol correctly. Our calculus is semantically richer, in particular, it gives information on which part of the protocol runs on which party and which kind of requests are treated in which thread, respectively. This kind of information is fundamental in the development of protocols, as well as in the implementation of protocols starting from a protocol description. There has been work on the automated translation from protocol descriptions in the spi calculus (another variant of the applied pi calculus) into Java programs, an approach that appears to be adaptable to our calculus, but not to multiset rewriting. This supports the claim that our calculus contains enough information to serve as a template for an implementation.
    For protocols that are first designed, then analysed for security, and later implemented on the basis of the analysed model, this translation from a model to an implementation needs to be performed, whether it is done automatically or by hand. One way or another, it should be as straightforward as possible.
    For the other direction, where a protocol description exists in one form or another, possibly in form of an implementation, and is to be modelled with the aim of analysing its security, we face similar problems: Encoding private channels, nested replications and locking mechanisms directly as multiset rewrite rules is a tricky and error-prone task. During our experiments with tamarin, we noticed that in particular the last point is often swept under the rug: Protocol steps typically consist of a single input, followed by several database lookups, and finally an output. In multiset rewriting calculi, they are usually modelled as a single rule, and therefore effectively atomic. Real implementations are different from that: Several entities might be involved, database lookups could be slow, etc. In this case, such models could obscure eventual issues in concurrent protocol steps, that would otherwise require, e. g., explicit locking. Ignoring the fact that protocol steps are not atomic in the model increases the risk of implicitly excluding attacks in the model that are well possible in a real implementation, e. g., race conditions.

  4. The protocols you analyse in your case studies have been analysed before, for example using multiset rewrite rules. So what is new?

    The short answer is that we provide a richer modeling not covered by existing work. For instance, in case of the Yubikey protocol, our modelling explicitly permits the authentication server to treat two queries not coming from the same Yubikey at the same time, or in case of PKCS#11, we learn that synchronisation is only necessary for attribute changes, not for the actual operations.
    Is this difference "worth the wait"? In case of the Yubikey, we only confirm an existing result in a stronger model, but given that the previous model is unrealistic (Yubikeys are autonomous and thus will cannot respect a global lock), assurance that the previous model made the "right" simplifications is necessary. In case of the Security API, knowing that a more relaxed synchronisation procedure is actually sufficient can lead to more efficient implementations. It is possible to faithfully model those protocols in tamarin's calculus, but difficult to do so, as the previous modellings of those case studies witness. Simplifications made in the modeling process are often performed ad hoc, which is where we see the need for our translation.

SAPIC*

SAPIC* extends SAPIC by a Kleene star operator (*) which allows to iterate a process a finite but arbitrary number of times. This construction is useful to specify for instance stream authentication protocols. We he used it to analyse a simple version of the TESLA protocol.

You may download the code of the extended tool, as well as the specification of TESLA.

Publications