diff --git a/.github/workflows/tamarin-integration-test.yaml b/.github/workflows/tamarin-integration-test.yaml new file mode 100644 index 000000000..075a1a675 --- /dev/null +++ b/.github/workflows/tamarin-integration-test.yaml @@ -0,0 +1,78 @@ +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/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 + 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 -noi diff --git a/.travis.yml b/.travis.yml deleted file mode 100644 index 05f736c91..000000000 --- a/.travis.yml +++ /dev/null @@ -1,58 +0,0 @@ -# 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 diff --git a/case-studies-regression/fast-tests/ake/bilinear/Scott_analyzed.spthy b/case-studies-regression/fast-tests/ake/bilinear/Scott_analyzed.spthy new file mode 100644 index 000000000..8fc84525b --- /dev/null +++ b/case-studies-regression/fast-tests/ake/bilinear/Scott_analyzed.spthy @@ -0,0 +1,1834 @@ +theory Scott begin + +// Function signature and definition of the equational theory E + +builtins: diffie-hellman, bilinear-pairing +functions: fst/1, hp/1, kdf/1, pair/2, snd/1 +equations: fst() = x.1, snd() = x.2 + + + +section{* Scott: MTI-C0 like identity based key exchange protocol *} + +rule (modulo E) KGC_Setup: + [ Fr( ~msk ) ] --[ KGCSetup( ) ]-> [ !MSK( ~msk ) ] + + /* has exactly the trivial AC variant */ + +rule (modulo E) KGC_request: + [ !MSK( ~msk ) ] --> [ !LTK( $ID, pmult(~msk, hp($ID)) ) ] + + /* has exactly the trivial AC variant */ + +rule (modulo E) Reveal_ltk: + [ !LTK( $ID, skID ) ] --[ LtkRev( $ID ) ]-> [ Out( skID ) ] + + /* has exactly the trivial AC variant */ + +rule (modulo E) Reveal_master_key: + [ !MSK( ~msk ) ] --[ MskRev( ) ]-> [ Out( ~msk ) ] + + /* has exactly the trivial AC variant */ + +rule (modulo E) Reveal_session_key: + [ !Sessk( ~ey, sek ) ] --[ SesskRev( ~ey ) ]-> [ Out( sek ) ] + + /* has exactly the trivial AC variant */ + +rule (modulo E) Init_1: + [ Fr( ~ex ), !LTK( $A, pmult(~s, hp($A)) ) ] + --> + [ + Init( ~ex, $A, $B, em(hp($B), pmult(~s, hp($A)))^~ex ), + Out( em(hp($B), pmult(~s, hp($A)))^~ex ) + ] + + /* + rule (modulo AC) Init_1: + [ Fr( ~ex ), !LTK( $A, pmult(~s, hp($A)) ) ] + --> + [ + Init( ~ex, $A, $B, em(hp($A), hp($B))^(~ex*~s) ), + Out( em(hp($A), hp($B))^(~ex*~s) ) + ] + */ + +rule (modulo E) Init_2: + [ Init( ~ex, $A, $B, X ), In( Y ) ] + --[ + Accept( ~ex, $A, $B, kdf() ), + Sid( ~ex, <'Init', $A, $B, X, Y> ), Match( ~ex, <'Resp', $B, $A, X, Y> ), + NotNeutral( Y ) + ]-> + [ !Sessk( ~ex, kdf() ) ] + + /* + rule (modulo AC) Init_2: + [ Init( ~ex, $A, $B, X ), In( Y ) ] + --[ + Accept( ~ex, $A, $B, kdf() ), + Sid( ~ex, <'Init', $A, $B, X, Y> ), Match( ~ex, <'Resp', $B, $A, X, Y> ), + NotNeutral( Y ) + ]-> + [ !Sessk( ~ex, kdf() ) ] + variants (modulo AC) + 1. ~ex = ~ex.10 + Y = Y.12 + z = Y.12^~ex.10 + + 2. ~ex = ~ex.11 + Y = z.14^inv(~ex.11) + z = z.14 + + 3. ~ex = ~ex.15 + Y = x.25^x.26 + z = x.25^(~ex.15*x.26) + + 4. ~ex = ~ex.17 + Y = x.29^inv((~ex.17*x.30)) + z = x.29^inv(x.30) + + 5. ~ex = ~ex.17 + Y = x.29^(x.30*inv(~ex.17)) + z = x.29^x.30 + + 6. ~ex = ~ex.18 + Y = x.30^(x.31*inv((~ex.18*x.32))) + z = x.30^(x.31*inv(x.32)) + */ + +rule (modulo E) Resp_1: + [ Fr( ~ey ), !LTK( $B, pmult(~s, hp($B)) ), In( X ) ] + --[ + Accept( ~ey, $B, $A, + kdf() + ), + Sid( ~ey, <'Resp', $B, $A, X, em(hp($A), pmult(~s, hp($B)))^~ey> ), + Match( ~ey, <'Init', $A, $B, X, em(hp($A), pmult(~s, hp($B)))^~ey> ), + NotNeutral( X ) + ]-> + [ + Out( em(hp($A), pmult(~s, hp($B)))^~ey ), + !Sessk( ~ey, kdf() ) + ] + + /* + rule (modulo AC) Resp_1: + [ Fr( ~ey ), !LTK( $B, pmult(~x, hp($B)) ), In( X ) ] + --[ + Accept( ~ey, $B, $A, kdf() ), + Sid( ~ey, <'Resp', $B, $A, X, em(hp($A), hp($B))^(~ey*~x)> ), + Match( ~ey, <'Init', $A, $B, X, em(hp($A), hp($B))^(~ey*~x)> ), + NotNeutral( X ) + ]-> + [ + Out( em(hp($A), hp($B))^(~ey*~x) ), + !Sessk( ~ey, kdf() ) + ] + variants (modulo AC) + 1. ~ey = ~ey.36 + X = X.38 + z = X.38^~ey.36 + + 2. ~ey = ~ey.36 + X = z.41^inv(~ey.36) + z = z.41 + + 3. ~ey = ~ey.372 + X = x.739^x.740 + z = x.739^(~ey.372*x.740) + + 4. ~ey = ~ey.374 + X = x.743^inv((~ey.374*x.744)) + z = x.743^inv(x.744) + + 5. ~ey = ~ey.374 + X = x.743^(x.744*inv(~ey.374)) + z = x.743^x.744 + + 6. ~ey = ~ey.375 + X = x.744^(x.745*inv((~ey.375*x.746))) + z = x.744^(x.745*inv(x.746)) + */ + +restriction notneutral: + "∀ x #i. (NotNeutral( x ) @ #i) ⇒ (¬(x = DH_neutral))" + // safety formula + +lemma key_agreement_reachable: + exists-trace + "∃ #i #j A B SID t1 t2 k. + (((Accept( t1, A, B, k ) @ #i) ∧ (Match( t1, SID ) @ #i)) ∧ + (Accept( t2, B, A, k ) @ #j)) ∧ + (Sid( t2, SID ) @ #j)" +/* +guarded formula characterizing all satisfying traces: +"∃ #i #j A B SID t1 t2 k. + (Accept( t1, A, B, k ) @ #i) ∧ + (Match( t1, SID ) @ #i) ∧ + (Accept( t2, B, A, k ) @ #j) ∧ + (Sid( t2, SID ) @ #j)" +*/ +simplify +solve( Accept( t1, A, B, k ) @ #i ) + case Init_2 + solve( Init( ~ex, $A, $B, X ) ▶₀ #i ) + case Init_1 + solve( Match( ~ex, SID ) @ #i ) + case Init_2 + solve( Accept( t2, $B, $A, + kdf() + ) @ #j ) + case Resp_1 + solve( !LTK( $B, pmult(~x, hp($B)) ) ▶₁ #j ) + case KGC_request + solve( Sid( ~ey, + <'Resp', $B, $A, em(hp($A), hp($B))^(~ex*~x), em(hp($A), hp($B))^(~ey*~x) + > + ) @ #j ) + case Resp_1 + solve( !KU( em(hp($A), hp($B))^(~ey*~x) ) @ #vk ) + case Resp_1_case_1 + solve( !KU( em(hp($A), hp($B))^(~ex*~x) ) @ #vk.1 ) + case Init_1_case_1 + SOLVED // trace found + qed + qed + qed + qed + qed + qed + qed +qed + +lemma key_secrecy: + all-traces + "∀ #i1 #i2 test A B k. + ((Accept( test, A, B, k ) @ #i1) ∧ (K( k ) @ #i2)) ⇒ + ((((∃ #i3. SesskRev( test ) @ #i3) ∨ + (∃ #i3 #i4. + ((KGCSetup( ) @ #i3) ∧ (KGCSetup( ) @ #i4)) ∧ (¬(#i3 = #i4)))) ∨ + (∃ matching #i3 #i4 sid. + ((Sid( matching, sid ) @ #i3) ∧ (Match( test, sid ) @ #i4)) ∧ + (∃ #i5. SesskRev( matching ) @ #i5))) ∨ + ((¬(∃ matching #i3 #i4 sid. + (Sid( matching, sid ) @ #i3) ∧ (Match( test, sid ) @ #i4))) ∧ + (((∃ #i5. LtkRev( B ) @ #i5) ∨ (∃ #i3. LtkRev( A ) @ #i3)) ∨ + (∃ #i3. MskRev( ) @ #i3))))" +/* +guarded formula characterizing all counter-examples: +"∃ #i1 #i2 test A B k. + (Accept( test, A, B, k ) @ #i1) ∧ (K( k ) @ #i2) + ∧ + (∀ #i3. (SesskRev( test ) @ #i3) ⇒ ⊥) ∧ + (∀ #i3 #i4. (KGCSetup( ) @ #i3) ∧ (KGCSetup( ) @ #i4) ⇒ #i3 = #i4) ∧ + (∀ matching #i3 #i4 sid. + (Sid( matching, sid ) @ #i3) ∧ (Match( test, sid ) @ #i4) + ⇒ + ∀ #i5. (SesskRev( matching ) @ #i5) ⇒ ⊥) ∧ + (((∃ matching #i3 #i4 sid. + (Sid( matching, sid ) @ #i3) ∧ (Match( test, sid ) @ #i4)) ∨ + ((∀ #i5. (LtkRev( B ) @ #i5) ⇒ ⊥) ∧ + (∀ #i3. (LtkRev( A ) @ #i3) ⇒ ⊥) ∧ + (∀ #i3. (MskRev( ) @ #i3) ⇒ ⊥))))" +*/ +simplify +solve( (∃ matching #i3 #i4 sid. + (Sid( matching, sid ) @ #i3) ∧ (Match( test, sid ) @ #i4)) ∥ + ((∀ #i5. (LtkRev( B ) @ #i5) ⇒ ⊥) ∧ + (∀ #i3. (LtkRev( A ) @ #i3) ⇒ ⊥) ∧ + (∀ #i3. (MskRev( ) @ #i3) ⇒ ⊥)) ) + case case_1 + solve( Accept( test, A, B, k ) @ #i1 ) + case Init_2 + solve( Init( ~ex, $A, $B, X ) ▶₀ #i1 ) + case Init_1 + solve( Sid( matching, sid ) @ #i3 ) + case Init_2 + solve( Init( ~ex.1, $A.1, $B.1, X ) ▶₀ #i3 ) + case Init_1 + by solve( Match( ~ex, + <'Init', $A.1, $B.1, em(hp($A.1), hp($B.1))^(~s*~ex.1), Y.1> + ) @ #i4 ) + qed + next + case Resp_1 + solve( !LTK( $B.1, pmult(~x, hp($B.1)) ) ▶₁ #i3 ) + case KGC_request + solve( Match( ~ex, + <'Resp', $B.1, $A.1, X, em(hp($A.1), hp($B.1))^(~ey*~s)> + ) @ #i4 ) + case Init_2 + solve( Init( ~ex, $A.1, $B.1, X ) ▶₀ #i4 ) + case Init_1 + solve( !KU( kdf() + ) @ #vk ) + case Reveal_session_key_case_1 + by contradiction /* from formulas */ + next + case Reveal_session_key_case_2 + by contradiction /* from formulas */ + next + case c_kdf + solve( !KU( em(hp($A), hp($B))^(~ex*~ey*~s) ) @ #vk.5 ) + case Init_1_case_1 + by solve( !KU( ~ey ) @ #vk.10 ) + next + case Init_1_case_2 + by solve( !KU( ~ey ) @ #vk.9 ) + next + case Init_1_case_3 + by solve( !KU( ~ex.1 ) @ #vk.13 ) + next + case Init_1_case_4 + by solve( !KU( ~ex.1 ) @ #vk.13 ) + next + case Init_1_case_5 + solve( !KU( ~s ) @ #vk.13 ) + case Reveal_master_key + by solve( !KU( ~ey ) @ #vk.14 ) + qed + next + case Init_1_case_6 + solve( !KU( ~s ) @ #vk.12 ) + case Reveal_master_key + by solve( !KU( ~ey ) @ #vk.13 ) + qed + next + case Resp_1_case_1 + by solve( !KU( ~ex ) @ #vk.10 ) + next + case Resp_1_case_2 + by solve( !KU( ~ex ) @ #vk.9 ) + next + case Resp_1_case_3 + by solve( !KU( ~ey.1 ) @ #vk.14 ) + next + case Resp_1_case_4 + by solve( !KU( ~ey.1 ) @ #vk.14 ) + next + case Resp_1_case_5 + solve( !KU( ~s ) @ #vk.13 ) + case Reveal_master_key + by solve( !KU( ~ex ) @ #vk.14 ) + qed + next + case Resp_1_case_6 + solve( !KU( ~s ) @ #vk.12 ) + case Reveal_master_key + by solve( !KU( ~ex ) @ #vk.13 ) + qed + next + case Reveal_ltk_case_1 + by solve( !KU( ~ex ) @ #vk.12 ) + next + case Reveal_ltk_case_2 + by solve( !KU( ~ex ) @ #vk.12 ) + next + case c_exp + by solve( !KU( ~ex ) @ #vk.12 ) + qed + qed + qed + qed + qed + qed + qed + next + case Resp_1 + solve( !LTK( $B, pmult(~x, hp($B)) ) ▶₁ #i1 ) + case KGC_request + solve( Sid( matching, sid ) @ #i3 ) + case Init_2 + solve( Init( ~ex, $A.1, $B.1, X.1 ) ▶₀ #i3 ) + case Init_1 + solve( Match( ~ey, + <'Init', $A.1, $B.1, em(hp($A.1), hp($B.1))^(~ex*~x), Y> + ) @ #i4 ) + case Resp_1 + solve( !KU( kdf() + ) @ #vk ) + case Reveal_session_key_case_1 + by contradiction /* from formulas */ + next + case Reveal_session_key_case_2 + by contradiction /* from formulas */ + next + case c_kdf + solve( !KU( em(hp($A), hp($B))^(~ex*~ey*~x) ) @ #vk.5 ) + case Init_1_case_1 + by solve( !KU( ~ey ) @ #vk.10 ) + next + case Init_1_case_2 + by solve( !KU( ~ey ) @ #vk.9 ) + next + case Init_1_case_3 + by solve( !KU( ~ex.1 ) @ #vk.13 ) + next + case Init_1_case_4 + by solve( !KU( ~ex.1 ) @ #vk.13 ) + next + case Init_1_case_5 + solve( !KU( ~x ) @ #vk.13 ) + case Reveal_master_key + by solve( !KU( ~ey ) @ #vk.14 ) + qed + next + case Init_1_case_6 + solve( !KU( ~x ) @ #vk.12 ) + case Reveal_master_key + by solve( !KU( ~ey ) @ #vk.13 ) + qed + next + case Resp_1_case_1 + by solve( !KU( ~ex ) @ #vk.10 ) + next + case Resp_1_case_2 + by solve( !KU( ~ex ) @ #vk.9 ) + next + case Resp_1_case_3 + by solve( !KU( ~ey.1 ) @ #vk.14 ) + next + case Resp_1_case_4 + by solve( !KU( ~ey.1 ) @ #vk.14 ) + next + case Resp_1_case_5 + solve( !KU( ~x ) @ #vk.13 ) + case Reveal_master_key + by solve( !KU( ~ex ) @ #vk.14 ) + qed + next + case Resp_1_case_6 + solve( !KU( ~x ) @ #vk.12 ) + case Reveal_master_key + by solve( !KU( ~ex ) @ #vk.13 ) + qed + next + case Reveal_ltk_case_1 + by solve( !KU( ~ex ) @ #vk.12 ) + next + case Reveal_ltk_case_2 + by solve( !KU( ~ex ) @ #vk.12 ) + next + case c_exp + by solve( !KU( ~ex ) @ #vk.12 ) + qed + qed + qed + qed + next + case Resp_1 + solve( !LTK( $B.1, pmult(~x.1, hp($B.1)) ) ▶₁ #i3 ) + case KGC_request + solve( Match( ~ey, + <'Resp', $B.1, $A.1, X.1, em(hp($A.1), hp($B.1))^(~x*~ey.1)> + ) @ #i4 ) + case Init_2 + by solve( Init( ~ey, $A.1, $B.1, X.1 ) ▶₀ #i4 ) + qed + qed + qed + qed + qed +next + case case_2 + solve( Accept( test, A, B, k ) @ #i1 ) + case Init_2 + solve( Init( ~ex, $A, $B, X ) ▶₀ #i1 ) + case Init_1 + solve( !KU( kdf() ) @ #vk ) + case Reveal_session_key_case_1 + by contradiction /* from formulas */ + next + case Reveal_session_key_case_2 + by contradiction /* from formulas */ + next + case c_kdf + solve( splitEqs(0) ) + case split_case_1 + solve( !KU( Y^~ex ) @ #vk.5 ) + case Init_1 + solve( !KU( ~s ) @ #vk.11 ) + case Reveal_master_key + by contradiction /* from formulas */ + qed + next + case c_exp + by solve( !KU( ~ex ) @ #vk.10 ) + qed + next + case split_case_2 + solve( !KU( z^inv(~ex) ) @ #vk.1 ) + case c_exp + by solve( !KU( ~ex ) @ #vk.11 ) + qed + next + case split_case_3 + solve( !KU( x^(~ex*x.1) ) @ #vk.5 ) + case Init_1_case_01 + solve( !KU( em(hp($A), hp($B))^~s ) @ #vk.2 ) + case Init_1_case_1 + by solve( !KU( ~ex.1 ) @ #vk.10 ) + next + case Init_1_case_2 + by solve( !KU( ~ex.1 ) @ #vk.10 ) + next + case Resp_1_case_1 + by solve( !KU( ~ey ) @ #vk.11 ) + next + case Resp_1_case_2 + by solve( !KU( ~ey ) @ #vk.11 ) + next + case Reveal_ltk_case_1 + by contradiction /* from formulas */ + next + case Reveal_ltk_case_2 + by contradiction /* from formulas */ + next + case c_exp + solve( !KU( ~s ) @ #vk.10 ) + case Reveal_master_key + by contradiction /* from formulas */ + qed + qed + next + case Init_1_case_02 + by solve( !KU( ~ex ) @ #vk.10 ) + next + case Init_1_case_03 + solve( !KU( em(hp($A), hp($B))^(~s*x) ) @ #vk.2 ) + case Init_1_case_01 + by solve( !KU( ~x ) @ #vk.10 ) + next + case Init_1_case_02 + by solve( !KU( ~x ) @ #vk.10 ) + next + case Init_1_case_03 + solve( !KU( ~s ) @ #vk.11 ) + case Reveal_master_key + by contradiction /* from formulas */ + qed + next + case Init_1_case_04 + solve( !KU( ~s ) @ #vk.12 ) + case Reveal_master_key + by contradiction /* from formulas */ + qed + next + case Init_1_case_05 + by solve( !KU( ~ex.1 ) @ #vk.12 ) + next + case Init_1_case_06 + solve( !KU( ~s ) @ #vk.11 ) + case Reveal_master_key + by contradiction /* from formulas */ + qed + next + case Init_1_case_07 + solve( !KU( ~s ) @ #vk.12 ) + case Reveal_master_key + by contradiction /* from formulas */ + qed + next + case Init_1_case_08 + by solve( !KU( ~ex.1 ) @ #vk.12 ) + next + case Init_1_case_09 + solve( !KU( ~s ) @ #vk.10 ) + case Reveal_master_key + by contradiction /* from formulas */ + qed + next + case Init_1_case_10 + by solve( !KU( ~ex.1 ) @ #vk.13 ) + next + case Init_1_case_11 + by solve( !KU( ~ex.1 ) @ #vk.13 ) + next + case Init_1_case_12 + solve( !KU( ~s ) @ #vk.10 ) + case Reveal_master_key + by contradiction /* from formulas */ + qed + next + case Init_1_case_13 + by solve( !KU( ~ex.1 ) @ #vk.13 ) + next + case Init_1_case_14 + by solve( !KU( ~ex.1 ) @ #vk.13 ) + next + case Init_1_case_15 + solve( !KU( ~s ) @ #vk.14 ) + case Reveal_master_key + by contradiction /* from formulas */ + qed + next + case Init_1_case_16 + solve( !KU( ~s ) @ #vk.14 ) + case Reveal_master_key + by contradiction /* from formulas */ + qed + next + case Init_1_case_17 + by solve( !KU( ~ex.1 ) @ #vk.14 ) + next + case Init_1_case_18 + by solve( !KU( ~ex.1 ) @ #vk.14 ) + next + case Init_1_case_19 + solve( !KU( ~s ) @ #vk.12 ) + case Reveal_master_key + by contradiction /* from formulas */ + qed + next + case Init_1_case_20 + by solve( !KU( ~ex.1 ) @ #vk.15 ) + next + case Init_1_case_21 + by solve( !KU( ~ex.1 ) @ #vk.15 ) + next + case Init_1_case_22 + solve( !KU( ~s ) @ #vk.12 ) + case Reveal_master_key + by contradiction /* from formulas */ + qed + next + case Init_1_case_23 + by solve( !KU( ~ex.1 ) @ #vk.15 ) + next + case Init_1_case_24 + by solve( !KU( ~ex.1 ) @ #vk.15 ) + next + case Init_1_case_25 + solve( !KU( ~s ) @ #vk.12 ) + case Reveal_master_key + by contradiction /* from formulas */ + qed + next + case Init_1_case_26 + solve( !KU( ~s ) @ #vk.15 ) + case Reveal_master_key + by contradiction /* from formulas */ + qed + next + case Init_1_case_27 + solve( !KU( ~s ) @ #vk.12 ) + case Reveal_master_key + by contradiction /* from formulas */ + qed + next + case Init_1_case_28 + solve( !KU( ~s ) @ #vk.15 ) + case Reveal_master_key + by contradiction /* from formulas */ + qed + next + case Resp_1_case_01 + by solve( !KU( ~x ) @ #vk.10 ) + next + case Resp_1_case_02 + by solve( !KU( ~x ) @ #vk.10 ) + next + case Resp_1_case_03 + solve( !KU( ~s ) @ #vk.12 ) + case Reveal_master_key + by contradiction /* from formulas */ + qed + next + case Resp_1_case_04 + solve( !KU( ~s ) @ #vk.13 ) + case Reveal_master_key + by contradiction /* from formulas */ + qed + next + case Resp_1_case_05 + by solve( !KU( ~ey ) @ #vk.13 ) + next + case Resp_1_case_06 + solve( !KU( ~s ) @ #vk.12 ) + case Reveal_master_key + by contradiction /* from formulas */ + qed + next + case Resp_1_case_07 + solve( !KU( ~s ) @ #vk.13 ) + case Reveal_master_key + by contradiction /* from formulas */ + qed + next + case Resp_1_case_08 + by solve( !KU( ~ey ) @ #vk.13 ) + next + case Resp_1_case_09 + solve( !KU( ~s ) @ #vk.10 ) + case Reveal_master_key + by contradiction /* from formulas */ + qed + next + case Resp_1_case_10 + by solve( !KU( ~ey ) @ #vk.14 ) + next + case Resp_1_case_11 + by solve( !KU( ~ey ) @ #vk.14 ) + next + case Resp_1_case_12 + solve( !KU( ~s ) @ #vk.10 ) + case Reveal_master_key + by contradiction /* from formulas */ + qed + next + case Resp_1_case_13 + by solve( !KU( ~ey ) @ #vk.14 ) + next + case Resp_1_case_14 + by solve( !KU( ~ey ) @ #vk.14 ) + next + case Resp_1_case_15 + solve( !KU( ~s ) @ #vk.15 ) + case Reveal_master_key + by contradiction /* from formulas */ + qed + next + case Resp_1_case_16 + solve( !KU( ~s ) @ #vk.15 ) + case Reveal_master_key + by contradiction /* from formulas */ + qed + next + case Resp_1_case_17 + by solve( !KU( ~ey ) @ #vk.15 ) + next + case Resp_1_case_18 + by solve( !KU( ~ey ) @ #vk.15 ) + next + case Resp_1_case_19 + solve( !KU( ~s ) @ #vk.13 ) + case Reveal_master_key + by contradiction /* from formulas */ + qed + next + case Resp_1_case_20 + by solve( !KU( ~ey ) @ #vk.16 ) + next + case Resp_1_case_21 + by solve( !KU( ~ey ) @ #vk.16 ) + next + case Resp_1_case_22 + solve( !KU( ~s ) @ #vk.13 ) + case Reveal_master_key + by contradiction /* from formulas */ + qed + next + case Resp_1_case_23 + by solve( !KU( ~ey ) @ #vk.16 ) + next + case Resp_1_case_24 + by solve( !KU( ~ey ) @ #vk.16 ) + next + case Resp_1_case_25 + solve( !KU( ~s ) @ #vk.13 ) + case Reveal_master_key + by contradiction /* from formulas */ + qed + next + case Resp_1_case_26 + solve( !KU( ~s ) @ #vk.16 ) + case Reveal_master_key + by contradiction /* from formulas */ + qed + next + case Resp_1_case_27 + solve( !KU( ~s ) @ #vk.13 ) + case Reveal_master_key + by contradiction /* from formulas */ + qed + next + case Resp_1_case_28 + solve( !KU( ~s ) @ #vk.16 ) + case Reveal_master_key + by contradiction /* from formulas */ + qed + next + case Reveal_ltk_case_01 + by contradiction /* from formulas */ + next + case Reveal_ltk_case_02 + by contradiction /* from formulas */ + next + case Reveal_ltk_case_03 + by contradiction /* from formulas */ + next + case Reveal_ltk_case_04 + by contradiction /* from formulas */ + next + case Reveal_ltk_case_05 + by contradiction /* from formulas */ + next + case Reveal_ltk_case_06 + by contradiction /* from formulas */ + next + case Reveal_ltk_case_07 + by contradiction /* from formulas */ + next + case Reveal_ltk_case_08 + by contradiction /* from formulas */ + next + case Reveal_ltk_case_09 + by contradiction /* non-normal bilinear pairing rule instance */ + next + case Reveal_ltk_case_10 + by contradiction /* from formulas */ + next + case Reveal_ltk_case_11 + by contradiction /* non-normal bilinear pairing rule instance */ + next + case Reveal_ltk_case_12 + by contradiction /* from formulas */ + next + case Reveal_ltk_case_13 + by contradiction /* non-normal bilinear pairing rule instance */ + next + case Reveal_ltk_case_14 + by contradiction /* from formulas */ + next + case Reveal_ltk_case_15 + by contradiction /* non-normal bilinear pairing rule instance */ + next + case Reveal_ltk_case_16 + by contradiction /* from formulas */ + next + case c_exp + solve( !KU( ~s ) @ #vk.13 ) + case Reveal_master_key + by contradiction /* from formulas */ + qed + qed + next + case Init_1_case_04 + by solve( !KU( ~ex ) @ #vk.11 ) + next + case Init_1_case_05 + by solve( !KU( ~ex ) @ #vk.11 ) + next + case Init_1_case_06 + by solve( !KU( ~ex.1 ) @ #vk.13 ) + next + case Init_1_case_07 + by solve( !KU( ~ex ) @ #vk.11 ) + next + case Init_1_case_08 + solve( !KU( ~s ) @ #vk.13 ) + case Reveal_master_key + by contradiction /* from formulas */ + qed + next + case Init_1_case_09 + solve( !KU( ~s ) @ #vk.13 ) + case Reveal_master_key + by contradiction /* from formulas */ + qed + next + case Init_1_case_10 + solve( !KU( ~s ) @ #vk.13 ) + case Reveal_master_key + by contradiction /* from formulas */ + qed + next + case Init_1_case_11 + by solve( !KU( ~ex ) @ #vk.11 ) + next + case Init_1_case_12 + by solve( !KU( ~ex.1 ) @ #vk.14 ) + next + case Init_1_case_13 + by solve( !KU( ~ex ) @ #vk.11 ) + next + case Init_1_case_14 + solve( !KU( ~s ) @ #vk.14 ) + case Reveal_master_key + by contradiction /* from formulas */ + qed + next + case Init_1_case_15 + solve( !KU( ~s ) @ #vk.14 ) + case Reveal_master_key + by contradiction /* from formulas */ + qed + next + case Resp_1_case_01 + by solve( !KU( ~ex ) @ #vk.11 ) + next + case Resp_1_case_02 + by solve( !KU( ~ex ) @ #vk.12 ) + next + case Resp_1_case_03 + by solve( !KU( ~ex ) @ #vk.12 ) + next + case Resp_1_case_04 + by solve( !KU( ~ey ) @ #vk.14 ) + next + case Resp_1_case_05 + by solve( !KU( ~ex ) @ #vk.12 ) + next + case Resp_1_case_06 + solve( !KU( ~s ) @ #vk.14 ) + case Reveal_master_key + by contradiction /* from formulas */ + qed + next + case Resp_1_case_07 + by solve( !KU( ~ex ) @ #vk.12 ) + next + case Resp_1_case_08 + by solve( !KU( ~ey ) @ #vk.15 ) + next + case Resp_1_case_09 + by solve( !KU( ~ex ) @ #vk.12 ) + next + case Resp_1_case_10 + solve( !KU( ~s ) @ #vk.15 ) + case Reveal_master_key + by contradiction /* from formulas */ + qed + next + case Reveal_ltk_case_1 + by solve( !KU( ~ex ) @ #vk.11 ) + next + case Reveal_ltk_case_2 + by solve( !KU( ~ex ) @ #vk.12 ) + next + case Reveal_ltk_case_3 + by solve( !KU( ~ex ) @ #vk.10 ) + next + case Reveal_ltk_case_4 + by solve( !KU( ~ex ) @ #vk.11 ) + next + case c_exp + by solve( !KU( ~ex ) @ #vk.12 ) + qed + next + case split_case_4 + solve( !KU( x^inv((~ex*x.1)) ) @ #vk.1 ) + case c_exp + by solve( !KU( ~ex ) @ #vk.13 ) + qed + next + case split_case_5 + solve( !KU( x^(x.1*inv(~ex)) ) @ #vk.1 ) + case Init_1_case_01 + by solve( !KU( ~ex ) @ #vk.11 ) + next + case Init_1_case_02 + by solve( !KU( ~ex ) @ #vk.13 ) + next + case Init_1_case_03 + by solve( !KU( ~ex.1 ) @ #vk.13 ) + next + case Init_1_case_04 + by solve( !KU( ~ex.1 ) @ #vk.13 ) + next + case Init_1_case_05 + solve( !KU( ~s ) @ #vk.13 ) + case Reveal_master_key + by contradiction /* from formulas */ + qed + next + case Init_1_case_06 + solve( !KU( ~s ) @ #vk.13 ) + case Reveal_master_key + by contradiction /* from formulas */ + qed + next + case Init_1_case_07 + by solve( !KU( ~ex ) @ #vk.12 ) + next + case Init_1_case_08 + by solve( !KU( ~ex ) @ #vk.12 ) + next + case Init_1_case_09 + by solve( !KU( ~ex.1 ) @ #vk.14 ) + next + case Init_1_case_10 + solve( !KU( ~s ) @ #vk.14 ) + case Reveal_master_key + by contradiction /* from formulas */ + qed + next + case Resp_1_case_01 + by solve( !KU( ~ex ) @ #vk.12 ) + next + case Resp_1_case_02 + by solve( !KU( ~ex ) @ #vk.14 ) + next + case Resp_1_case_03 + by solve( !KU( ~ey ) @ #vk.14 ) + next + case Resp_1_case_04 + by solve( !KU( ~ey ) @ #vk.14 ) + next + case Resp_1_case_05 + solve( !KU( ~s ) @ #vk.14 ) + case Reveal_master_key + by contradiction /* from formulas */ + qed + next + case Resp_1_case_06 + solve( !KU( ~s ) @ #vk.14 ) + case Reveal_master_key + by contradiction /* from formulas */ + qed + next + case Resp_1_case_07 + by solve( !KU( ~ex ) @ #vk.13 ) + next + case Resp_1_case_08 + by solve( !KU( ~ex ) @ #vk.13 ) + next + case Resp_1_case_09 + by solve( !KU( ~ey ) @ #vk.15 ) + next + case Resp_1_case_10 + solve( !KU( ~s ) @ #vk.15 ) + case Reveal_master_key + by contradiction /* from formulas */ + qed + next + case Reveal_ltk_case_1 + by solve( !KU( ~ex ) @ #vk.12 ) + next + case Reveal_ltk_case_2 + by solve( !KU( ~ex ) @ #vk.14 ) + next + case Reveal_ltk_case_3 + by solve( !KU( ~ex ) @ #vk.11 ) + next + case Reveal_ltk_case_4 + by solve( !KU( ~ex ) @ #vk.13 ) + next + case c_exp + by solve( !KU( ~ex ) @ #vk.14 ) + qed + next + case split_case_6 + solve( !KU( x^(x.1*inv((~ex*x.2))) ) @ #vk.1 ) + case Init_1_case_01 + by solve( !KU( ~ex ) @ #vk.12 ) + next + case Init_1_case_02 + by solve( !KU( ~ex ) @ #vk.14 ) + next + case Init_1_case_03 + by solve( !KU( ~ex.1 ) @ #vk.13 ) + next + case Init_1_case_04 + by solve( !KU( ~ex.1 ) @ #vk.13 ) + next + case Init_1_case_05 + solve( !KU( ~s ) @ #vk.13 ) + case Reveal_master_key + by contradiction /* from formulas */ + qed + next + case Init_1_case_06 + solve( !KU( ~s ) @ #vk.13 ) + case Reveal_master_key + by contradiction /* from formulas */ + qed + next + case Init_1_case_07 + by solve( !KU( ~ex.1 ) @ #vk.13 ) + next + case Init_1_case_08 + solve( !KU( ~s ) @ #vk.13 ) + case Reveal_master_key + by contradiction /* from formulas */ + qed + next + case Init_1_case_09 + by solve( !KU( ~ex.1 ) @ #vk.14 ) + next + case Init_1_case_10 + solve( !KU( ~s ) @ #vk.14 ) + case Reveal_master_key + by contradiction /* from formulas */ + qed + next + case Resp_1_case_01 + by solve( !KU( ~ex ) @ #vk.13 ) + next + case Resp_1_case_02 + by solve( !KU( ~ex ) @ #vk.15 ) + next + case Resp_1_case_03 + by solve( !KU( ~ey ) @ #vk.14 ) + next + case Resp_1_case_04 + by solve( !KU( ~ey ) @ #vk.14 ) + next + case Resp_1_case_05 + solve( !KU( ~s ) @ #vk.14 ) + case Reveal_master_key + by contradiction /* from formulas */ + qed + next + case Resp_1_case_06 + solve( !KU( ~s ) @ #vk.14 ) + case Reveal_master_key + by contradiction /* from formulas */ + qed + next + case Resp_1_case_07 + by solve( !KU( ~ey ) @ #vk.14 ) + next + case Resp_1_case_08 + solve( !KU( ~s ) @ #vk.14 ) + case Reveal_master_key + by contradiction /* from formulas */ + qed + next + case Resp_1_case_09 + by solve( !KU( ~ey ) @ #vk.15 ) + next + case Resp_1_case_10 + solve( !KU( ~s ) @ #vk.15 ) + case Reveal_master_key + by contradiction /* from formulas */ + qed + next + case Reveal_ltk_case_1 + by solve( !KU( ~ex ) @ #vk.13 ) + next + case Reveal_ltk_case_2 + by solve( !KU( ~ex ) @ #vk.15 ) + next + case Reveal_ltk_case_3 + by solve( !KU( ~ex ) @ #vk.12 ) + next + case Reveal_ltk_case_4 + by solve( !KU( ~ex ) @ #vk.14 ) + next + case c_exp + by solve( !KU( ~ex ) @ #vk.15 ) + qed + qed + qed + qed + next + case Resp_1 + solve( !LTK( $B, pmult(~x, hp($B)) ) ▶₁ #i1 ) + case KGC_request + solve( !KU( kdf() ) @ #vk ) + case Reveal_session_key_case_1 + by contradiction /* from formulas */ + next + case Reveal_session_key_case_2 + by contradiction /* from formulas */ + next + case c_kdf + solve( splitEqs(0) ) + case split_case_1 + solve( !KU( X^~ey ) @ #vk.5 ) + case Resp_1 + solve( !KU( ~x ) @ #vk.11 ) + case Reveal_master_key + by contradiction /* from formulas */ + qed + next + case c_exp + by solve( !KU( ~ey ) @ #vk.10 ) + qed + next + case split_case_2 + solve( !KU( z^inv(~ey) ) @ #vk.1 ) + case c_exp + by solve( !KU( ~ey ) @ #vk.11 ) + qed + next + case split_case_3 + solve( !KU( x.1^(~ey*x.2) ) @ #vk.5 ) + case Init_1_case_01 + by solve( !KU( ~ey ) @ #vk.10 ) + next + case Init_1_case_02 + by solve( !KU( ~ey ) @ #vk.11 ) + next + case Init_1_case_03 + by solve( !KU( ~ey ) @ #vk.11 ) + next + case Init_1_case_04 + by solve( !KU( ~ex ) @ #vk.13 ) + next + case Init_1_case_05 + by solve( !KU( ~ey ) @ #vk.11 ) + next + case Init_1_case_06 + solve( !KU( ~x ) @ #vk.13 ) + case Reveal_master_key + by contradiction /* from formulas */ + qed + next + case Init_1_case_07 + by solve( !KU( ~ey ) @ #vk.11 ) + next + case Init_1_case_08 + by solve( !KU( ~ex ) @ #vk.14 ) + next + case Init_1_case_09 + by solve( !KU( ~ey ) @ #vk.11 ) + next + case Init_1_case_10 + solve( !KU( ~x ) @ #vk.14 ) + case Reveal_master_key + by contradiction /* from formulas */ + qed + next + case Resp_1_case_01 + solve( !KU( em(hp($A), hp($B))^~x ) @ #vk.2 ) + case Init_1_case_1 + by solve( !KU( ~ex ) @ #vk.10 ) + next + case Init_1_case_2 + by solve( !KU( ~ex ) @ #vk.10 ) + next + case Resp_1_case_1 + by solve( !KU( ~ey.1 ) @ #vk.11 ) + next + case Resp_1_case_2 + by solve( !KU( ~ey.1 ) @ #vk.11 ) + next + case Reveal_ltk_case_1 + by contradiction /* from formulas */ + next + case Reveal_ltk_case_2 + by contradiction /* from formulas */ + next + case c_exp + solve( !KU( ~x ) @ #vk.10 ) + case Reveal_master_key + by contradiction /* from formulas */ + qed + qed + next + case Resp_1_case_02 + by solve( !KU( ~ey ) @ #vk.11 ) + next + case Resp_1_case_03 + solve( !KU( em(hp($A), hp($B))^(~x*x.1) ) @ #vk.2 ) + case Init_1_case_01 + by solve( !KU( ~x.1 ) @ #vk.10 ) + next + case Init_1_case_02 + by solve( !KU( ~x.1 ) @ #vk.10 ) + next + case Init_1_case_03 + solve( !KU( ~x ) @ #vk.11 ) + case Reveal_master_key + by contradiction /* from formulas */ + qed + next + case Init_1_case_04 + solve( !KU( ~x ) @ #vk.12 ) + case Reveal_master_key + by contradiction /* from formulas */ + qed + next + case Init_1_case_05 + by solve( !KU( ~ex ) @ #vk.12 ) + next + case Init_1_case_06 + solve( !KU( ~x ) @ #vk.11 ) + case Reveal_master_key + by contradiction /* from formulas */ + qed + next + case Init_1_case_07 + solve( !KU( ~x ) @ #vk.12 ) + case Reveal_master_key + by contradiction /* from formulas */ + qed + next + case Init_1_case_08 + by solve( !KU( ~ex ) @ #vk.12 ) + next + case Init_1_case_09 + solve( !KU( ~x ) @ #vk.10 ) + case Reveal_master_key + by contradiction /* from formulas */ + qed + next + case Init_1_case_10 + by solve( !KU( ~ex ) @ #vk.13 ) + next + case Init_1_case_11 + by solve( !KU( ~ex ) @ #vk.13 ) + next + case Init_1_case_12 + solve( !KU( ~x ) @ #vk.10 ) + case Reveal_master_key + by contradiction /* from formulas */ + qed + next + case Init_1_case_13 + by solve( !KU( ~ex ) @ #vk.13 ) + next + case Init_1_case_14 + by solve( !KU( ~ex ) @ #vk.13 ) + next + case Init_1_case_15 + solve( !KU( ~x ) @ #vk.14 ) + case Reveal_master_key + by contradiction /* from formulas */ + qed + next + case Init_1_case_16 + solve( !KU( ~x ) @ #vk.14 ) + case Reveal_master_key + by contradiction /* from formulas */ + qed + next + case Init_1_case_17 + by solve( !KU( ~ex ) @ #vk.14 ) + next + case Init_1_case_18 + by solve( !KU( ~ex ) @ #vk.14 ) + next + case Init_1_case_19 + solve( !KU( ~x ) @ #vk.12 ) + case Reveal_master_key + by contradiction /* from formulas */ + qed + next + case Init_1_case_20 + by solve( !KU( ~ex ) @ #vk.15 ) + next + case Init_1_case_21 + by solve( !KU( ~ex ) @ #vk.15 ) + next + case Init_1_case_22 + solve( !KU( ~x ) @ #vk.12 ) + case Reveal_master_key + by contradiction /* from formulas */ + qed + next + case Init_1_case_23 + by solve( !KU( ~ex ) @ #vk.15 ) + next + case Init_1_case_24 + by solve( !KU( ~ex ) @ #vk.15 ) + next + case Init_1_case_25 + solve( !KU( ~x ) @ #vk.12 ) + case Reveal_master_key + by contradiction /* from formulas */ + qed + next + case Init_1_case_26 + solve( !KU( ~x ) @ #vk.15 ) + case Reveal_master_key + by contradiction /* from formulas */ + qed + next + case Init_1_case_27 + solve( !KU( ~x ) @ #vk.12 ) + case Reveal_master_key + by contradiction /* from formulas */ + qed + next + case Init_1_case_28 + solve( !KU( ~x ) @ #vk.15 ) + case Reveal_master_key + by contradiction /* from formulas */ + qed + next + case Resp_1_case_01 + by solve( !KU( ~x.1 ) @ #vk.10 ) + next + case Resp_1_case_02 + by solve( !KU( ~x.1 ) @ #vk.10 ) + next + case Resp_1_case_03 + solve( !KU( ~x ) @ #vk.12 ) + case Reveal_master_key + by contradiction /* from formulas */ + qed + next + case Resp_1_case_04 + solve( !KU( ~x ) @ #vk.13 ) + case Reveal_master_key + by contradiction /* from formulas */ + qed + next + case Resp_1_case_05 + by solve( !KU( ~ey.1 ) @ #vk.13 ) + next + case Resp_1_case_06 + solve( !KU( ~x ) @ #vk.12 ) + case Reveal_master_key + by contradiction /* from formulas */ + qed + next + case Resp_1_case_07 + solve( !KU( ~x ) @ #vk.13 ) + case Reveal_master_key + by contradiction /* from formulas */ + qed + next + case Resp_1_case_08 + by solve( !KU( ~ey.1 ) @ #vk.13 ) + next + case Resp_1_case_09 + solve( !KU( ~x ) @ #vk.10 ) + case Reveal_master_key + by contradiction /* from formulas */ + qed + next + case Resp_1_case_10 + by solve( !KU( ~ey.1 ) @ #vk.14 ) + next + case Resp_1_case_11 + by solve( !KU( ~ey.1 ) @ #vk.14 ) + next + case Resp_1_case_12 + solve( !KU( ~x ) @ #vk.10 ) + case Reveal_master_key + by contradiction /* from formulas */ + qed + next + case Resp_1_case_13 + by solve( !KU( ~ey.1 ) @ #vk.14 ) + next + case Resp_1_case_14 + by solve( !KU( ~ey.1 ) @ #vk.14 ) + next + case Resp_1_case_15 + solve( !KU( ~x ) @ #vk.15 ) + case Reveal_master_key + by contradiction /* from formulas */ + qed + next + case Resp_1_case_16 + solve( !KU( ~x ) @ #vk.15 ) + case Reveal_master_key + by contradiction /* from formulas */ + qed + next + case Resp_1_case_17 + by solve( !KU( ~ey.1 ) @ #vk.15 ) + next + case Resp_1_case_18 + by solve( !KU( ~ey.1 ) @ #vk.15 ) + next + case Resp_1_case_19 + solve( !KU( ~x ) @ #vk.13 ) + case Reveal_master_key + by contradiction /* from formulas */ + qed + next + case Resp_1_case_20 + by solve( !KU( ~ey.1 ) @ #vk.16 ) + next + case Resp_1_case_21 + by solve( !KU( ~ey.1 ) @ #vk.16 ) + next + case Resp_1_case_22 + solve( !KU( ~x ) @ #vk.13 ) + case Reveal_master_key + by contradiction /* from formulas */ + qed + next + case Resp_1_case_23 + by solve( !KU( ~ey.1 ) @ #vk.16 ) + next + case Resp_1_case_24 + by solve( !KU( ~ey.1 ) @ #vk.16 ) + next + case Resp_1_case_25 + solve( !KU( ~x ) @ #vk.13 ) + case Reveal_master_key + by contradiction /* from formulas */ + qed + next + case Resp_1_case_26 + solve( !KU( ~x ) @ #vk.16 ) + case Reveal_master_key + by contradiction /* from formulas */ + qed + next + case Resp_1_case_27 + solve( !KU( ~x ) @ #vk.13 ) + case Reveal_master_key + by contradiction /* from formulas */ + qed + next + case Resp_1_case_28 + solve( !KU( ~x ) @ #vk.16 ) + case Reveal_master_key + by contradiction /* from formulas */ + qed + next + case Reveal_ltk_case_01 + by contradiction /* from formulas */ + next + case Reveal_ltk_case_02 + by contradiction /* from formulas */ + next + case Reveal_ltk_case_03 + by contradiction /* from formulas */ + next + case Reveal_ltk_case_04 + by contradiction /* from formulas */ + next + case Reveal_ltk_case_05 + by contradiction /* from formulas */ + next + case Reveal_ltk_case_06 + by contradiction /* from formulas */ + next + case Reveal_ltk_case_07 + by contradiction /* from formulas */ + next + case Reveal_ltk_case_08 + by contradiction /* from formulas */ + next + case Reveal_ltk_case_09 + by contradiction /* non-normal bilinear pairing rule instance */ + next + case Reveal_ltk_case_10 + by contradiction /* from formulas */ + next + case Reveal_ltk_case_11 + by contradiction /* non-normal bilinear pairing rule instance */ + next + case Reveal_ltk_case_12 + by contradiction /* from formulas */ + next + case Reveal_ltk_case_13 + by contradiction /* non-normal bilinear pairing rule instance */ + next + case Reveal_ltk_case_14 + by contradiction /* from formulas */ + next + case Reveal_ltk_case_15 + by contradiction /* non-normal bilinear pairing rule instance */ + next + case Reveal_ltk_case_16 + by contradiction /* from formulas */ + next + case c_exp + solve( !KU( ~x ) @ #vk.13 ) + case Reveal_master_key + by contradiction /* from formulas */ + qed + qed + next + case Resp_1_case_04 + by solve( !KU( ~ey ) @ #vk.12 ) + next + case Resp_1_case_05 + by solve( !KU( ~ey ) @ #vk.12 ) + next + case Resp_1_case_06 + by solve( !KU( ~ey.1 ) @ #vk.14 ) + next + case Resp_1_case_07 + by solve( !KU( ~ey ) @ #vk.12 ) + next + case Resp_1_case_08 + solve( !KU( ~x ) @ #vk.13 ) + case Reveal_master_key + by contradiction /* from formulas */ + qed + next + case Resp_1_case_09 + solve( !KU( ~x ) @ #vk.14 ) + case Reveal_master_key + by contradiction /* from formulas */ + qed + next + case Resp_1_case_10 + solve( !KU( ~x ) @ #vk.13 ) + case Reveal_master_key + by contradiction /* from formulas */ + qed + next + case Resp_1_case_11 + by solve( !KU( ~ey ) @ #vk.12 ) + next + case Resp_1_case_12 + by solve( !KU( ~ey.1 ) @ #vk.15 ) + next + case Resp_1_case_13 + by solve( !KU( ~ey ) @ #vk.12 ) + next + case Resp_1_case_14 + solve( !KU( ~x ) @ #vk.15 ) + case Reveal_master_key + by contradiction /* from formulas */ + qed + next + case Resp_1_case_15 + solve( !KU( ~x ) @ #vk.14 ) + case Reveal_master_key + by contradiction /* from formulas */ + qed + next + case Reveal_ltk_case_1 + by solve( !KU( ~ey ) @ #vk.11 ) + next + case Reveal_ltk_case_2 + by solve( !KU( ~ey ) @ #vk.12 ) + next + case Reveal_ltk_case_3 + by solve( !KU( ~ey ) @ #vk.10 ) + next + case Reveal_ltk_case_4 + by solve( !KU( ~ey ) @ #vk.11 ) + next + case c_exp + by solve( !KU( ~ey ) @ #vk.12 ) + qed + next + case split_case_4 + solve( !KU( x.1^inv((~ey*x.2)) ) @ #vk.1 ) + case c_exp + by solve( !KU( ~ey ) @ #vk.13 ) + qed + next + case split_case_5 + solve( !KU( x.1^(x.2*inv(~ey)) ) @ #vk.1 ) + case Init_1_case_01 + by solve( !KU( ~ey ) @ #vk.11 ) + next + case Init_1_case_02 + by solve( !KU( ~ey ) @ #vk.13 ) + next + case Init_1_case_03 + by solve( !KU( ~ex ) @ #vk.13 ) + next + case Init_1_case_04 + by solve( !KU( ~ex ) @ #vk.13 ) + next + case Init_1_case_05 + solve( !KU( ~x ) @ #vk.13 ) + case Reveal_master_key + by contradiction /* from formulas */ + qed + next + case Init_1_case_06 + solve( !KU( ~x ) @ #vk.13 ) + case Reveal_master_key + by contradiction /* from formulas */ + qed + next + case Init_1_case_07 + by solve( !KU( ~ey ) @ #vk.12 ) + next + case Init_1_case_08 + by solve( !KU( ~ey ) @ #vk.12 ) + next + case Init_1_case_09 + by solve( !KU( ~ex ) @ #vk.14 ) + next + case Init_1_case_10 + solve( !KU( ~x ) @ #vk.14 ) + case Reveal_master_key + by contradiction /* from formulas */ + qed + next + case Resp_1_case_01 + by solve( !KU( ~ey ) @ #vk.12 ) + next + case Resp_1_case_02 + by solve( !KU( ~ey ) @ #vk.14 ) + next + case Resp_1_case_03 + by solve( !KU( ~ey.1 ) @ #vk.14 ) + next + case Resp_1_case_04 + by solve( !KU( ~ey.1 ) @ #vk.14 ) + next + case Resp_1_case_05 + solve( !KU( ~x ) @ #vk.14 ) + case Reveal_master_key + by contradiction /* from formulas */ + qed + next + case Resp_1_case_06 + solve( !KU( ~x ) @ #vk.14 ) + case Reveal_master_key + by contradiction /* from formulas */ + qed + next + case Resp_1_case_07 + by solve( !KU( ~ey ) @ #vk.13 ) + next + case Resp_1_case_08 + by solve( !KU( ~ey ) @ #vk.13 ) + next + case Resp_1_case_09 + by solve( !KU( ~ey.1 ) @ #vk.15 ) + next + case Resp_1_case_10 + solve( !KU( ~x ) @ #vk.15 ) + case Reveal_master_key + by contradiction /* from formulas */ + qed + next + case Reveal_ltk_case_1 + by solve( !KU( ~ey ) @ #vk.12 ) + next + case Reveal_ltk_case_2 + by solve( !KU( ~ey ) @ #vk.14 ) + next + case Reveal_ltk_case_3 + by solve( !KU( ~ey ) @ #vk.11 ) + next + case Reveal_ltk_case_4 + by solve( !KU( ~ey ) @ #vk.13 ) + next + case c_exp + by solve( !KU( ~ey ) @ #vk.14 ) + qed + next + case split_case_6 + solve( !KU( x.1^(x.2*inv((~ey*x.3))) ) @ #vk.1 ) + case Init_1_case_01 + by solve( !KU( ~ey ) @ #vk.12 ) + next + case Init_1_case_02 + by solve( !KU( ~ey ) @ #vk.14 ) + next + case Init_1_case_03 + by solve( !KU( ~ex ) @ #vk.13 ) + next + case Init_1_case_04 + by solve( !KU( ~ex ) @ #vk.13 ) + next + case Init_1_case_05 + solve( !KU( ~x ) @ #vk.13 ) + case Reveal_master_key + by contradiction /* from formulas */ + qed + next + case Init_1_case_06 + solve( !KU( ~x ) @ #vk.13 ) + case Reveal_master_key + by contradiction /* from formulas */ + qed + next + case Init_1_case_07 + by solve( !KU( ~ex ) @ #vk.13 ) + next + case Init_1_case_08 + solve( !KU( ~x ) @ #vk.13 ) + case Reveal_master_key + by contradiction /* from formulas */ + qed + next + case Init_1_case_09 + by solve( !KU( ~ex ) @ #vk.14 ) + next + case Init_1_case_10 + solve( !KU( ~x ) @ #vk.14 ) + case Reveal_master_key + by contradiction /* from formulas */ + qed + next + case Resp_1_case_01 + by solve( !KU( ~ey ) @ #vk.13 ) + next + case Resp_1_case_02 + by solve( !KU( ~ey ) @ #vk.15 ) + next + case Resp_1_case_03 + by solve( !KU( ~ey.1 ) @ #vk.14 ) + next + case Resp_1_case_04 + by solve( !KU( ~ey.1 ) @ #vk.14 ) + next + case Resp_1_case_05 + solve( !KU( ~x ) @ #vk.14 ) + case Reveal_master_key + by contradiction /* from formulas */ + qed + next + case Resp_1_case_06 + solve( !KU( ~x ) @ #vk.14 ) + case Reveal_master_key + by contradiction /* from formulas */ + qed + next + case Resp_1_case_07 + by solve( !KU( ~ey.1 ) @ #vk.14 ) + next + case Resp_1_case_08 + solve( !KU( ~x ) @ #vk.14 ) + case Reveal_master_key + by contradiction /* from formulas */ + qed + next + case Resp_1_case_09 + by solve( !KU( ~ey.1 ) @ #vk.15 ) + next + case Resp_1_case_10 + solve( !KU( ~x ) @ #vk.15 ) + case Reveal_master_key + by contradiction /* from formulas */ + qed + next + case Reveal_ltk_case_1 + by solve( !KU( ~ey ) @ #vk.13 ) + next + case Reveal_ltk_case_2 + by solve( !KU( ~ey ) @ #vk.15 ) + next + case Reveal_ltk_case_3 + by solve( !KU( ~ey ) @ #vk.12 ) + next + case Reveal_ltk_case_4 + by solve( !KU( ~ey ) @ #vk.14 ) + next + case c_exp + by solve( !KU( ~ey ) @ #vk.15 ) + qed + qed + qed + qed + qed +qed + +/* All well-formedness checks were successful. */ + +end +/* Output +maude tool: 'maude' + checking version: 3.0. OK. + checking installation: OK. + + +analyzing: examples/ake/bilinear/Scott.spthy + +------------------------------------------------------------------------------ +analyzed: examples/ake/bilinear/Scott.spthy + + output: examples/ake/bilinear/Scott.spthy.tmp + processing time: 21.595820781s + key_agreement_reachable (exists-trace): verified (10 steps) + key_secrecy (all-traces): verified (518 steps) + +------------------------------------------------------------------------------ + +============================================================================== +summary of summaries: + +analyzed: examples/ake/bilinear/Scott.spthy + + output: examples/ake/bilinear/Scott.spthy.tmp + processing time: 21.595820781s + key_agreement_reachable (exists-trace): verified (10 steps) + key_secrecy (all-traces): verified (518 steps) + +============================================================================== +*/