adds the specification generator

README.md

@@ -6,6 +6,8 @@
 
 This repository provides the following content:
 - [Full paper](./full_paper.pdf) containing the proofs
+- [Full paper with diff](./full_paper_colored.pdf) containing the full paper with changes compared to the previous submission marked in blue
 - Subdirectory `wireguard/model` contains the Tamarin model together with instructions how to verify it
 - Subdirectory `wireguard/implementation` contains the verified Go implementation together with instructions how to verify and execute it.
 - The subdirectory `dh` contains the verified DH protocol model together with a verified Go and Java implementations. Additionally, `dh/faulty-go-implementation` contains a Go implementation that tries to send the DH private key in plaintext for which verification fails because the IO specification does not permit such a send operation.
+- The subdirectory `specification-generator` contains the sources of our tool to generate I/O specifications for Gobra & VeriFast from a Tamarin model.

specification-generator/README.md

@@ -0,0 +1,25 @@
+# Tool for I/O Specification Generation
+
+The `src` directory contains the source code of our tool to generate I/O specifications from a Tamarin theory file. Note that it is a fork of Tamarin itself to reuse the parsing of input files.
+The `example-config-files` directory contains examples of configuration files to customize the operations of our tool.
+
+To build & execute our tool, [Haskell Stack](https://docs.haskellstack.org/en/stable/README) must be installed.
+
+## Generating I/O Specification
+Our tool must first be built using
+```
+stack build
+```
+
+Before using a Tamarin theory file as input to our tool, it should be verified in Tamarin first.
+Running the following command in the `src` folder will create I/O specifications for the Gobra verifier (`stack build` must have been executed):
+```
+stack exec -- tamarin-prover --tamigloo-compiler ../example-config-files/dh_gobra_config.txt
+```
+Note that the input Tamarin theory file is specified as `input_file` in the configuration file.
+Furthermore, `base_dir` specifies the output directory for the files containing the generated IO specification.
+
+The following command will instead generate I/O specifications for the VeriFast verifier (`stack build` must have been executed):
+```
+stack exec -- tamarin-prover --tamigloo-compiler ../example-config-files/dh_verifast_config.txt
+```

specification-generator/example-config-files/dh_gobra_config.txt

@@ -0,0 +1,9 @@
+
+
+input_file ../../dh/model/dh.spthy
+
+base_dir ../generated_iospecs_dh_gobra
+module dh
+make_go_mod False
+gobra_jar ../../wireguard/implementation/gobra.jar
+verifier gobra

specification-generator/example-config-files/dh_verifast_config.txt

@@ -0,0 +1,6 @@
+
+
+input_file ../../dh/model/dh.spthy
+
+base_dir ../generated_iospecs_dh_verifast
+verifier verifast

specification-generator/src/.dockerignore

@@ -0,0 +1,5 @@
+.git
+.stack-work
+.worktree
+lib/*/.stack-work
+examples

specification-generator/src/.gitignore

@@ -0,0 +1,45 @@
+.hsenv
+hsenv.log
+dist
+cabal-dev
+testbed
+case-studies/**/*.spthy
+case-studies/**/system.info
+case-studies-regression/fast-tests/system.info
+case-studies-sapic
+case-studies-sequential
+tamarin-prover-img
+.cabal-sandbox/
+cabal-sandbox/
+cabal.sandbox.config
+.stack-work/
+
+*.spthy.out
+*.spthy.tmp
+
+*.hi
+*.o
+*.prof
+*.un~
+*~
+
+*.cmi
+*.cmo
+plugins/sapic/lexer.ml
+plugins/sapic/sapic
+
+*.hpc
+unit.tix
+
+narrow
+unit
+
+client_session_key.aes
+
+.DS_Store
+tags
+stack.yaml.lock
+
+*.iml
+.idea/
+out/

specification-generator/src/.hgignore

@@ -0,0 +1,24 @@
+syntax:glob
+
+.svn
+
+*~
+.*.swp
+*.orig
+
+dist
+testbed
+
+*.hi
+*.o
+
+.hpc
+unit.tix
+
+narrow
+unit
+
+tags
+
+client_session_key.aes
+tamarin-prover-img

specification-generator/src/.travis.yml

@@ -0,0 +1,58 @@
+# Adapted from https://github.com/commercialhaskell/all-cabal-hashes-tool/blob/master/.travis.yml and https://raw.githubusercontent.com/commercialhaskell/stack/stable/doc/travis-simple.yml
+
+language: generic
+sudo: false
+env:
+  - OPAMYES=1
+
+cache:
+  directories:
+  - $HOME/.cabal
+  - $HOME/.ghc
+  - $HOME/.local/bin/
+  - $HOME/.stack
+  - .stack-work/
+
+addons:
+  apt:
+    sources:
+      - avsm
+    packages:
+    - camlp4-extra
+    - graphviz
+    - libgmp-dev
+    - ocaml
+    - ocaml-native-compilers
+    - opam
+
+before_install:
+  # Download and unpack the stack executable
+  - mkdir -p ~/.local/bin
+  - export PATH=$HOME/.local/bin:$PATH
+  - travis_retry curl -L https://www.stackage.org/stack/linux-x86_64 | tar xz --wildcards --strip-components=1 -C ~/.local/bin '*/stack'
+  - chmod a+x ~/.local/bin/stack
+  - stack --no-terminal setup
+  - travis_retry curl -L https://github.com/tamarin-prover/tamarin-prover/releases/download/1.6.0/Maude-2.7.1-linux.zip > maude.zip
+  - unzip -o maude.zip -d ~/.local/bin/
+  - mv -f ~/.local/bin/maude.linux64 ~/.local/bin/maude
+  - chmod a+x ~/.local/bin/maude
+  # create directories for automated tests
+  - mkdir -p case-studies case-studies/ake case-studies/ake/bilinear case-studies/ake/dh case-studies/related_work case-studies/related_work/StatVerif_ARR_CSF11 case-studies/related_work/AIF_Moedersheim_CCS10 case-studies/related_work/TPM_DKRS_CSF11 case-studies/related_work/YubiSecure_KS_STM12 case-studies/features case-studies/features/auto-sources case-studies/features/auto-sources/spore case-studies/features/xor case-studies/features/xor/basicfunctionality case-studies/features/injectivity case-studies/features/multiset case-studies/features/private_function_symbols case-studies/features/equivalence case-studies/fast-tests case-studies/fast-tests/related_work case-studies/fast-tests/related_work/StatVerif_ARR_CSF11 case-studies/fast-tests/related_work/AIF_Moedersheim_CCS10 case-studies/fast-tests/related_work/TPM_DKRS_CSF11 case-studies/fast-tests/related_work/YubiSecure_KS_STM12 case-studies/fast-tests/features case-studies/fast-tests/features/injectivity case-studies/fast-tests/features/multiset case-studies/fast-tests/features/private_function_symbols case-studies/fast-tests/features/equivalence case-studies/fast-tests/csf18-xor case-studies/fast-tests/csf18-xor/diff-models case-studies/fast-tests/regression case-studies/fast-tests/regression/diff case-studies/fast-tests/cav13 case-studies/fast-tests/post17 case-studies/fast-tests/csf12 case-studies/fast-tests/loops case-studies/fast-tests/ccs15 case-studies/classic case-studies/sapic case-studies/sapic/fast case-studies/sapic/fast/GJM-contract case-studies/sapic/fast/statVerifLeftRight case-studies/sapic/fast/feature-inevent-restriction case-studies/sapic/fast/basic case-studies/sapic/fast/MoedersheimWebService case-studies/sapic/fast/feature-let-bindings case-studies/sapic/fast/feature-locations case-studies/sapic/fast/feature-boundonce case-studies/sapic/fast/feature-xor case-studies/sapic/fast/SCADA case-studies/sapic/fast/feature-secret-channel case-studies/sapic/fast/fairexchange-mini case-studies/sapic/fast/feature-predicates case-studies/sapic/slow case-studies/sapic/slow/NSL case-studies/sapic/slow/PKCS11 case-studies/sapic/slow/encWrapDecUnwrap case-studies/sapic/slow/feature-locations case-studies/sapic/slow/Yubikey case-studies/csf18-xor case-studies/csf18-xor/diff-models case-studies/regression case-studies/regression/trace case-studies/regression/diff case-studies/cav13 case-studies/post17 case-studies/csf12 case-studies/csf19-wrapping case-studies/loops case-studies/ccs15 case-studies/classic case-studies/fast-tests/ake case-studies/fast-tests/ake/bilinear
+
+
+
+install:
+  # pre-build 'mwc-random' and 'SHA' as otherwise Travis CI sometimes runs out of memory
+  - stack --no-terminal build mwc-random SHA -j 1
+  - stack --no-terminal install
+
+  # SAPIC
+  # - opam init
+  # - eval `opam config env`
+  - stack install
+  # - make -C plugins/sapic
+
+script:
+  - tamarin-prover test
+  # - make sapic-case-studies
+  - python3 regressionTests.py -noi

specification-generator/src/AUTHORS

@@ -0,0 +1,13 @@
+Authors:
+  Benedikt Schmidt <[email protected]>
+  Simon Meier      <[email protected]>
+
+Obervational Equivalence authors:
+  Jannik Dreier <[email protected]>
+  Ralf Sasse    <[email protected]>
+
+Contributors:
+  protocol models, GUI:   Cas Cremers <[email protected]>
+  original web interface: Cedric Staub <[email protected]>
+  YubiKey models, SAPIC:  Robert Kuennemann <[email protected]>
+  and many others