Official LSV Web Site

AKISS

Abstract

AKISS is a tool implementing a procedure for verifying trace equivalence (or equivalently may-testing equivalence) for bounded security processes with no else branches employing cryptographic primitives modeled by an optimally reducing rewrite system. Trace equivalence can be used to model strong secrecy, vote-privacy and other security properties.

AKISS uses an fully-abstract encoding of symbolic traces into Horn clauses, thereby extending the KISS which can only check static equivalence. In order to get rid of the equatinal theory modeling the crytographic primitives, AKISS employs the algorithms for computing strongly complete sets of variants and complete set of unifiers of SubVariant.

AKISS is described in an article submitted for publication, in Chapter 5 of the PhD thesis of Ștefan Ciobâcă, a preliminary version of which is available here and in the research report available here.

Installing AKISS

AKISS in written in Ocaml. The source files for AKISS are available on its github page.

After installing the above dependencies, it is sufficient to type:

make
to compile AKISS.

Running AKISS

After succesfully compiling AKISS, you can run it on an input such as the following input file "cat examples-thesis/running-example/running-example-both-traces.api" found in AKISS's distribution file:

$  cat examples/running-example/running-example-both-traces.api
/* this examples illustrates why symbolic trace-to-symbolic trace
equivalence checking is not always complete. */

symbols enc/2,       // models encryption
  dec/2;             //    and decryption

channels c;

private a, b, k, ok;

var X, Y, Z;

rewrite dec(enc(X, Y), Y) -> X;

s = out(c, enc(a, k)).out(c, enc(b, k)).in(c, X).[enc(dec(X, k), k) = X].out(c, ok).0;

r1 = out(c, enc(a, k)).out(c, enc(b, k)).in(c, X).[X = enc(a, k)].out(c, ok).0;

r2 = out(c, enc(a, k)).out(c, enc(b, k)).in(c, X).[X = enc(b, k)].out(c, ok).0;

equivalentct? s and r1, r2; // s is equivalent to r1 and r2, but not to r1
// nor to r2
// as can be seen from the other examples running-example-first-trace.api
// and running-example-second-trace.api

The file begins with a technical description of the example in C-style comments "/* */". These comments do not nest. Next, a few preliminary declarations are made. "enc" and "dec" are declared as function symbols of arity 2, modelling encryption and decryption. C++ style comments "//" appear next to each symbol. These comments run to the end-of-line.

One channel "c" is declared. Channels can only be public and atomic. Next, a set of 4 private names is declared. Private names intuitively represent fresh values chosen by the protocol participants, values which are a-priori unknown to the attacker. Next, "X", "Y" and "Z" are declared as being variables. Function symbols, channel names, private names and variables should be identifiers as in the C language. The declarations up to this point can be arbitrarely permuted and several directives for declaring the same types of entities are allowed. Duplicates are disallowed. Function symbols have an unique arity.

Next comes the definition of the rewrite system. In this case, there is only one rewrite rule, although several are allowed (see the other examples for the syntax of multiple rewrite rules) which states that decryption (the function symbol "dec") cancels out encryption (the function symbol "enc") if the right key is used.

After all rewrite rules, symbolic traces and processes can be specified. Here we declare three traces "s", "r1" and "r2". All three traces have the same basic structure, with two inputs followed by an input followed by a test followed by an output, if the test succeds. All three traces begin with outputing the encryption of two secrets names "a" and "b" with the same secret key "k".

In the case of the trace "s", the test is equivalent to checking that the input received in the third step is an encryption with "k" (the test encodes exactly this). In the case of "r1", the test checks that what was received is the encryption of "a" with "k" and in "r2", the test checks that what was received is the encryption of "b" with "k".

To run AKISS on the example file, simply type:

$. ./akiss.native < examples/running-example/running-example-both-traces.api
s and r1, r2 are TRACE EQUIVALENT!

AKISS was able to prove that the symbolic trace "s" is equivalent to the set of symbolic traces "r1", "r2". Note however that "s" is not equivalent to either "r1" or "r2". This can be checked using AKISS as well:

$ cat examples/running-example/running-example-first-trace.api
... [omitted as it is the same as above] ...

equivalent? s and r1;
$ ./akiss.native < examples/running-example/running-example-first-trace.api
The following tests work on s but not on r1:
check_identity(world(out(c), world(out(c), world(in(c, w1), world(test, world(out(c), empty))))), dec(enc(X219, X221), X221), X219)

check_run(world(out(c), world(out(c), world(in(c, w1), world(test, world(out(c), empty))))))

AKISS says that there is a test which works on "s" but not on "r1". The the consists of letting "s" perform two outputs, then sending it the second thing it output ("w1" refers to the second output, "w0" to the first), letting it perform a test and letting it output. This tests works on "s" but not on "r1" as "r1" will block when checking "enc(a, k) = enc(b, k)" in its fourth step. Similarly,

$ cat examples/running-example/running-example-second-trace.api
... [omitted as it is the same as above] ...

equivalent? s and r2;
$ ./akiss.native < examples/running-example/running-example-second-trace.api
The following tests work on s but not on r2:
check_identity(world(out(c), world(out(c), world(in(c, w0), world(test, world(out(c), empty))))), dec(enc(X219, X221), X221), X219)

check_run(world(out(c), world(out(c), world(in(c, w0), world(test, world(out(c), empty))))))

Note that this time it was the first output "w0" to be used in the test distinguishing "s" from "r2".

Equivalences

