mgrabovsky / cryptoverif-py-lib Goto Github PK

This repository contains the supporting library for my CryptoVerif Python implementations fork along with two examples of its usage (adapted from the original CryptoVerif code).

⚠ PLEASE NOTE: This fork is no longer maintained. ⚠

To build the Python implementation files, you will need the Python implementations CryptoVerif fork.

To run the examples, you will need Python 3.

To run the fancy Woo–Lam shared key protocol example, you will need Docker and the Python libraries listed in wlskout/requirements.txt as well.

The CryptoVerif script for this file is nspk3tbl.ocv in the root directory. The example is to be run in the nsout/ directory.

To run this example, edit nsout/Makefile and modify the CV to point to the executable of the CryptoVerif fork. Then, in the nsout/ directory, run

$ make impl
$ make test

This will generate the Python implementation files that correspond to the CryptoVerif protocol script, and subsequently run the testing script. The keys are automatically generated by the library.

The associated CryptoVerif script is in the woolamsk.cv file. The unverified parts of the implementation are in the wlsout/ directory.

To run this example, edit wlskout/Makefile and modify the CV to point to the executable of the CryptoVerif fork. To install the required Python libraries, it is recommended to use a sandbox:

$ virtualenv env
$ source env/bin/activate
$ pip install -r requirements.txt

To run the example, you will first need to generate the implementation files and secret shared keys:

$ make impl
$ make keys

You can then create the Docker containers:

$ make docker

This will create two containers named wlsk_server and wlsk_responder. It is recommended to run those interactively in separate tmux panes so that you can see what's going on:

pane1$ docker start -ai wlsk_server
pane2$ docker start -ai wlsk_responder

Finally, run the initiator script:

pane3$ python initiator.py

It will ask you for the responder's address, which should be available in the corresponding container's output. The initiator will connect to the responder once and then quit. The server and responder will accept connections as long as they're running, so you can run the initiator as many times as you desire.

Here's a screen capture of how two consecutive runs of the WLSK example look:

See the LICENSE file for details.