cpp2dpa

Abstract

cpp2dpa is a tool to convert cryptographic protocols into deterministic pushdown automata, enabling proofs of equivalence and discovery of attacks. The procedure is detailed in the journal version of this article, which contains detailed proofs, implementation details and additional examples.

cpp2dpa is coded in Python 3. Here are the sources.

To carry the proofs or find attacks, cpp2dpa is interfacing with a modified version of the LALBLC tool which requires the Numpy package. This version includes optimized conversion from automata to grammars and the possibility to store grammars. The source is available here.

Installing cpp2dpa

You first need to install Python3, along with the Numpy module, available here. To install Numpy, assuming you run a Unix system and extracted the sources:

python3 setup.py build
python3 setup.py install

Then, to install LALBLC, you first need to extract the archive

mkdir LALBLC
tar -xvf LALBLC.tar.gz LALBlC/ 

And finally, to install cpp2dpa:

mkdir cpp2dpa
tar -xvf cpp2dpa.tar.gz cpp2dpa/ 

If you did not use the same folders, you need to update the path in the file cpp2dpa.py, as well as in the example files such as Test.py.

How to write protocols in cpp2dpa

Protocols are written as Python Protocol objects. They consist in one or several variables and a list of rules, of the form (channel, input pattern, output pattern). Here are the two protocols of the first running example from the article.

passport1 = Protocol(['x'],
             [
                 # Making mackm(2) a signature-like primitive
                 ('cmac','x.mackm','x'),
                 ('cmac','x.mackm2','x'),
                 # Giving a message from a previous session
                 ('c0', 'start', 'nr0.kr0.np0.ke.mackm'),
                 # The protocol
                 # The reader is not modeled
                 ('c1', 'start', 'nr.kr.np.ke.mackm'),
                 ('c2', 'x.ke.mackm', 'x.qmacok'),
                 ('c3', 'x.np.qmacok', 'x.np.kp.mackm'),
                 ])
passport2 = Protocol(['x'],
             [
                 # Making mackm(2) a signature-like primitive
                 ('cmac','x.mackm','x'),
                 ('cmac','x.mackm2','x'),
                 # Giving a message from a previous session
                 ('c0', 'start', 'nr0.kr0.np0.ke.mackm'),
                 # The protocol
                 # The reader is not modeled
                 ('c1', 'start', 'nr.kr.nq.ke2.mackm2'),
                 ('c2', 'x.ke2.mackm2', 'x.qmacok'),
                 ('c3', 'x.nq.qmacok', 'x.nq.kq.mackm2'),
                 ])

Other examples are avaiblable in the Examples folder, containing, among others, the full running example and the electronic passport.

Running cpp2dpa

To prove the (non)-equivalence of the two protocols passport1 and passport2, as described in the article, you can use the file Test.py (note that the third argument for each protocol is just an arbitrary string used as name), and the command, in the cpp2dpa folder:

python3 Test.py

The output would then be (in three parts):

RunningExample1 reach grammar successfully computed.
################################
Result using strategy 1
################################
[1, ['init', 'c0', 'c0', 'c2', 'c2', 'exit']]

Hence proving than the trace of passport1 obtained by using the messages built through channels init, c0 and c2 cannot be matched by passport2, thus constituting an attack. Then, examining the case of tests reducing to constants only, you would get:

RunningExample1 const grammar successfully computed.
################################
Result using strategy 1
################################
number of nodes 43
list of adresses of open nodes:
 []
list of adresses of closed nodes:
 ['e', 'e*0', 'e*1', 'e*2', 'e*3', 'e*4', 'e*5', 'e*5*0', 'e*5*1', 'e*5*2', 'e*5*3', 'e*5*4', 
'e*5*5', 'e*5*6', 'e*5*6*0', 'e*5*6*1', 'e*5*6*2', 'e*5*6*3', 'e*5*6*4', 'e*5*6*5', 'e*5*6*6',
 'e*5*6*6*0', 'e*5*6*6*1', 'e*5*6*6*2', 'e*5*6*6*3', 'e*5*6*6*4', 'e*5*6*6*5', 'e*5*6*6*5*0',
 'e*5*6*6*5*1', 'e*5*6*6*5*2', 'e*5*6*6*5*3', 'e*5*6*6*5*4', 'e*5*6*6*5*5', 'e*5*6*6*5*6',
 'e*5*6*6*5*6*0', 'e*5*6*6*5*6*1', 'e*5*6*6*5*6*2', 'e*5*6*6*5*6*3', 'e*5*6*6*5*6*4',
 'e*5*6*6*5*6*5', 'e*5*6*6*5*6*6', 'e*5*6*6*6', 'e*6']
list of adresses of nodes with dedrule==TC*:
 []

  0 lists of unifiers:

total cardinality:
 43
number of closed nodes:
 43
number of open nodes:
 0
all mgu's

Thus proving that no constant test can distinguish between the frames generated by passport1 and passport2.

Finally, the case where you consider guarded tests leads to the last part of the output:

RunningExample1 fork grammar successfully computed.
################################
Result using strategy 1
################################
[1, ['init', 'c0', 'c0', 'blue+c2', 'blue+c2', 'phase2', 'exit']]

which witnesses a attack similar the one already observed with the reach automata.

Output files for the corrected version of the protocol can be found here: reach automata const automata fork automata.

Output files for the first example can be found here: reach automata const automata fork automata.

Output files for the second example can be found here: reach automata const automata fork automata.

About LSV