DNP3 SAv5 (Asymmetric) Tamarin file README
==========================================

This is the README for the Tamarin files associated with the Journal of Computer Security submission 
''Secure Authentication in the Grid: A formal analysis of DNP3: SAv5''.
These models have the Asymmetric mode of the Update Key Change Protocol included (where the ESORICS
2017 submission did not.) Full paper link at [https://tamarin-prover.github.io/](https://tamarin-prover.github.io/).

Please see the sub-directory `/examples/jcs18/ESORICS-symmetric-only/` for the (obsolete) symmetric-only models from the ESORICS 2017 submission (The ESORICS paper can be found at https://doi.org/10.1007/978-3-319-66402-6_23).

Authors: Cas Cremers, Martin Dehnel-Wild, Kevin Milner.

**TL;DR: Install Tamarin. Run `make` on this directory. Visit [http://127.0.0.1:3001/](http://127.0.0.1:3001/)**


Tamarin Installation
--------------------

To run these files, you will need the Tamarin Prover tool installed.

Please follow the [instruction instructions within the Tamarin Manual (link)](https://tamarin-prover.github.io/manual/book/002_installation.html).



Running Tamarin to verify these files
-------------------------------------

If you have both m4 and make installed, please then run

>     make

on this directory. This will generate the correct output files.

Once this is running, please then visit [http://127.0.0.1:3001/](http://127.0.0.1:3001/) in your browser.

This will open the interactive Tamarin web GUI, where you will be able to interact with the lemmas and generate proofs.


You may have to click ''Allow the application tamarin-prover to accept incoming network connections''.
If port 3001 is already being used for something on your system, please change this port number in the Makefile.

If you do not have both `m4` and `make` installed, please copy and paste the following command into a terminal in this directory:

>     tamarin-prover interactive . --port=3001 --heuristic=i

and then point your browser to [http://localhost:3001/](http://localhost:3001/).
This will run the Tamarin Prover with the correct heuristic against the current folder (and the `*.spthy` files in it), and then open the interactive Tamarin web-GUI.

Within this web-page, you then have the choice between `DNP3Asymm`,
`DNP3AsymmProven`, `DNP3AsymmTraceExists`, and `DNP3_incorrect`.

- `DNP3Asymm` is the main model. Feel free to play around with this, or to click
  'autoprove' on any or all of these lemmas. These all prove fairly
  quickly on modern computers, but prove fastest with the latest version of
  Tamarin (`1.3.0` or higher, built from source). Minimum version required: `1.2.2`. This is
  from the file `dnp3.spthy` (generated by `m4` from `dnp3.m4`). If you just want
  to read the source-code, please read `dnp3.m4`, as the ordering will make the
  most sense to the reader. Tamarin struggles to find an automatic proof for
  the `CSQ_Uniqueness` lemma, so we include that lemma pre-proven manually.

  To prove a property in the interactive web UI, click "sorry" at the bottom
  of a lemma, and then "autoprove" (or press the 'a' character on your keyboard).

- `DNP3AsymmProven` is the same main model, but with all the proofs pre-
  calculated. This is from the file `dnp3-proven.spthy`. This will take a
  little while to load (~10mins) as it has to check that the presented proofs
  are indeed correct. When it does load, everything should be green.

- `DNP3AsymmTraceExists` is the same as the main model, but with an exists-trace
  lemma added in, manually proven correct, and the proof saved. This is to give
  the reader a small demonstration that the protocol models do work as intended
  in the honest setting, and that the security proofs haven't been generated on
  a non-functional protocol model. The output trace can be viewed by clicking
  the 'SOLVED // trace found' link within the proof, or alternatively, readers
  can view the trace.png image within this directory.

- `DNP3_incorrect` is the *incorrect* attack from Amoah et al., 2014 [26]. This is a
  significant under-approximation of the main (symmetric-only) model, to make
  the attack work. Please read Section 6 of the main paper for more details.
  This is from the file `dnp3-amoah-attack.spthy`.


The main `DNP3Asymm` file is provided as an m4 file, as we use m4 macros to change
the order of some of the protocol rules for the sake of proof-speed; Tamarin
solves goals for various rules dependent on the order of the rules in the file,
so the logical order as per the protocol execution is not the most efficient for
Tamarin's heuristics. Note: this DOES NOT affect the protocol model's
correctness or validity, or possible protocol execution paths, it merely changes
the order in which goals are solved. We also provide `dnp3.spthy` pre-generated
(for users without `m4`), but it is not recommended that you attempt to read this
version. Feel free to run `m4 dnp3.m4 > dnp3.spthy` to confirm that the latter
file was actually generated by the former.


All results and timings for the JCS paper were originally proven with the specific version [`tamarin-prover version 1.3.0`](https://github.com/tamarin-prover/tamarin-prover/tree/8e823691ad3325bce8921617b013735523d74557), but we recommend using the latest release of Tamarin by [following the installation instructions in the manual](https://tamarin-prover.github.io/manual/book/002_installation.html), or getting the [latest release from GitHub](https://github.com/tamarin-prover/tamarin-prover/releases). As of June 2018, we recommend using [version 1.4.0](https://github.com/tamarin-prover/tamarin-prover/releases/tag/1.4.0), as all results have been tested with this.



For reference, the DNP3 standard can be found at: [http://ieeexplore.ieee.org/document/6327578/](http://ieeexplore.ieee.org/document/6327578/).
Protocol definitions can be found in Chapter 7 of this document.
All message formats are described in Appendix A.45.x where x is the
object reference number. (e.g. `g120v4` = Appendix A.45.4)
