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.
After installing the above dependencies, it is sufficient to type:
maketo compile 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
$ 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".
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.
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.