KISS (Knowledge In Security protocolS) is an implementation of the procedure for deduction and static equivalence presented in in our research report. The procedure is able to handle cryptographic primitives modeled by any convergent term rewriting system. KISS is known to terminate on a wide range of rewriting systems, such as subterm convergent rewriting systems, blind signatures and trapdoor commitment.
bz2ed C++ source code
set of example inputs
mkdir kiss ;; create a directory cd kiss ;; to place source code  download the above archives into the current directory  tar xjvf kiss.tar.bz2 ;; unzip the source code tar xjvf examples.tar.bz2 ;; unzip the examples make ;; compile kiss ./kiss < runningexample.in ;; test the tool on the ;; running example of the paper
KISS reads queries from the standard input and outputs answers to standard output. The input must corespond to the following BNFlike grammar:
Number ::= [09]* 
Identifier ::= ([az]  [AZ]  _  [09])* 
Term ::= Identifier  Identifier(Term#)
signature pair/2, fst/1, snd/1, enc/2, dec/2; variables x, y, z; names a, b, c, k, w1, w2, w3; rewrite fst(pair(x, y)) > x, snd(pair(x, y)) > y, dec(enc(x, y), y) > x; frames phi1 = new a, k.{w1 = enc(a, k), w2 = a}, phi2 = new b, k.{w1 = enc(b, k), w2 = c}; questions deducible a phi1, equiv phi1 phi2, knowledgebase phi1; The first line declares 5 function symbols, together with their arity. The following lines declares that the identifiers x, y and z will be used as variables. The following line declares that the identifiers a, b, c, k, w1, w2 and w3 will be used as names. The declaration of term rewriting system starts on the fourth line and it contains three rewrite rules. Next follow the frame declarations. We declare two frames, phi1 and phi2. Each of the two frames contains two bound names: a and k for phi1 and resp. b and k for phi2. The frames each contain two messages identified by the names w1 and resp. w2. On the fourth to last line start the questions. The first question is to determine if the term a is deducible from the frame phi1. The next question asks if the two frames are statically equivalent and the last question asks for the knowledge base associated to the frame phi1. For reference, here is the output of KISS when run on the above example: Saturating frame phi1... We have 7 deduction facts and 3 eq. facts. Saturating frame phi2... We have 8 deduction facts and 4 eq. facts. Answers to questions: Yupii, phi1  a with recipe w2 Sorry, phi1 is not statically equivalent to phi2 Here's an equation that holds in phi2 but not in phi1 [ c ~ w2  ] Voila the saturated knowledge base of phi1: Deduction facts: [ dec(\X0,\X1) > dec(\x0,\x1)  \X0 > \x0, \X1 > \x1 ] [ enc(\X0,\X1) > enc(\x0,\x1)  \X0 > \x0, \X1 > \x1 ] [ fst(\X0) > fst(\x0)  \X0 > \x0 ] [ pair(\X0,\X1) > pair(\x0,\x1)  \X0 > \x0, \X1 > \x1 ] [ snd(\X0) > snd(\x0)  \X0 > \x0 ] [ w1 > enc(a,k)  ] [ w2 > a  ] Equational facts: [ dec(enc(\X0,\X1),\X1) ~ \X0  ] [ fst(pair(\X0,\X1)) ~ \X0  ] [ snd(pair(\X0,\X1)) ~ \X1  ] The program starts by applying the saturation procedure on phi1 and phi2. In general, because the underlying problem is undecidable, the saturation process does not terminate. For this particular term rewriting system, saturation is guaranteed to terminate (in polynomial time). After having saturated all frames, KISS starts answering questions^{[*]}. KISS is glad to see that the term a is indeed deducible from phi1 with recipe w2. It is sorry to inform you that phi1 and phi2 are not statically equivalent and it gives an example of an equation that holds in phi2 but not in phi1 (the equation being c ~ w2). Had there been an equation that would hold in phi1 but not in phi2, KISS would have informed you of that as well. Finally, KISS joyfully shows you the knowledgebase associated to phi1. Command line argumentsIn order to see the intermediate deduction and equational facts (i.e. the unsolved ones), you can increase the verbosity to 2 (or even to 4): ./kiss v 2 < example.in Saturating frame phi1... Solving [ dec(\Y0,\Y1) > \y0  \Y0 > enc(\y0,\y1), \Y1 > \y1 ] Solving [ dec(enc(\Y0,\Y1),\Y2) > \y0  \Y0 > \y0, \Y1 > \y1, \Y2 > \y1 ] Solving [ dec(w1,\Y0) > a  \Y0 > k ] ... If you do not like to see KISS happy, you can shut it up using the sober option: ./kiss sober < example.in ... Answers to questions: phi1  a with recipe w2 phi1 is not statically equivalent to phi2 Here's an equation that holds in phi2 but not in phi1 [ c ~ w2  ] ... ContactIf you have questions/problems regarding KISS, please contact Ștefan Ciobâcă at name@lsv.enscachan.fr. Use "ciobaca" for name.^{[*]} "Computers are useless. They can only give you answers." Picasso
