YAPA

YAPA (Yet Another Protocol Analyzer) is a tool dedicated to the analysis of deducibility and static equivalence.
These two notions play an important role in the field of formal verification of security protocols, as they characterize the knowledge of an eavesdropper observing the run of a protocol. Specifically,


Download

The current version of the tool is available as a tar-gzip file : yapa_v0_7.tgz . It includes the Ocaml source files, a Makefile and some examples.

For installing, uncompress the file using (for instance) tar xzf yapa_v0_7.tgz then compile everything with make depend and make all (or make opt to use the native-code compiler). To run script files, simply run ./yapa (or ./yapa.opt) on them. You may also try ./yapa --help to list command-line options.

Features

The current tool accepts any equational theory described by a finite and convergent (i.e. confluent and terminating) set of rewrite rules. Correctness and completeness are guaranteed whenever the tool completes successfully.

The procedure always succeeds in a polynomial number of iterations when provided a (weak) subterm convergent theory, that is, a confluent set of rewrite rules of the form l -> r where r is either a proper subterm of l or a normal ground term.
In particular, this encompasses subterm convergent theories as defined by M. Abadi and V. Cortier [ICALP'04, CSFW'05, TCS'06].

The procedure provably never fails on layered convergent theories, a new class of theories encompassing e.g. blind signatures, pairing-homomorphic encryption, and prefix-homomorphic encryption. Besides, in all these examples, the procedure provably terminates as well. (See our technical report.)

For more complex theories, the tool may not terminate or report a failure of the procedure.

Quick examples

Consider the set of messages built upon secret random numbers, by applications of deterministic encryption/decryption (say a blockcipher), pairing and projections :

T, U, V... ::= a,b,c,k,n...
| enc(U,V) | dec(U,V)
| pair(U,V) | fst(U) | snd(U)
From a logical point of view, the semantics of these operations is accounted for by the following equations:
dec(enc(x,y), y) = x enc(dec(x,y), y) = x
fst(pair(x,y)) = x snd(pair(x,y)) = x

1) Deducibility. Consider for instance the following message:

pair(pair(enc(a,b), enc(b,c)), c)
To determine that the secret a is deducible from this term, we may run the tool on this script: 
symbol enc(2), dec(2), pair(2), fst(1), snd(1)
secret a, b, c

rule dec(enc(x,y),y)=x
rule enc(dec(x,y),y)=x
rule fst(pair(x,y))=x
rule snd(pair(x,y))=y

frame phi {
      x = pair(pair(enc(a,b), enc(b,c)), c)
}

query reachable a in phi
We obtain: 
$ ./yapa -v 0 test0a.yp
Starting a new problem.
Is a reachable from phi ?
=> true:
phi( dec(fst(fst(x)), dec(snd(fst(x)), snd(x))) )
The last term indeed evaluates to a modulo the equational theory under consideration.

2) Static equivalence. Now consider the two messages:

pair(enc(a,a), a) and pair(enc(a,a), b)
To check that these two messages can be distinguished, let us run the tool on this script: 
symbol enc(2), dec(2), pair(2), fst(1), snd(1)
secret a, b, c

rule dec(enc(x,y),y)=x
rule enc(dec(x,y),y)=x
rule fst(pair(x,y))=x
rule snd(pair(x,y))=y

frame phi1 {
      x = pair(enc(a,a), a)
}

frame phi2 {
      x = pair(enc(a,a), b)
}

query equivalent phi1 phi2
We obtain: 
$ ./yapa -v 0 test0b.yp
Starting a new problem.
Are phi1 and phi2 statically equivalent ?
=> false: x = pair(enc(snd(x), snd(x)), snd(x)) in phi1 but x <> pair(enc(snd(x), snd(x)), snd(x)) in phi2
As the given equation holds on the first message but not on the second, the two messages are not statically equivalrefent.

Technical reference

For more details on the algorithm, you may have a look at our research report. More involved examples are also provided in the distribution files.



Laboratoire Specification et Verification (LSV) -- CNRS UMR 8643 & ENS Cachan & INRIA Futurs.

You may send questions and comments to : mathieu.baudet@lsv.ens-cachan.fr