The query "equivalent?" tests for course trace equivalence, an equivalence which coincides with trace equivalence for determinate processes. If the processes that are being tested are not known to be determinate, the query "equivalentsq?" should be used instead. The query "equivalentsq?" will make sure that every symbolic trace of the right hand side is equivalent to a symbolic trace on the left hand side. This is a sufficient condition for trace equivalence. The following examples models vote privacy in the FOO e-voting protocol. As the protocol is not determinate, equivalentsq? is used. AKISS can prove that the equivalence holds, therefore FOO has vote privacy.

bash-3.2$ cat examples/foo/foo.api
// This is a modeling of the Fujioka et al. (FOO) protocol.
// Vote-privacy is proven.
// 
// Informal description of the voter role is as follows:
//
// Phase 1: 
// V -> Admin: sign(blind(commit(vote, r), b), kV))
// Admin -> V: sign(blind(commit(vote, r), b), kAdmin))
// Phase 2: 
// V -> Collector: sign(commit(vote, r), kAdmin)
// Phase 3: 
// V -> Collector: r
//
// Note that Admin and Collector are not supposed to be trusted and hence not modeled, i.e. they are part of the attacker
//

symbols open/2, commit/2, check/2, sign/2, pk/1, unblind/2, blind/2, yes/0, no/0, kAuth/0;

private rAyes, bAyes, rAno, bAno, kA, kB, rBno, bBno, rByes, bByes;

channels A, B, C;

var x, y, z, xAyes, xBno, xByes, xAno;


// Rewrite rules for commitment and blind signatures
rewrite open(commit(x, y), y) -> x;
rewrite check(sign(x, y), pk(y)) -> x;
rewrite unblind(sign(blind(x, y), z), y) -> sign(x, z);

// Phases 1-3 for voter A voting 'yes'
AyesP1 = out(A, sign(blind(commit(yes, rAyes), bAyes), kA)).in(A, xAyes). [check(xAyes, pk(kAuth)) = blind(commit(yes, rAyes), bAyes)].0;
AyesP2 = out(C, unblind(xAyes, bAyes)).0;
AyesP3 = out(C, rAyes).0;


// Phases 1-3 for voter A voting 'no'
AnoP1 = out(A, sign(blind(commit(no, rAno), bAno), kA)).in(A, xAno). [check(xAno, pk(kAuth)) = blind(commit(no, rAno), bAno)].0;
AnoP2 = out(C, unblind(xAno, bAno)).0;
AnoP3 = out(C, rAno).0;

// Phases 1-3 for voter B voting 'yes'
ByesP1 = out(B, sign(blind(commit(yes, rByes), bByes), kB)).in(B, xByes).[check(xByes, pk(kAuth)) = blind(commit(yes, rByes), bByes)].0;
ByesP2 = out(C, unblind(xByes, bByes)).0;
ByesP3 = out(C, rByes).0;

// Phases 1-3 for voter B voting 'no'
BnoP1 = out(B, sign(blind(commit(no, rBno), bBno), kB)).in(B, xBno).[check(xBno, pk(kAuth)) = blind(commit(no, rBno), bBno)].0;
BnoP2 = out(C, unblind(xBno, bBno)).0;
BnoP3 = out(C, rBno).0;

// Interleaving each of the phases separately
Phase1AyesBno = interleave_opt AyesP1, BnoP1;
Phase2AyesBno = interleave_opt AyesP2, BnoP2;
Phase3AyesBno = interleave_opt AyesP3, BnoP3;

// protocol for A voting 'yes' and B voting 'no'
AyesBno = sequence Phase1AyesBno, Phase2AyesBno, Phase3AyesBno;

// Interleaving each of the phases separately
Phase1AnoByes = interleave_opt AnoP1, ByesP1;
Phase2AnoByes = interleave_opt AnoP2, ByesP2;
Phase3AnoByes = interleave_opt AnoP3, ByesP3;

// protocol for A voting 'no' and B voting 'yes'
AnoByes = sequence Phase1AnoByes, Phase2AnoByes, Phase3AnoByes;

// publishing public keys
Setup = out(C, pk(kA)).out(C, pk(kB)).0;

P = sequence Setup, AyesBno;
Q = sequence Setup, AnoByes;

equivalentft? P and Q;

When we run AKISS on the above file, after ~15 seconds we receive a message that AKISS has been able to prove the equivalence.

$ ./akiss.native < examples-thesis/foo/foo.api 
P01, P02, P03, P04, P05, P06, P07, P08, P09, P10, P11, P12, P13, P14, P15, P16, P17, P18, P19, P20, P21, P22, P23, P24 and Q01, Q02, Q03, Q04, Q05, Q06, Q07, Q08, Q09, Q10, Q11, Q12, Q13, Q14, Q15, Q16, Q17, Q18, Q19, Q20, Q21, Q22, Q23, Q24 are trace equivalent

We suspect that AKISS always terminates at least for subterm convergent equational theories but we have not been able to show this due to the complex shapes of the Horn clauses being generated. If AKISS does not seem to terminate, you can run it with the "-verbose" and/or the "-debug" option, which will make it output several of the actions being performed.

Contact

If you have questions/problems regarding AKISS, please contact Ștefan Ciobâcă at name@lsv.ens-cachan.fr. Use "ciobaca" for name.

References

AKISS is described in an article submitted for publication, in Chapter 5 of the PhD thesis of Ștefan Ciobâcă, a preliminary version of which is available here and in the research report available here.

About LSV