Add Esorics'23 Bluetooth examples (#605) #328
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| name: Tamarin compilation and regression tests | |
| on: [push, pull_request] | |
| jobs: | |
| Tamarin-Integration-Test: | |
| runs-on: ubuntu-latest | |
| steps: | |
| - run: echo "Tamarin compilation and regression test triggered by a ${{ github.event_name }} event." | |
| - run: echo "Branch ${{ github.ref }}, repository ${{ github.repository }}." | |
| - name: Check out repository code | |
| uses: actions/checkout@v3 | |
| - name: Installation of dependencies | |
| run: | | |
| sudo apt-get update | |
| sudo apt-get install graphviz | |
| - name: Caching | |
| uses: actions/cache@v2 | |
| with: | |
| path: | | |
| ~/.stack | |
| ~/.cabal | |
| ~/.ghc | |
| ~/.local/bin/ | |
| .stack-work | |
| # best effort for cache: tie it to Stack resolver and package config | |
| key: ${{ runner.os }}-stack-${{ hashFiles('stack.yaml.lock', 'package.yaml') }} | |
| restore-keys: | | |
| ${{ runner.os }}-stack | |
| - name: Pre-install | |
| run: | | |
| mkdir -p ~/.local/bin | |
| export PATH=$HOME/.local/bin:$PATH | |
| 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 | |
| curl -L https://github.com/SRI-CSL/Maude/releases/download/3.2.1/Maude-3.2.1-linux.zip > maude.zip | |
| unzip -oj maude.zip -d ~/.local/bin/ | |
| mv -f ~/.local/bin/maude.linux64 ~/.local/bin/maude | |
| chmod a+x ~/.local/bin/maude | |
| mkdir -p case-studies case-studies/ake case-studies/ake/bilinear case-studies/ake/dh case-studies/related_work | |
| mkdir -p case-studies/related_work/StatVerif_ARR_CSF11 case-studies/related_work/AIF_Moedersheim_CCS10 | |
| mkdir -p case-studies/related_work/TPM_DKRS_CSF11 case-studies/related_work/YubiSecure_KS_STM12 case-studies/features | |
| mkdir -p case-studies/features/auto-sources case-studies/features/auto-sources/spore case-studies/features/xor | |
| mkdir -p case-studies/features/xor/basicfunctionality case-studies/features/injectivity case-studies/features/multiset | |
| mkdir -p case-studies/features/private_function_symbols case-studies/features/equivalence case-studies/fast-tests | |
| mkdir -p case-studies/fast-tests/related_work case-studies/fast-tests/related_work/StatVerif_ARR_CSF11 | |
| mkdir -p case-studies/fast-tests/related_work/AIF_Moedersheim_CCS10 case-studies/fast-tests/related_work/TPM_DKRS_CSF11 | |
| mkdir -p case-studies/fast-tests/related_work/YubiSecure_KS_STM12 case-studies/fast-tests/features | |
| mkdir -p case-studies/fast-tests/features/injectivity case-studies/fast-tests/features/multiset | |
| mkdir -p case-studies/fast-tests/features/private_function_symbols case-studies/fast-tests/features/equivalence | |
| mkdir -p case-studies/fast-tests/csf18-xor case-studies/fast-tests/csf18-xor/diff-models case-studies/fast-tests/regression | |
| mkdir -p case-studies/fast-tests/regression/diff case-studies/fast-tests/cav13 case-studies/fast-tests/post17 | |
| mkdir -p case-studies/fast-tests/csf12 case-studies/fast-tests/loops case-studies/fast-tests/ccs15 case-studies/classic | |
| mkdir -p case-studies/sapic case-studies/sapic/fast case-studies/sapic/fast/GJM-contract case-studies/sapic/fast/statVerifLeftRight | |
| mkdir -p case-studies/sapic/fast/feature-inevent-restriction case-studies/sapic/fast/basic | |
| mkdir -p case-studies/sapic/fast/MoedersheimWebService case-studies/sapic/fast/feature-let-bindings | |
| mkdir -p case-studies/sapic/fast/feature-locations case-studies/sapic/fast/feature-boundonce case-studies/sapic/fast/feature-xor | |
| mkdir -p case-studies/sapic/fast/SCADA case-studies/sapic/fast/feature-secret-channel case-studies/sapic/fast/fairexchange-mini | |
| mkdir -p case-studies/sapic/fast/feature-predicates case-studies/sapic/slow case-studies/sapic/slow/NSL case-studies/sapic/slow/PKCS11 | |
| mkdir -p case-studies/sapic/slow/encWrapDecUnwrap case-studies/sapic/slow/feature-locations case-studies/sapic/slow/Yubikey | |
| mkdir -p case-studies/csf18-xor case-studies/csf18-xor/diff-models case-studies/regression case-studies/regression/trace | |
| mkdir -p case-studies/regression/diff case-studies/cav13 case-studies/post17 case-studies/csf12 case-studies/csf19-wrapping | |
| mkdir -p case-studies/loops case-studies/ccs15 case-studies/classic case-studies/fast-tests/ake case-studies/fast-tests/ake/bilinear | |
| - name: Compilation | |
| run: | | |
| stack --no-terminal build mwc-random SHA -j 1 | |
| stack --no-terminal install | |
| stack install | |
| - name: Regression tests | |
| run: | | |
| tamarin-prover test | |
| python3 regressionTests.py -v 6 -noi | |
| - name: Store case studies as artifact | |
| if: success() || failure() | |
| uses: actions/upload-artifact@v3 | |
| with: | |
| name: case-studies | |
| path: case-studies |