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
The code of our prototype along with the examples is available here
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.
Frequently Asked Questions
- 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.
- Is this translation sound?
Yes, it is sound, as well as complete. The same holds for the
tamarin prover's constraint solving algorithm.
- 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.
- 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* 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
You may download the code of the extended tool,
as well as the specification of TESLA.
- Steve Kremer and Robert Künnemann. Automated Analysis of Security Protocols with Global State. In Proceedings of the 35th IEEE Symposium on Security and Privacy (S&P'14), IEEE Computer Society Press, San Jose, CA, USA, May 2014.
- Robert Künnemann.
Automated backward analysis of PKCS#11 v2.20.
In Principles of Security and Trust, to appear.
(long version + model files)]
- Itsaka Rakotonirina. Vérification automatique de protocoles de sécurité avec mémoire
globale et boucles. (In French). Sep 2014.