tamarin-prover 0.8.2.1 → 0.8.4.0
raw patch · 37 files changed
+4869/−102 lines, 37 filesdep ~cmdargsdep ~tamarin-prover-termdep ~tamarin-prover-theorynew-uploader
Dependency ranges changed: cmdargs, tamarin-prover-term, tamarin-prover-theory, tamarin-prover-utils
Files
- data/CHANGES +34/−0
- data/examples/ake/bilinear/Chen_Kudla.spthy +250/−0
- data/examples/ake/bilinear/Chen_Kudla_eCK.spthy +251/−0
- data/examples/ake/bilinear/Joux.spthy +75/−0
- data/examples/ake/bilinear/Joux_EphkRev.spthy +82/−0
- data/examples/ake/bilinear/README +4/−0
- data/examples/ake/bilinear/RYY.spthy +152/−0
- data/examples/ake/bilinear/RYY_PFS.spthy +152/−0
- data/examples/ake/bilinear/Scott.spthy +161/−0
- data/examples/ake/bilinear/Scott_EphkRev.spthy +174/−0
- data/examples/ake/bilinear/TAK1.spthy +124/−0
- data/examples/ake/bilinear/TAK1_eCK_like.spthy +130/−0
- data/examples/ake/dh/DHKEA_NAXOS_C_eCK_PFS_keyreg_partially_matching.spthy +227/−0
- data/examples/ake/dh/DHKEA_NAXOS_C_eCK_PFS_partially_matching.spthy +221/−0
- data/examples/ake/dh/NAXOS_eCK.spthy +148/−0
- data/examples/ake/dh/NAXOS_eCK_PFS.spthy +149/−0
- data/examples/ake/dh/UM_one_pass_attack.spthy +208/−0
- data/examples/ake/dh/UM_one_pass_fix.spthy +224/−0
- data/examples/ake/dh/UM_three_pass.spthy +244/−0
- data/examples/ake/dh/UM_three_pass_combined.spthy +309/−0
- data/examples/ake/dh/UM_three_pass_combined_fixed.spthy +356/−0
- data/examples/ake/dh/client_session_key.aes +1/−0
- data/examples/cav13/DH_example.spthy +36/−0
- data/examples/features/multiset/counter.spthy +38/−0
- data/examples/features/private_function_symbols/NAXOS_eCK_PFS_private.spthy +147/−0
- data/examples/features/private_function_symbols/NAXOS_eCK_private.spthy +146/−0
- data/examples/related_work/YubiSecure_KS_STM12/Yubikey.spthy +12/−0
- data/examples/related_work/YubiSecure_KS_STM12/Yubikey_and_YubiHSM.spthy +43/−8
- data/examples/thesis-benedikt/running-examples/DH_Message_Deduction.spthy +38/−0
- data/examples/thesis-benedikt/running-examples/UM_one_pass_eCK_like.spthy +93/−0
- data/examples/thesis-benedikt/running-examples/UM_one_pass_private.spthy +70/−0
- data/intruder_variants_bp.spthy +407/−0
- data/intruder_variants_dh.spthy +59/−59
- src/Main/Console.hs +1/−0
- src/Main/Mode/Intruder.hs +17/−22
- src/Main/TheoryLoader.hs +44/−6
- tamarin-prover.cabal +42/−7
data/CHANGES view
@@ -1,3 +1,37 @@+* 0.8.4+ features:+ 1. irreducible function symbols are now allowed in formulas+ 2. Support for an AC operator "+" which can also be used+ in formulas.+ See the examples+ - "ake/bilinear/{Joux,TAK1}.spthy" for modeling multisets,+ - "features/multiset/counter.spthy" for modeling natural+ numbers as counters, and+ - "ake/dh/DHKEA_NAXOS_C_eCK_PFS_partially_matching.spthy" for+ modeling lists with an "isPrefixOf" operation.+ See below for documentation.+ 3. Support for reasoning about protocols that use bilinear pairing+ (see "ake/bilinear/" for examples).+ 4. Support for private function symbols (see "cav13/DH_example.spthy"+ and "features/private_function_symbols/" for examples.++ documentation:+ - Schmidt's PhD thesis on "Formal Analysis of Key Exchange and Physical+ Protocols" is now available online at++ http://www.infsec.ethz.ch/research/software/tamarin++ and provides a detailed explanation of the theory and application of+ Tamarin including the reasoning about Diffie-Hellman exponentiation+ and bilinear pairing.++ new protocol models (most of them referenced in Schmidt's thesis):+ - Identity-based key exchange protocols (RYY, Scott, Chen-Kudla)+ - tripartite group key exchange protocols (Joux, TAK1)+ - multiprotocol scenarios for 3-pass AKE protocols (DHKEA+NAXOS-C, UM-C+UM-1)+ - new Yubikey models that model counters with multisets (contributed by+ Robert Künnemann).+ * 0.8.2.1 bugfix release Should fix the ominous "no such lemma or proof path" GUI bug.
+ data/examples/ake/bilinear/Chen_Kudla.spthy view
@@ -0,0 +1,250 @@+theory Chen_Kudla+begin++builtins: bilinear-pairing++functions: kdf/1, hp/1, h/1++section{* A variant of the Chen-Kudla protocol that uses ordered concatenation instead + addition of points *}++/*+ * Protocol: Chen-Kudla (with concatenation)+ * Modeler: Benedikt Schmidt+ * Date: May 2012+ * Source: Boyd overview identity based key exchange protocols+ *+ * Status: Working+ */+++// Key generation center++rule KGC_Setup:+ let mpk = pmult(~msk,'P')+ in+ [ Fr(~msk) ]+ --[ KGCSetup() ]->+ [ !MSK( ~msk )+ , !MPK( mpk )+ , Out( mpk )+ ]++rule KGC_request:+ [ !MSK( ~msk ) ]+ -->+ [ !LTK( $ID, pmult(~msk, hp($ID)) ) ]+++// Reveals++rule Reveal_ltk:+ [ !LTK( $ID, skID ) ]+ --[ LtkRev($ID) ]->+ [ Out(skID) ]++rule Reveal_master_key:+ [ !MSK( ~msk ) ]+ --[ MskRev() ]->+ [ Out( ~msk ) ]+++rule Reveal_session_key:+ [ !Sessk( ~ey, kdf(sek) ) ]+ --[ SesskRev( ~ey ) ]->+ [ Out( kdf(sek) ) ]+++rule Reveal_ephemeral_key:+ [ !Ephk( ~ex ) ]+ --[ EphkRev( ~ex ) ]->+ [ Out( ~ex ) ]++// Protocol++rule Init_1:+ let X = pmult(~ex,'P')+ in+ [ Fr( ~ex )+ ]+ -->+ [ Init( ~ex, $A, $B )+ , Out( X )+ , !Ephk( ~ex )+ ]++rule Init_2:+ let skA = pmult(~s1, hp($A))+ mpk = pmult(~s2,'P')+ X = pmult(~ex,'P')+ sessKey = kdf( em(hp($B), mpk)^~ex, em(skA, Y), pmult(~ex,Y), $A, $B, X, Y )+ in+ [ Init( ~ex, $A, $B )+ , !MPK( mpk )+ , !LTK( $A, skA )+ , In( Y )+ ]+ --[ Accept( ~ex, $A, $B, sessKey )+ , Sid( ~ex, <'Init',$A,$B,X,Y> )+ // a matching session for ~ex has the following sid+ , Match( ~ex, <'Resp',$B,$A,X,Y> )+ ]->+ [ !Sessk( ~ex, sessKey ) ]++rule Resp_1:+ let skB = pmult(~msk, hp($B))+ mpk = pmult(~msk, 'P')+ Y = pmult(~ey,'P')+ // instead of multiplying the two em-terms, we concatenate them+ sessKey = kdf( em(skB, X), em(hp($A), mpk)^~ey, pmult(~ey,X), $A, $B, X, Y)+ in+ [ Fr( ~ey )+ , !LTK( $B, skB )+ , !MPK( mpk )+ , In( X )+ ]+ --[ Accept( ~ey, $B, $A, sessKey )+ , Sid( ~ey, <'Resp',$B,$A,X,Y> )+ // a matching session for ~ey has the following sid+ , Match( ~ey, <'Init',$A,$B,X,Y> )+ ]->+ [ Out( Y )+ , !Sessk( ~ey, sessKey )+ , !Ephk(~ey)+ ]++lemma key_agreement_reachable:+ exists-trace+ "Ex #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"+++lemma key_secrecy_ephemeral_no_WPFS:+ /* + * If there exists a Test session whose key k is known to the+ * Adversary, then...+ */+ "(All #i1 #i2 test A B k.+ Accept(test, A, B, k) @ i1 & K( k ) @ i2+ ==> ( + // ... the test session must be "not clean".+ // test is not clean if one of the following has happened:+ //+ // session-key-reveal of test thread.+ (Ex #i3. SesskRev( test ) @ i3 )+ + // more than one KGCSetup+ | (Ex #i3 #i4. KGCSetup() @ i3 & KGCSetup() @ i4 & not (#i3 = #i4))+ + // there is a matching session+ | (Ex matching #i3 #i4 sid.+ // matching's 'sid' info matches with test+ ( Sid ( matching, sid ) @ i3 & Match( test, sid ) @ i4)+ & ( + // matching's session key was revealed+ (Ex #i5. SesskRev( matching ) @ i5 )++ // (matching's longterm key or master key) and ephemeral key was revealed+ | ( ((Ex #i5. LtkRev( B ) @ i5 ) | (Ex #i5. MskRev() @ i5 ))+ & (Ex #i5. EphkRev( matching ) @ i5 ))++ // both ephemeral keys are revealed, this is allowed in eCK+ // the corresponding attack uses em(hp(A),mpk)^ekmatch ...+ | ( (Ex #i5. EphkRev( matching ) @ i5 )+ & (Ex #i5. EphkRev( test ) @ i5 )+ )++ // (test's longterm key or master key) and ephemeral key was revealed+ | ( ((Ex #i5. LtkRev( A ) @ i5 ) | (Ex #i5. MskRev() @ i5 ))+ & (Ex #i5. EphkRev( test ) @ i5 ))++ )+ )++ // there is no matching session+ | ( (not (Ex matching #i3 #i4 sid.+ // matching's 'sid' info matches with test+ ( Sid ( matching, sid ) @ i3 & Match( test, sid ) @ i4)))++ & ( + // the longterm key of test.peer was revealed+ (Ex #i5. LtkRev( B ) @ i5 )++ // the ephemeral key of test was revealed+ // in eCK, this would be allowed as long as the longterm key of test is not revealed.+ | (Ex #i3. EphkRev( test ) @ i3 )+ + // the master key was revealed+ | (Ex #i3. MskRev() @ i3)+ )+ )++ )+ )"++/*+/* For this property, there is an attack where+ both ephemeral keys are revealed.+*/+lemma key_secrecy_eCK_like:+ /* + * If there exists a Test session whose key k is known to the+ * Adversary, then...+ */+ "(All #i1 #i2 test A B k.+ Accept(test, A, B, k) @ i1 & K( k ) @ i2+ ==> ( + // ... the test session must be "not clean".+ // test is not clean if one of the following has happened:+ //+ // session-key-reveal of test thread.+ (Ex #i3. SesskRev( test ) @ i3 )+ + // more than one KGCSetup+ | (Ex #i3 #i4. KGCSetup() @ i3 & KGCSetup() @ i4 & not (#i3 = #i4))+ + // there is a matching session+ | (Ex matching #i3 #i4 sid.+ // matching's 'sid' info matches with test+ ( Sid ( matching, sid ) @ i3 & Match( test, sid ) @ i4)+ & ( + // matching's session key was revealed+ (Ex #i5. SesskRev( matching ) @ i5 )++ // (matching's longterm key or master key) and ephemeral key was revealed+ | ( ((Ex #i5. LtkRev( B ) @ i5 ) | (Ex #i5. MskRev() @ i5 ))+ & (Ex #i5. EphkRev( matching ) @ i5 ))++ // (test's longterm key or master key) and ephemeral key was revealed+ | ( ((Ex #i5. LtkRev( A ) @ i5 ) | (Ex #i5. MskRev() @ i5 ))+ & (Ex #i5. EphkRev( test ) @ i5 ))++ )+ )++ // there is no matching session+ | ( (not (Ex matching #i3 #i4 sid.+ // matching's 'sid' info matches with test+ ( Sid ( matching, sid ) @ i3 & Match( test, sid ) @ i4)))++ & ( + // the longterm key of test.peer was revealed+ (Ex #i5. LtkRev( B ) @ i5 )++ // the ephemeral key of test was revealed+ // in eCK, this would be allowed as long as the longterm key of test is not revealed.+ | (Ex #i3. EphkRev( test ) @ i3 )+ + // the master key was revealed+ | (Ex #i3. MskRev() @ i3)+ )+ )++ )+ )"+*/++end
+ data/examples/ake/bilinear/Chen_Kudla_eCK.spthy view
@@ -0,0 +1,251 @@+theory Chen_Kudla+begin++builtins: bilinear-pairing++functions: kdf/1, hp/1, h/1++section{* A variant of the Chen-Kudla protocol that uses ordered concatenation instead + addition of points *}++/*+ * Protocol: Chen-Kudla (with concatenation)+ * Modeler: Benedikt Schmidt+ * Date: May 2012+ * Source: Boyd overview identity based key exchange protocols+ *+ * Status: Working+ */+++// Key generation center++rule KGC_Setup:+ let mpk = pmult(~msk,'P')+ in+ [ Fr(~msk) ]+ --[ KGCSetup() ]->+ [ !MSK( ~msk )+ , !MPK( mpk )+ , Out( mpk )+ ]++rule KGC_request:+ [ !MSK( ~msk ) ]+ -->+ [ !LTK( $ID, pmult(~msk, hp($ID)) ) ]+++// Reveals++rule Reveal_ltk:+ [ !LTK( $ID, skID ) ]+ --[ LtkRev($ID) ]->+ [ Out(skID) ]++rule Reveal_master_key:+ [ !MSK( ~msk ) ]+ --[ MskRev() ]->+ [ Out( ~msk ) ]+++rule Reveal_session_key:+ [ !Sessk( ~ey, kdf(sek) ) ]+ --[ SesskRev( ~ey ) ]->+ [ Out( kdf(sek) ) ]+++rule Reveal_ephemeral_key:+ [ !Ephk( ~ex ) ]+ --[ EphkRev( ~ex ) ]->+ [ Out( ~ex ) ]++// Protocol++rule Init_1:+ let X = pmult(~ex,'P')+ in+ [ Fr( ~ex )+ ]+ -->+ [ Init( ~ex, $A, $B )+ , Out( X )+ , !Ephk( ~ex )+ ]++rule Init_2:+ let skA = pmult(~s1, hp($A))+ mpk = pmult(~s2,'P')+ X = pmult(~ex,'P')+ sessKey = kdf( em(hp($B), mpk)^~ex, em(skA, Y), pmult(~ex,Y), $A, $B, X, Y )+ in+ [ Init( ~ex, $A, $B )+ , !MPK( mpk )+ , !LTK( $A, skA )+ , In( Y )+ ]+ --[ Accept( ~ex, $A, $B, sessKey )+ , Sid( ~ex, <'Init',$A,$B,X,Y> )+ // a matching session for ~ex has the following sid+ , Match( ~ex, <'Resp',$B,$A,X,Y> )+ ]->+ [ !Sessk( ~ex, sessKey ) ]++rule Resp_1:+ let skB = pmult(~msk, hp($B))+ mpk = pmult(~msk, 'P')+ Y = pmult(~ey,'P')+ // instead of multiplying the two em-terms, we concatenate them+ sessKey = kdf( em(skB, X), em(hp($A), mpk)^~ey, pmult(~ey,X), $A, $B, X, Y)+ in+ [ Fr( ~ey )+ , !LTK( $B, skB )+ , !MPK( mpk )+ , In( X )+ ]+ --[ Accept( ~ey, $B, $A, sessKey )+ , Sid( ~ey, <'Resp',$B,$A,X,Y> )+ // a matching session for ~ey has the following sid+ , Match( ~ey, <'Init',$A,$B,X,Y> )+ ]->+ [ Out( Y )+ , !Sessk( ~ey, sessKey )+ , !Ephk(~ey)+ ]++/*+lemma key_agreement_reachable:+ exists-trace+ "Ex #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"+*/++/*+lemma key_secrecy_ephemeral_no_WPFS:+ /* + * If there exists a Test session whose key k is known to the+ * Adversary, then...+ */+ "(All #i1 #i2 test A B k.+ Accept(test, A, B, k) @ i1 & K( k ) @ i2+ ==> ( + // ... the test session must be "not clean".+ // test is not clean if one of the following has happened:+ //+ // session-key-reveal of test thread.+ (Ex #i3. SesskRev( test ) @ i3 )+ + // more than one KGCSetup+ | (Ex #i3 #i4. KGCSetup() @ i3 & KGCSetup() @ i4 & not (#i3 = #i4))+ + // there is a matching session+ | (Ex matching #i3 #i4 sid.+ // matching's 'sid' info matches with test+ ( Sid ( matching, sid ) @ i3 & Match( test, sid ) @ i4)+ & ( + // matching's session key was revealed+ (Ex #i5. SesskRev( matching ) @ i5 )++ // (matching's longterm key or master key) and ephemeral key was revealed+ | ( ((Ex #i5. LtkRev( B ) @ i5 ) | (Ex #i5. MskRev() @ i5 ))+ & (Ex #i5. EphkRev( matching ) @ i5 ))++ // both ephemeral keys are revealed, this is allowed in eCK+ // the corresponding attack uses em(hp(A),mpk)^ekmatch ...+ | ( (Ex #i5. EphkRev( matching ) @ i5 )+ & (Ex #i5. EphkRev( test ) @ i5 )+ )++ // (test's longterm key or master key) and ephemeral key was revealed+ | ( ((Ex #i5. LtkRev( A ) @ i5 ) | (Ex #i5. MskRev() @ i5 ))+ & (Ex #i5. EphkRev( test ) @ i5 ))++ )+ )++ // there is no matching session+ | ( (not (Ex matching #i3 #i4 sid.+ // matching's 'sid' info matches with test+ ( Sid ( matching, sid ) @ i3 & Match( test, sid ) @ i4)))++ & ( + // the longterm key of test.peer was revealed+ (Ex #i5. LtkRev( B ) @ i5 )++ // the ephemeral key of test was revealed+ // in eCK, this would be allowed as long as the longterm key of test is not revealed.+ | (Ex #i3. EphkRev( test ) @ i3 )+ + // the master key was revealed+ | (Ex #i3. MskRev() @ i3)+ )+ )++ )+ )"+*/++/* For this property, there is an attack where+ both ephemeral keys are revealed.+*/+lemma key_secrecy_eCK_like:+ /* + * If there exists a Test session whose key k is known to the+ * Adversary, then...+ */+ "(All #i1 #i2 test A B k.+ Accept(test, A, B, k) @ i1 & K( k ) @ i2+ ==> ( + // ... the test session must be "not clean".+ // test is not clean if one of the following has happened:+ //+ // session-key-reveal of test thread.+ (Ex #i3. SesskRev( test ) @ i3 )+ + // more than one KGCSetup+ | (Ex #i3 #i4. KGCSetup() @ i3 & KGCSetup() @ i4 & not (#i3 = #i4))+ + // there is a matching session+ | (Ex matching #i3 #i4 sid.+ // matching's 'sid' info matches with test+ ( Sid ( matching, sid ) @ i3 & Match( test, sid ) @ i4)+ & ( + // matching's session key was revealed+ (Ex #i5. SesskRev( matching ) @ i5 )++ // (matching's longterm key or master key) and ephemeral key was revealed+ | ( ((Ex #i5. LtkRev( B ) @ i5 ) | (Ex #i5. MskRev() @ i5 ))+ & (Ex #i5. EphkRev( matching ) @ i5 ))++ // (test's longterm key or master key) and ephemeral key was revealed+ | ( ((Ex #i5. LtkRev( A ) @ i5 ) | (Ex #i5. MskRev() @ i5 ))+ & (Ex #i5. EphkRev( test ) @ i5 ))++ )+ )++ // there is no matching session+ | ( (not (Ex matching #i3 #i4 sid.+ // matching's 'sid' info matches with test+ ( Sid ( matching, sid ) @ i3 & Match( test, sid ) @ i4)))++ & ( + // the longterm key of test.peer was revealed+ (Ex #i5. LtkRev( B ) @ i5 )++ // the ephemeral key of test was revealed+ // in eCK, this would be allowed as long as the longterm key of test is not revealed.+ | (Ex #i3. EphkRev( test ) @ i3 )+ + // the master key was revealed+ | (Ex #i3. MskRev() @ i3)+ )+ )++ )+ )"++end
+ data/examples/ake/bilinear/Joux.spthy view
@@ -0,0 +1,75 @@+theory Joux+begin++section{* The Joux Protocol using Signatures*}++/*+ * Protocol: The Joux Protocol.+ * Source: "A One Round Protocol for Tripartite Diffie-Hellman"+ * A. Joux+ * Modeler: Benedikt Schmidt+ * Date: July 2012+ *+ * Model: PFS+ * Status: working+ */++builtins: bilinear-pairing, signing, multiset++// Public key infrastructure+rule Register_pk:+ [ Fr(~ltk) ] + --[ ]-> + [ !Ltk($A, ~ltk), !Pk($A, pk(~ltk)), Out(pk(~ltk)) ]++// Reveals+rule Reveal_ltk:+ [ !Ltk(A, ltk) ]+ --[ LtkReveal(A) ]->+ [ Out(ltk) ]+++// Protocol+rule Proto1:+ let hkA = pmult(~ekA ,'P')+ in+ [ Fr(~ekA), !Ltk($A, ltkA) ]+ --[ ]->+ [ PState( $A, $B + $C, ~ekA )+ , Out( <hkA, sign{$A, $B + $C, hkA }ltkA> )+ ]++rule Proto2:+ [ PState( $A, $B + $C, ~ekA)+ , !Pk($B, pk(ltkB))+ , !Pk($C, pk(ltkC))+ , In( < XB, sign{$B, $A + $C, XB}ltkB > )+ , In( < XC, sign{$C, $A + $B, XC}ltkC > )+ ]+ --[ SessionKey($A, $B + $C, em(XB,XC) ^ ~ekA) ]->+ []++lemma session_key_establish:+ exists-trace+ "Ex A B C #ia #ib #ic k.+ ( SessionKey(A,B + C, k) @ ia &+ SessionKey(B,C + A, k) @ ib &+ SessionKey(C,B + A, k) @ ic &+ not (A = B) &+ not (B = C) &+ not (A = C) &+ not ( Ex #j. LtkReveal(A) @ j ) &+ not ( Ex #j. LtkReveal(B) @ j ) &+ not ( Ex #j. LtkReveal(C) @ j ))"+++lemma Session_Key_Secrecy_PFS:+ "(All A B C sessKey #i #k. + SessionKey(A,B + C,sessKey) @ i &+ K(sessKey) @ k+ ==>+ (Ex #l. LtkReveal(A) @ l & l < i )+ | (Ex #l. LtkReveal(B) @ l & l < i )+ | (Ex #l. LtkReveal(C) @ l & l < i ))"++end
+ data/examples/ake/bilinear/Joux_EphkRev.spthy view
@@ -0,0 +1,82 @@+theory Joux_EphkRev+begin++section{* The Joux Protocol using Signatures*}++/*+ * Protocol: The Joux Protocol.+ * Source: "A One Round Protocol for Tripartite Diffie-Hellman"+ * A. Joux+ * Modeler: Benedikt Schmidt+ * Date: July 2012+ *+ * Model: PFS with ephemeral key reveals+ * Status: working+ */++builtins: bilinear-pairing, signing, multiset++// Public key infrastructure+rule Register_pk:+ [ Fr(~ltk) ] + --[ ]-> + [ !Ltk($A, ~ltk), !Pk($A, pk(~ltk)), Out(pk(~ltk)) ]++// Reveals+rule Reveal_ltk:+ [ !Ltk(A, ltk) ]+ --[ LtkReveal(A) ]->+ [ Out(ltk) ]+++// Protocol+rule Proto1:+ let hkA = pmult(~ekA ,'P')+ in+ [ Fr(~ekA), !Ltk($A, ltkA) ]+ --[ ]->+ [ PState( $A, $B + $C, ~ekA )+ , Out( <hkA, sign{$A, $B + $C, hkA }ltkA> )+ , !Ephk( ~ekA)+ ]++rule Proto2:+ [ PState( $A, $B + $C, ~ekA)+ , !Pk($B, pk(ltkB))+ , !Pk($C, pk(ltkC))+ , In( < XB, sign{$B, $A + $C, XB}ltkB > )+ , In( < XC, sign{$C, $A + $B, XC}ltkC > )+ ]+ --[ SessionKey($A, $B + $C, em(XB,XC) ^ ~ekA) ]->+ []++rule EphkRev:+ [ !Ephk(x) ]+ --[ EphkReveal(x) ]->+ [ Out(x) ]++lemma session_key_establish:+ exists-trace+ "Ex A B C #ia #ib #ic k.+ ( SessionKey(A,B + C, k) @ ia &+ SessionKey(B,C + A, k) @ ib &+ SessionKey(C,B + A, k) @ ic &+ not (A = B) &+ not (B = C) &+ not (A = C) &+ not ( Ex #j. LtkReveal(A) @ j ) &+ not ( Ex #j. LtkReveal(B) @ j ) &+ not ( Ex #j. LtkReveal(C) @ j ))"+++lemma Session_Key_Secrecy_PFS:+ "(All A B C sessKey #i #k. + SessionKey(A,B + C,sessKey) @ i &+ K(sessKey) @ k+ ==>+ (Ex #l. LtkReveal(A) @ l & l < i )+ | (Ex #l. LtkReveal(B) @ l & l < i )+ | (Ex #l. LtkReveal(C) @ l & l < i )+ | (Ex #l x. EphkReveal(x) @ l & l < i ))"++end
+ data/examples/ake/bilinear/README view
@@ -0,0 +1,4 @@+This folder contains case studies from+Benedikt Schmidt's Ph.D. thesis.+The remaining case studies from the thesis+can be found in the "csf12" folder.
+ data/examples/ake/bilinear/RYY.spthy view
@@ -0,0 +1,152 @@+theory RYY+begin++builtins: bilinear-pairing++functions: kdf/1, hp/1++section{* RYY : UM-like identity based key exchange protocol *}++/*+ * Protocol: RYY+ * Modeler: Benedikt Schmidt+ * Date: July 2012+ * Source: Boyd overview identity based key exchange protocols+ *+ * Status: Working+ */+++// Key generation center++rule KGC_Setup:+ [ Fr(msk) ]+ -->+ [ !MSK( msk ) ]++rule KGC_request:+ [ !MSK( s ) ]+ -->+ [ !LTK( $ID, pmult(s, hp($ID)) ) ]+++// Reveals++rule Reveal_ltk:+ [ !LTK( $ID, skID ) ]+ --[ LtkRev($ID) ]->+ [ Out(skID) ]++rule Reveal_master_key:+ [ !MSK( msk ) ]+ --[ MskRev() ]->+ [ Out( msk ) ]++rule Reveal_session_key:+ [ !Sessk( ~ey, sek ) ]+ --[ SesskRev( ~ey ) ]->+ [ Out( sek ) ]+++// Protocol++rule Init_1:+ [ Fr( ~ex ) ]+ -->+ [ Init( ~ex, $A, $B )+ , Out( 'g'^~ex )+ ]++rule Init_2:+ let X = 'g'^~ex+ sessKey = kdf( Y^~ex, em(hp($B), skA), $A, $B, X, Y )+ in+ [ Init( ~ex, $A, $B )+ , !LTK( $A, skA )+ , In( Y )+ ]+ --[ Accept( ~ex, sessKey )+ , Sid( ~ex, <$A,$B,X,Y,'Init'> )+ ]->+ [ !Sessk( ~ex, sessKey )]+++rule Resp_1:+ let Y = 'g'^~ey+ sessKey = kdf(X^~ey, em(skB, hp($A)), $A, $B, X, Y)+ in+ [ Fr( ~ey )+ , !LTK( $B, skB )+ , In( X )+ ]+ --[ Accept( ~ey, sessKey )+ , Sid( ~ey, <$B,$A,Y,X,'Resp'> )+ ]->+ [ Out( Y )+ , !Sessk( ~ey, sessKey )+ ]+++lemma key_agreement_reachable:+ exists-trace+ "Ex #i #j A B X Y t1 t2 k role1 role2.+ Accept(t1, k) @ i+ & Sid(t1, <A,B,X,Y,role1>) @ i+ & Accept(t2, k) @ j+ & Sid(t2, <B,A,Y,X,role2>) @ j+ & not (role1 = role2)"+++lemma key_secrecy_WPFS:+ /* + * We do not consider ephemeral key reveals for RYY+ * + * If there exists a test session whose key k is known to the+ * Adversary with some session id, then...+ */+ "(All #i1 #i2 test A B X Y role1 k.+ Accept(test, k) @ i1 & K( k ) @ i2 & Sid(test, <A,B,X,Y,role1>) @ i1+ ==> ( + // ... the test session must be "not clean".+ // test is not clean if one of the following has happened:+ //+ // 1. The adversary has revealed the test's session key.+ (Ex #i3. SesskRev( test ) @ i3 )++ // 2. There is a matching session and+ | (Ex matching #i3 role2.+ ( Sid ( matching, <B,A,Y,X,role2> ) @ i3 & not (role1 = role2))+ & ( + // (a) the adversary has revealed the session key of the matching sesssion, or+ (Ex #i5. SesskRev( matching ) @ i5 )++ // (b) the adversary revealed the longterm key of test's peer before test finished, or+ | (Ex #i5. LtkRev( B ) @ i5 & i5 < i1)++ // (c) the adversary revealed the longterm key of test's actor before test finished, or+ | (Ex #i5. LtkRev( A ) @ i5 & i5 < i1 )++ // (d) the adversary revealed the master key before test finished.+ | (Ex #i5. MskRev() @ i5 & i5 < i1 )+ )+ )++ // 3. There is no matching session and+ | ( (not (Ex matching #i3 role2.+ ( Sid ( matching, <B,A,Y,X,role2> ) @ i3 & not (role1 = role2))))++ & ( + // (a) the adversary revealed the longterm key of test's peer, or+ (Ex #i5. LtkRev( B ) @ i5)++ // (b) the adversary revealed the longterm key of test's actor, or+ | (Ex #i3. LtkRev(A) @ i3)+ + // (c) the adversary revealed the master key.+ | (Ex #i3. MskRev() @ i3)+ )+ )+ )+ )"++end
+ data/examples/ake/bilinear/RYY_PFS.spthy view
@@ -0,0 +1,152 @@+theory RYY+begin++builtins: bilinear-pairing++functions: kdf/1, hp/1++section{* RYY : UM-like identity based key exchange protocol *}++/*+ * Protocol: RYY+ * Modeler: Benedikt Schmidt+ * Date: July 2012+ * Source: Boyd overview identity based key exchange protocols+ *+ * Status: Working+ */+++// Key generation center++rule KGC_Setup:+ [ Fr(msk) ]+ -->+ [ !MSK( msk ) ]++rule KGC_request:+ [ !MSK( s ) ]+ -->+ [ !LTK( $ID, pmult(s, hp($ID)) ) ]+++// Reveals++rule Reveal_ltk:+ [ !LTK( $ID, skID ) ]+ --[ LtkRev($ID) ]->+ [ Out(skID) ]++rule Reveal_master_key:+ [ !MSK( msk ) ]+ --[ MskRev() ]->+ [ Out( msk ) ]++rule Reveal_session_key:+ [ !Sessk( ~ey, sek ) ]+ --[ SesskRev( ~ey ) ]->+ [ Out( sek ) ]+++// Protocol++rule Init_1:+ [ Fr( ~ex ) ]+ -->+ [ Init( ~ex, $A, $B )+ , Out( 'g'^~ex )+ ]++rule Init_2:+ let X = 'g'^~ex+ sessKey = kdf( Y^~ex, em(hp($B), skA), $A, $B, X, Y )+ in+ [ Init( ~ex, $A, $B )+ , !LTK( $A, skA )+ , In( Y )+ ]+ --[ Accept( ~ex, sessKey )+ , Sid( ~ex, <$A,$B,X,Y,'Init'> )+ ]->+ [ !Sessk( ~ex, sessKey )]+++rule Resp_1:+ let Y = 'g'^~ey+ sessKey = kdf(X^~ey, em(skB, hp($A)), $A, $B, X, Y)+ in+ [ Fr( ~ey )+ , !LTK( $B, skB )+ , In( X )+ ]+ --[ Accept( ~ey, sessKey )+ , Sid( ~ey, <$B,$A,Y,X,'Resp'> )+ ]->+ [ Out( Y )+ , !Sessk( ~ey, sessKey )+ ]+++lemma key_agreement_reachable:+ exists-trace+ "Ex #i #j A B X Y t1 t2 k role1 role2.+ Accept(t1, k) @ i+ & Sid(t1, <A,B,X,Y,role1>) @ i+ & Accept(t2, k) @ j+ & Sid(t2, <B,A,Y,X,role2>) @ j+ & not (role1 = role2)"+++lemma key_secrecy_PFS:+ /* + * We do not consider ephemeral key reveals for RYY+ * + * If there exists a test session whose key k is known to the+ * Adversary with some session id, then...+ */+ "(All #i1 #i2 test A B X Y role1 k.+ Accept(test, k) @ i1 & K( k ) @ i2 & Sid(test, <A,B,X,Y,role1>) @ i1+ ==> ( + // ... the test session must be "not clean".+ // test is not clean if one of the following has happened:+ //+ // 1. The adversary has revealed the test's session key.+ (Ex #i3. SesskRev( test ) @ i3 )++ // 2. There is a matching session and+ | (Ex matching #i3 role2.+ ( Sid ( matching, <B,A,Y,X,role2> ) @ i3 & not (role1 = role2))+ & ( + // (a) the adversary has revealed the session key of the matching sesssion, or+ (Ex #i5. SesskRev( matching ) @ i5 )++ // (b) the adversary revealed the longterm key of test's peer before test finished, or+ | (Ex #i5. LtkRev( B ) @ i5 & i5 < i1)++ // (c) the adversary revealed the longterm key of test's actor before test finished, or+ | (Ex #i5. LtkRev( A ) @ i5 & i5 < i1 )++ // (d) the adversary revealed the master key before test finished.+ | (Ex #i5. MskRev() @ i5 & i5 < i1 )+ )+ )++ // 3. There is no matching session and+ | ( (not (Ex matching #i3 role2.+ ( Sid ( matching, <B,A,Y,X,role2> ) @ i3 & not (role1 = role2))))++ & ( + // (a) the adversary revealed the longterm key of test's peer, or+ (Ex #i3. LtkRev( B ) @ i3 & i3 < i1)++ // (b) the adversary revealed the longterm key of test's actor, or+ | (Ex #i3. LtkRev(A) @ i3 & i3 < i1)+ + // (c) the adversary revealed the master key.+ | (Ex #i3. MskRev() @ i3 & i3 < i1)+ )+ )+ )+ )"++end
+ data/examples/ake/bilinear/Scott.spthy view
@@ -0,0 +1,161 @@+theory Scott+begin++builtins: bilinear-pairing++functions: kdf/1, hp/1++section{* Scott: MTI-C0 like identity based key exchange protocol *}++/*+ * Protocol: Scott+ * Modeler: Benedikt Schmidt+ * Date: May 2012+ * Source: Boyd overview identity based key exchange protocols+ *+ * Status: Working+ */+++// Key generation center++rule KGC_Setup:+ [ Fr( ~msk ) ]+ --[ KGCSetup() ]->+ [ !MSK( ~msk ) ]++rule KGC_request:+ [ !MSK( ~msk ) ]+ -->+ [ !LTK( $ID, pmult( ~msk, hp($ID) ) ) ]+++// Reveals++rule Reveal_ltk:+ [ !LTK( $ID, skID ) ]+ --[ LtkRev($ID) ]->+ [ Out(skID) ]++rule Reveal_master_key:+ [ !MSK( ~msk ) ]+ --[ MskRev() ]->+ [ Out( ~msk ) ]++rule Reveal_session_key:+ [ !Sessk( ~ey, sek ) ]+ --[ SesskRev( ~ey ) ]->+ [ Out( sek ) ]+++// Protocol++rule Init_1:+ let skA = pmult( ~s, hp($A) )+ X = em( skA, hp($B) )^~ex+ in + [ Fr( ~ex )+ , !LTK( $A, skA )+ ]+ -->+ [ Init( ~ex, $A, $B, X )+ , Out( X )+ ]++rule Init_2:+ let sessKey = kdf( Y^~ex, $A, $B, X, Y )+ in+ [ Init( ~ex, $A, $B, X )+ , In( Y )+ ]+ --[ Accept( ~ex, $A, $B, sessKey )+ , Sid( ~ex, <'Init',$A,$B,X,Y> )+ // a matching session for ~ex has the following sid+ , Match( ~ex, <'Resp',$B,$A,X,Y> )+ ]->+ [ !Sessk( ~ex, sessKey ) ]+++rule Resp_1:+ let skB = pmult( ~s, hp($B))+ Y = em(hp($A), skB)^~ey+ sessKey = kdf(X^~ey, $A, $B, X, Y)+ in+ [ Fr( ~ey )+ , !LTK( $B, skB )+ , In( X )+ ]+ --[ Accept( ~ey, $B, $A, sessKey )+ , Sid( ~ey, <'Resp',$B,$A,X,Y> )+ // a matching session for ~ey has the following sid+ , Match( ~ey, <'Init',$A,$B,X,Y> )+ ]->+ [ Out( Y )+ , !Sessk( ~ey, sessKey )+ ]+++lemma key_agreement_reachable:+ exists-trace+ "Ex #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"++++lemma key_secrecy:+ /* + * We do not consider ephemeral key reveals here.+ * There is a simple attack where another session of+ * A is used to get em(hp(A), hp(B))^s which is then sent+ * to A as Y. Then A uses X = em(hp(A), hp(B))^(s*ex) as+ * input for the kdf.+ * + * If there exists a Test session whose key k is known to the+ * Adversary, then...+ */+ "(All #i1 #i2 test A B k.+ Accept(test, A, B, k) @ i1 & K( k ) @ i2+ ==> ( + // ... the test session must be "not clean".+ // test is not clean if one of the following has happened:+ //+ // session-key-reveal of test thread.+ (Ex #i3. SesskRev( test ) @ i3 )+ + // more than one KGC+ | (Ex #i3 #i4. KGCSetup() @ i3 & KGCSetup() @ i4 & not (#i3 = #i4))+ + // there is a matching session+ | (Ex matching #i3 #i4 sid.+ // matching's 'sid' info matches with test+ ( Sid ( matching, sid ) @ i3 & Match( test, sid ) @ i4)+ & ( + // matching's session key was revealed+ (Ex #i5. SesskRev( matching ) @ i5 )+ )+ )++ // there is no matching session+ | ( (not (Ex matching #i3 #i4 sid.+ // matching's 'sid' info matches with test+ ( Sid ( matching, sid ) @ i3 & Match( test, sid ) @ i4)))++ & ( + // the longterm key of test.peer was revealed+ (Ex #i5. LtkRev( B ) @ i5 )++ // the longterm key of test.actor was revealed+ | (Ex #i3. LtkRev(A) @ i3 )+ + // the master key was revealed+ | (Ex #i3. MskRev() @ i3)+ )+ )++ )+ )"++end
+ data/examples/ake/bilinear/Scott_EphkRev.spthy view
@@ -0,0 +1,174 @@+theory Scott+begin++builtins: bilinear-pairing++functions: kdf/1, hp/1++section{* Scott: MTI-C0 like identity based key exchange protocol *}++/*+ * Protocol: Scott+ * Modeler: Benedikt Schmidt+ * Date: May 2012+ * Source: Boyd overview identity based key exchange protocols+ *+ * Status: Working+ */+++// Key generation center++rule KGC_Setup:+ [ Fr( ~msk ) ]+ --[ KGCSetup() ]->+ [ !MSK( ~msk ) ]++rule KGC_request:+ [ !MSK( ~msk ) ]+ -->+ [ !LTK( $ID, pmult( ~msk, hp($ID) ) ) ]+++// Reveals++rule Reveal_ltk:+ [ !LTK( $ID, skID ) ]+ --[ LtkRev($ID) ]->+ [ Out(skID) ]++rule Reveal_master_key:+ [ !MSK( ~msk ) ]+ --[ MskRev() ]->+ [ Out( ~msk ) ]++rule Reveal_session_key:+ [ !Sessk( ~ey, sek ) ]+ --[ SesskRev( ~ey ) ]->+ [ Out( sek ) ]++rule Reveal_ephmeral_key:+ [ !Ephk( ~ey ) ]+ --[ EphkRev( ~ey ) ]->+ [ Out( ~ey ) ]+++// Protocol++rule Init_1:+ let skA = pmult( ~s, hp($A) )+ X = em( skA, hp($B) )^~ex+ in + [ Fr( ~ex )+ , !LTK( $A, skA )+ ]+ -->+ [ Init( ~ex, $A, $B, X )+ , Out( X )+ , !Ephk( ~ex )+ ]++rule Init_2:+ let sessKey = kdf( Y^~ex, $A, $B, X, Y )+ in+ [ Init( ~ex, $A, $B, X )+ , In( Y )+ ]+ --[ Accept( ~ex, $A, $B, sessKey )+ , Sid( ~ex, <'Init',$A,$B,X,Y> )+ // a matching session for ~ex has the following sid+ , Match( ~ex, <'Resp',$B,$A,X,Y> )+ ]->+ [ !Sessk( ~ex, sessKey ) ]+++rule Resp_1:+ let skB = pmult( ~s, hp($B))+ Y = em(hp($A), skB)^~ey+ sessKey = kdf(X^~ey, $A, $B, X, Y)+ in+ [ Fr( ~ey )+ , !LTK( $B, skB )+ , In( X )+ ]+ --[ Accept( ~ey, $B, $A, sessKey )+ , Sid( ~ey, <'Resp',$B,$A,X,Y> )+ // a matching session for ~ey has the following sid+ , Match( ~ey, <'Init',$A,$B,X,Y> )+ ]->+ [ Out( Y )+ , !Sessk( ~ey, sessKey )+ , !Ephk( ~ey) + ]+++lemma key_agreement_reachable:+ exists-trace+ "Ex #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"++++lemma key_secrecy:+ /* + * We allow ephemeral key reveals here.+ * There is a simple attack where another session of+ * A is used to get em(hp(A), hp(B))^s which is then sent+ * to A as Y. Then A uses X = em(hp(A), hp(B))^(s*ex) as+ * input for the kdf.+ * + * If there exists a Test session whose key k is known to the+ * Adversary, then...+ */+ "(All #i1 #i2 test A B k.+ Accept(test, A, B, k) @ i1 & K( k ) @ i2+ ==> ( + // ... the test session must be "not clean".+ // test is not clean if one of the following has happened:+ //+ // session-key-reveal of test thread.+ (Ex #i3. SesskRev( test ) @ i3 )+ + // more than one KGC+ | (Ex #i3 #i4. KGCSetup() @ i3 & KGCSetup() @ i4 & not (#i3 = #i4))+ + // Ephemeral Key reveal and long-term key reveal for test session+ | (Ex #i5. EphkRev( test ) @ i5 & Ex #i6. LtkRev( A ) @ i6)++ // there is a matching session+ | (Ex matching #i3 #i4 sid.+ // matching's 'sid' info matches with test+ ( Sid ( matching, sid ) @ i3 & Match( test, sid ) @ i4)+ & ( + // matching's session key was revealed+ (Ex #i5. SesskRev( matching ) @ i5 )++ // Ephemeral Key reveal and long-term key reveal for test session+ | (Ex #i5. EphkRev( matching ) @ i5 & Ex #i6. LtkRev( B ) @ i6)+ )+ )++ // there is no matching session+ | ( (not (Ex matching #i3 #i4 sid.+ // matching's 'sid' info matches with test+ ( Sid ( matching, sid ) @ i3 & Match( test, sid ) @ i4)))++ & ( + // the longterm key of test.peer was revealed+ (Ex #i5. LtkRev( B ) @ i5 )++ // the longterm key of test.actor was revealed+ | (Ex #i3. LtkRev(A) @ i3 )+ + // the master key was revealed+ | (Ex #i3. MskRev() @ i3)+ )+ )++ )+ )"++end
+ data/examples/ake/bilinear/TAK1.spthy view
@@ -0,0 +1,124 @@+theory TAK1+begin++section{* The TAK1 Protocol. *}++/*+ * Protocol: TAK1+ * Modeler: Benedikt Schmidt+ * Date: July 2012+ *+ * Status: working+ */++builtins: bilinear-pairing, multiset+functions: kdf/1, tag/1, h/1++// Public key infrastructure+rule Register_pk:+ [ Fr( ~ea ) ]+ -->+ [ !Ltk( $A, ~ea ), !Pk( $A, pmult(~ea,'P') ), Out( pmult(~ea,'P') ) ]++// Key reveals++rule Reveal_ltk:+ [ !Ltk( $A, ~ea ) ]+ --[ LtkRev( $A ) ]->+ [ Out( ~ea ) ]++rule Reveal_ephk:+ [ !EphKey( ~ek ) ]+ --[ EphkRev( ~ek ) ]->+ [ Out( ~ek ) ]++rule Reveal_sessk:+ [ !SessKey( ~sid, kdf(sessKey ) ) ]+ --[ SesskRev( ~sid ) ]->+ [ Out( kdf(sessKey) ) ]+++// Protocol++rule Proto1:+ let XA = pmult(~ex,'P')+ in+ [ Fr( ~ex ) ]+ --[ Origin( ~ex, XA ), Participants($A + $B + $C) ]->+ [ PState1( ~ex, $A, $B, $C )+ , Out( XA )+ , !EphKey( ~ex )+ ]+++// We split this rule into two steps 'Proto2'+// and 'Proto3' to speed up the variant computation.+rule Proto2:+ [ PState1( ~ex, $A, $B, $C )+ , In( XB ) + , In( XC )+ ]+ -->+ // we first compute em(XB, XC)+ [ PState2( ~ex, $A, $B, $C, tag(XB), tag(XC), em(XB, XC) ) ]+++rule Proto3:+ let pkB = pmult(~eb,'P')+ pkC = pmult(~ec,'P')+ XA = pmult(~ex,'P')+ sessKey = kdf(emXBXC ^ ~ex, em(pkB,pkC) ^ ~ea,+ $A + $B + $C,+ tag(XA) + tag(XB) + tag(XC))+ in+ [ PState2( ~ex, $A, $B, $C, tag(XB), tag(XC), emXBXC )+ , !Ltk( $A, ~ea)+ , !Pk( $B, pkB )+ , !Pk( $C, pkC )+ ]+ --[ Accept( ~ex, $A, $B, $C, XA, tag(XB), tag(XC), sessKey )+ , Match( ~ex, <tag(XA) + tag(XB) + tag(XC), $A + $B + $C> )+ , Sid( ~ex, <tag(XA) + tag(XB) + tag(XC), $A + $B + $C> ) ]->+ // A session matches if the same multiset of messages has+ // been received and the same multiset of agents has participated+ [ !SessKey( ~ex, sessKey ) ]+++lemma session_key_establish:+ exists-trace+ "Ex A B C XA XB XC sa sb sc #ia #ib #ic k.+ ( Accept(sa, A, B, C, XA, tag(XB), tag(XC), k) @ ia &+ Accept(sb, B, A, C, XB, tag(XA), tag(XC), k) @ ib &+ Accept(sc, C, A, B, XC, tag(XA), tag(XB), k) @ ic &+ not (A = B) &+ not (B = C) &+ not (A = C) &+ not (Ex #j. LtkRev(A) @ j ) &+ not (Ex #j. LtkRev(B) @ j ) &+ not (Ex #j. LtkRev(C) @ j ))"++lemma Session_Key_Secrecy:+ "(All stest A B C XA XB XC sessKey sessString #i #j. + Accept(stest, A, B, C, XA, tag(XB), tag(XC), sessKey) @ i &+ K(sessKey) @ j &+ Match(stest, sessString) @ i+ ==>+ ( + // no session key reveal for matching session (includes stest)+ ( Ex #m #n smatch. Sid(smatch, sessString) @ m & SesskRev(smatch) @ n )++ // no origin session for either XB or XC+ | ( ( not (Ex #k spartner. Origin(spartner, XC) @ k ) + | not (Ex #k spartner. Origin(spartner, XB) @ k ))+ // no longterm key reveal for any of the participants allowed+ & ( (Ex #m. LtkRev(A) @ m )+ | (Ex #m. LtkRev(B) @ m )+ | (Ex #m. LtkRev(C) @ m )))++ | // there are origin sessions for both XB and XC+ (Ex #k #l spartner1 spartner2.+ Origin(spartner1, XB) @ k & Origin(spartner2, XC) @ l+ & (( ((Ex #v1. LtkRev(A) @ v1) | (Ex #v1. LtkRev(B) @ v1) | (Ex #v1. LtkRev(C) @ v1))+ & ((Ex #v2. EphkRev(stest) @ v2) | (Ex #v2. EphkRev(spartner1) @ v2) | (Ex #v2. EphkRev(spartner2) @ v2)))))))"++end
+ data/examples/ake/bilinear/TAK1_eCK_like.spthy view
@@ -0,0 +1,130 @@+theory TAK1+begin++section{* The TAK1 Protocol. *}++/*+ * Protocol: TAK1+ * Modeler: Benedikt Schmidt+ * Date: July 2012+ *+ * Status: working+ */++builtins: bilinear-pairing, multiset+functions: kdf/1, tag/1, h/1++// Public key infrastructure+rule Register_pk:+ [ Fr( ~ea ) ]+ -->+ [ !Ltk( $A, ~ea ), !Pk( $A, pmult(~ea,'P') ), Out( pmult(~ea,'P') ) ]++// Key reveals++rule Reveal_ltk:+ [ !Ltk( $A, ~ea ) ]+ --[ LtkRev( $A ) ]->+ [ Out( ~ea ) ]++rule Reveal_ephk:+ [ !EphKey( ~ek ) ]+ --[ EphkRev( ~ek ) ]->+ [ Out( ~ek ) ]++rule Reveal_sessk:+ [ !SessKey( ~sid, kdf(sessKey ) ) ]+ --[ SesskRev( ~sid ) ]->+ [ Out( kdf(sessKey) ) ]+++// Protocol++rule Proto1:+ let XA = pmult(~ex,'P')+ in+ [ Fr( ~ex ) ]+ --[ Origin( ~ex, XA ), Participants($A + $B + $C) ]->+ [ PState1( ~ex, $A, $B, $C )+ , Out( XA )+ , !EphKey( ~ex )+ ]+++// We split this rule into two steps 'Proto2'+// and 'Proto3' to speed up the variant computation.+rule Proto2:+ [ PState1( ~ex, $A, $B, $C )+ , In( XB ) + , In( XC )+ ]+ -->+ // we first compute em(XB, XC)+ [ PState2( ~ex, $A, $B, $C, tag(XB), tag(XC), em(XB, XC) ) ]+++rule Proto3:+ let pkB = pmult(~eb,'P')+ pkC = pmult(~ec,'P')+ XA = pmult(~ex,'P')+ sessKey = kdf(emXBXC ^ ~ex, em(pkB,pkC) ^ ~ea,+ $A + $B + $C,+ tag(XA) + tag(XB) + tag(XC))+ in+ [ PState2( ~ex, $A, $B, $C, tag(XB), tag(XC), emXBXC )+ , !Ltk( $A, ~ea)+ , !Pk( $B, pkB )+ , !Pk( $C, pkC )+ ]+ --[ Accept( ~ex, $A, $B, $C, XA, tag(XB), tag(XC), sessKey )+ , Match( ~ex, <tag(XA) + tag(XB) + tag(XC), $A + $B + $C> )+ , Sid( ~ex, <tag(XA) + tag(XB) + tag(XC), $A + $B + $C> ) ]->+ // A session matches if the same multiset of messages has+ // been received and the same multiset of agents has participated+ [ !SessKey( ~ex, sessKey ) ]+++lemma session_key_establish:+ exists-trace+ "Ex A B C XA XB XC sa sb sc #ia #ib #ic k.+ ( Accept(sa, A, B, C, XA, tag(XB), tag(XC), k) @ ia &+ Accept(sb, B, A, C, XB, tag(XA), tag(XC), k) @ ib &+ Accept(sc, C, A, B, XC, tag(XA), tag(XB), k) @ ic &+ not (A = B) &+ not (B = C) &+ not (A = C) &+ not (Ex #j. LtkRev(A) @ j ) &+ not (Ex #j. LtkRev(B) @ j ) &+ not (Ex #j. LtkRev(C) @ j ))"++lemma Session_Key_Secrecy:+ "(All stest A B C XA XB XC sessKey sessString #i #j. + Accept(stest, A, B, C, XA, tag(XB), tag(XC), sessKey) @ i &+ K(sessKey) @ j &+ Match(stest, sessString) @ i+ ==>+ ( + // no session key reveal for matching session (includes stest)+ ( Ex #m #n smatch. Sid(smatch, sessString) @ m & SesskRev(smatch) @ n )++ // no origin session for either XB or XC+ | ( ( not (Ex #k spartner. Origin(spartner, XC) @ k ) + | not (Ex #k spartner. Origin(spartner, XB) @ k ))+ // no longterm key reveal for any of the participants allowed+ & ( (Ex #m. LtkRev(A) @ m )+ | (Ex #m. LtkRev(B) @ m )+ | (Ex #m. LtkRev(C) @ m )))++ | // there are origin sessions for both XB and XC+ // We modify the model from TAK1 to allow reveals+ (Ex #k #l spartner1 spartner2.+ Origin(spartner1, XB) @ k & Origin(spartner2, XC) @ l++ // We modify the model from TAK1 to additionally allow+ & ((( ((Ex #v1. LtkRev(B) @ v1) | (Ex #v1. LtkRev(C) @ v1))+ & ((Ex #v2. EphkRev(spartner1) @ v2) | (Ex #v2. EphkRev(spartner2) @ v2))))+ // for an ephemeral reveal for the test session or a long-term key reveal+ // for the actor of test, but not both+ | ((Ex #v1. LtkRev(A) @ v1) & (Ex #v2. EphkRev(stest) @ v2))))))"++end
+ data/examples/ake/dh/DHKEA_NAXOS_C_eCK_PFS_keyreg_partially_matching.spthy view
@@ -0,0 +1,227 @@+theory DHKEA_NAXOS_C_eCK_PFS_keyreg_partially_matching+begin++builtins: diffie-hellman, multiset++/*+ * Protocol: NAXOS-C+ * Modeler: Cas Cremers, Benedikt Schmidt+ * Date: January 2012/April 2012/September 2012+ * Source: "Reusing Static Keys in Key Agreement Protocols"+ * Chatterjee, Menezes, Ustaoglu+ * Property: eCK-PFS security+ *+ * Status: Working+ */++functions: h1/1, h2/1, h/1+functions: first/1, second/1, concat/2+equations: concat(first(x), second(x)) = x++/* Protocol rules */++/* In the description in the paper, we omitted the sorts. + * In this description they are made explicit.+ * '$A' is equivalent to 'A:pub'+ * '~x' is equivalent to 'x:fresh'+ */++/* Generate long-term keypair */+rule generate_ltk:+ let pkA = 'g'^~ea + in+ [ Fr(~ea) ] + --[ RegKey($A), Honest($A) ]->+ [ !Ltk( $A, ~ea ), !Pk( $A, pkA ), Out( pkA ) ]++/* Keyreg dishonest */+rule generate_ltk_dishonest:+ [ In(pkA) ]+ --[ RegKey($A) ]->+ [ !Pk( $A, pkA ) ]++/* NAXOS Initiator */+rule Init_NAXOS_1:+ let X = 'g'^h1(<~ex, ~ea >)+ in+ [ Fr( ~ex ), !Ltk( $A, ~ea ) ]+ --[ Sid( ~ex, < $A, $B, <'1',X> , 'Init', 'NAXOS_C' >)]->+ [ Init_1( ~ex, $A, $B, ~ea, X )+ , !Ephk(~ex, ~ex)+ , Out( X ) ]++rule Init_NAXOS_2:+ let exp = h1( < ~ex, ~ea > )+ kstring = h( < Y^~ea, KB^exp, Y^exp, $A, $B, X, Y, 'NAXOS_C' > )+ key = second( kstring )+ conf = h2( < first( kstring ), 'I', $A, $B, X, Y, 'NAXOS_C' > )+ confB = h2( < first( kstring ), 'R', $B, $A, Y, X, 'NAXOS_C' > )+ in+ [ Init_1( ~ex, $A, $B, ~ea, X), !Pk( $B, KB )+ , In( <$B, Y, confB> ) ]+ --[ Accept( ~ex, key)+ , Sid( ~ex, < $A, $B, (<'1',X> + <'2',Y> + <'3',<$A, conf>>), 'Init' , 'NAXOS_C'>)+ ]->+ [ Out( <$A, conf> )+ , !Sessk( ~ex, key) ]++/* NAXOS Responder */+rule Resp_NAXOS_1:+ let exp = h1( < ~ey, ~eb > )+ Y = 'g'^exp+ kstring = h( < KA^exp, X^~eb, X^exp, $A, $B, X, Y, 'NAXOS_C' > )+ key = second( kstring )+ conf = h2( < first( kstring ), 'R', $B, $A, Y, X, 'NAXOS_C' > )+ confA = h2( < first( kstring ), 'I', $A, $B, X, Y, 'NAXOS_C' > )+ in+ [ Fr( ~ey ), !Ltk($B, ~eb), !Pk($A, KA)+ , In( X ) ]+ --[ Sid( ~ey, < $B, $A, (<'1',X> + <'2',Y>), 'Respo', 'NAXOS_C' > ) ]->+ [ Out( <$B,Y,conf> )+ , Resp_1( ~ey, $B, $A, Y , X, confA, key )+ , !Ephk(~ey, ~ey) ]++rule Resp_NAXOS_2:+ [ Resp_1( ~ey, $B, $A, Y, X, confA, key )+ , In( <$A, confA> ) ]+ --[ Accept( ~ey, key )+ , Sid( ~ey, < $B, $A, (<'1',X> + <'2',Y>+ <'3',<$A,confA>>), 'Respo', 'NAXOS_C' > )+ ]->+ [ !Sessk( ~ey, key) ]+++/* DHKEA Initiator */++rule Init_DHKEA_1:+ let X = 'g'^h1(<~ex, ~ea >)+ in+ [ Fr( ~ex ), !Ltk( $A, ~ea ) ]+ --[ Sid( ~ex, < $A, $B, <'1',X>, 'Init', 'DHKEA' >)+ ]->+ [ Init_DHKEA_1( ~ex, $A, $B, ~ea, X )+ , !Ephk(~ex, ~ex)+ , Out( X ) ]++rule Init_DHKEA_2:+ let KB = 'g'^~eb+ exp = h1( < ~ex, ~ea > )+ kstring = h( < Y^exp, $A, $B, X, Y, 'DHKEA' > )+ key = second( kstring )+ conf = h2( < first( kstring ), Y^~ea, 'I', $A, $B, X, Y, 'DHKEA' > )+ confB = h2( < first( kstring ), KB^exp, 'R', $B, $A, Y, X, 'DHKEA' > )+ in+ [ Init_DHKEA_1( ~ex, $A, $B, ~ea, X), !Pk( $B, KB )+ , In( <$B, Y, confB> ) ]+ --[ Accept( ~ex, key)+ , Sid( ~ex, < $A, $B, (<'1',X> + <'2',Y> + <'3',<$A, conf>>), 'Init', 'DHKEA' >)+ ]->+ [ Out( <$A, conf> )+ , !Sessk( ~ex, key) ]++/* DHKEA Responder */+rule Resp_DHKEA_1:+ let KA = 'g'^~lkI+ exp = h1( < ~ey, ~eb > )+ Y = 'g'^exp+ kstring = h( < X^exp, $A, $B, X, Y, 'DHKEA' > )+ key = second( kstring )+ conf = h2( < first( kstring ), X^~eb, 'R', $B, $A, Y, X, 'DHKEA' > )+ confA = h2( < first( kstring ), KA^exp, 'I', $A, $B, X, Y, 'DHKEA' > )+ in+ [ Fr( ~ey ), !Ltk($B, ~eb), !Pk($A, KA)+ , In( X ) ]+ --[ Sid( ~ey, < $B, $A, (<'1',X> + <'2',Y>), 'Respo', 'DHKEA' > )+ ]->+ [ Out( <$B,Y,conf> )+ , Resp_DHKEA_1( ~ey, $B, $A, Y , X, confA, key )+ , !Ephk(~ey, ~ey) ]++rule Resp_DHKEA_2:+ [ Resp_DHKEA_1( ~ey, $B, $A, Y, X, confA, key )+ , In( <$A, confA> ) ]+ --[ Accept( ~ey, key )+ , Sid( ~ey, < $B, $A, (<'1',X> + <'2',Y>+ <'3',<$A,confA>>), 'Respo', 'DHKEA' > )+ ]->+ [ !Sessk( ~ey, key) ]+++/* Key Reveals for the eCK model */+rule Sessk_reveal: + [ !Sessk(~s, k) ] --[ RevealSessk(~s) ]-> [ Out(k) ]++rule Ltk_reveal:+ [ !Ltk($A, ea) ] --[ RevealLtk($A) ]-> [ Out(ea) ]++rule Ephk_reveal:+ [ !Ephk(~s, ~ek) ] --[ RevealEphk(~s) ]-> [ Out(~ek) ]++++axiom RegKeyUnique:+ "All #i #j A. RegKey(A) @ i & RegKey(A) @ j ==> #i = #j"+++/* Security properties */++lemma execution_match_same_key_NAXOS:+ exists-trace+ "Ex #i1 #i2 s1 s2 k A B com role1 role2.+ Accept( s1, k) @ i1+ & Accept( s2, k) @ i2+ & Sid( s1, <A,B,com,role1, 'NAXOS_C'> ) @ i1+ & Sid( s2, <B,A,com,role2, 'NAXOS_C'> ) @ i2+ & not (role1 = role2)"+++lemma eCK_key_secrecy:+ /* + * The property specification is a (logically equivalent) simplified+ * version of the one in the original eCK (ProvSec) paper:+ *+ * If there exists a test session whose key k is known to the+ * Adversary with some session-id, then...+ */+ "(All #i1 #i2 #i3 #i4 test A B k com role proto.+ Accept(test, k) @ i1 & K( k ) @ i2+ & Sid(test, < A, B, com, role, proto> ) @ i1 // we want the last Sid at the same time as Accept+ & Honest(A) @ i3 & Honest(B) @ i4+ ==> ( + /* ... the test session must be "not clean".+ * test is not clean if one of the following has happened:+ */+ /* 1. The adversary has revealed the session key of the test session. */+ (Ex #i3. RevealSessk( test ) @ i3 )+ + /* 2. The adversary has revealed both the longterm key of A and the+ ephemeral key of the test session */+ | (Ex #i5 #i6. RevealLtk ( A ) @ i5 & RevealEphk ( test ) @ i6 )++ /* 3. There is a matching session and */+ | (Ex matchingSession #i3 matchingRole matchingCom.+ ( Sid ( matchingSession, < B, A, matchingCom, matchingRole, proto > ) @ i3 + & not ( matchingRole = role )+ & ((Ex rest. matchingCom + rest = com) | (matchingCom = com))+ & not (Ex #i4 sid. Sid ( matchingSession, sid) @ i4 & #i3 < #i4))+ & (+ /* (a) the adversary has revealed the session key of the matching session, or */+ (Ex #i5. RevealSessk( matchingSession ) @ i5 )++ /* (b) the adversary has revealed the longterm key of B and the ephemeral+ key of the matching session. */+ | (Ex #i5 #i6. RevealLtk ( B ) @ i5 & RevealEphk ( matchingSession ) @ i6 )+ )+ )+ /* 4. There is no matching session and */+ | ( ( not (Ex matchingSession #i3 matchingRole matchingCom.+ Sid ( matchingSession, < B, A, matchingCom, matchingRole, proto > ) @ i3 + & not ( matchingRole = role )+ & ((Ex rest. matchingCom + rest = com) | (matchingCom = com))+ & not (Ex #i4 sid. Sid ( matchingSession, sid) @ i4 & #i3 < #i4)))++ /* the adversary has revealed the longterm key of B. */+ & (Ex #i5. RevealLtk (B) @ i5 & #i5 < #i1)+ )+ )+ )"++end
+ data/examples/ake/dh/DHKEA_NAXOS_C_eCK_PFS_partially_matching.spthy view
@@ -0,0 +1,221 @@+theory DHKEA_NAXOS_C_eCK_PFS_partially_matching+begin++builtins: diffie-hellman, multiset++/*+ * Protocol: NAXOS-C+ * Modeler: Cas Cremers, Benedikt Schmidt+ * Date: January 2012/April 2012/September 2012+ * Source: "Reusing Static Keys in Key Agreement Protocols"+ * Chatterjee, Menezes, Ustaoglu+ * Property: eCK-PFS security+ *+ * Status: Working+ */++functions: h1/1, h2/1, h/1+functions: first/1, second/1, concat/2+equations: concat(first(x), second(x)) = x++/* Protocol rules */++/* In the description in the paper, we omitted the sorts. + * In this description they are made explicit.+ * '$A' is equivalent to 'A:pub'+ * '~x' is equivalent to 'x:fresh'+ */++/* Generate long-term keypair */+rule generate_ltk:+ let pkA = 'g'^~ea + in+ [ Fr(~ea) ] + --[ RegKey($A), Honest($A) ]->+ [ !Ltk( $A, ~ea ), !Pk( $A, pkA ), Out( pkA ) ]++/* NAXOS Initiator */+rule Init_NAXOS_1:+ let X = 'g'^h1(<~ex, ~ea >)+ in+ [ Fr( ~ex ), !Ltk( $A, ~ea ) ]+ --[ Sid( ~ex, < $A, $B, <'1',X> , 'Init', 'NAXOS_C' >)]->+ [ Init_1( ~ex, $A, $B, ~ea, X )+ , !Ephk(~ex, ~ex)+ , Out( X ) ]++rule Init_NAXOS_2:+ let exp = h1( < ~ex, ~ea > )+ kstring = h( < Y^~ea, KB^exp, Y^exp, $A, $B, X, Y, 'NAXOS_C' > )+ key = second( kstring )+ conf = h2( < first( kstring ), 'I', $A, $B, X, Y, 'NAXOS_C' > )+ confB = h2( < first( kstring ), 'R', $B, $A, Y, X, 'NAXOS_C' > )+ in+ [ Init_1( ~ex, $A, $B, ~ea, X), !Pk( $B, KB )+ , In( <$B, Y, confB> ) ]+ --[ Accept( ~ex, key)+ , Sid( ~ex, < $A, $B, (<'1',X> + <'2',Y> + <'3',<$A, conf>>), 'Init' , 'NAXOS_C'>)+ ]->+ [ Out( <$A, conf> )+ , !Sessk( ~ex, key) ]++/* NAXOS Responder */+rule Resp_NAXOS_1:+ let exp = h1( < ~ey, ~eb > )+ Y = 'g'^exp+ kstring = h( < KA^exp, X^~eb, X^exp, $A, $B, X, Y, 'NAXOS_C' > )+ key = second( kstring )+ conf = h2( < first( kstring ), 'R', $B, $A, Y, X, 'NAXOS_C' > )+ confA = h2( < first( kstring ), 'I', $A, $B, X, Y, 'NAXOS_C' > )+ in+ [ Fr( ~ey ), !Ltk($B, ~eb), !Pk($A, KA)+ , In( X ) ]+ --[ Sid( ~ey, < $B, $A, (<'1',X> + <'2',Y>), 'Respo', 'NAXOS_C' > ) ]->+ [ Out( <$B,Y,conf> )+ , Resp_1( ~ey, $B, $A, Y , X, confA, key )+ , !Ephk(~ey, ~ey) ]++rule Resp_NAXOS_2:+ [ Resp_1( ~ey, $B, $A, Y, X, confA, key )+ , In( <$A, confA> ) ]+ --[ Accept( ~ey, key )+ , Sid( ~ey, < $B, $A, (<'1',X> + <'2',Y>+ <'3',<$A,confA>>), 'Respo', 'NAXOS_C' > )+ ]->+ [ !Sessk( ~ey, key) ]+++/* DHKEA Initiator */++rule Init_DHKEA_1:+ let X = 'g'^h1(<~ex, ~ea >)+ in+ [ Fr( ~ex ), !Ltk( $A, ~ea ) ]+ --[ Sid( ~ex, < $A, $B, <'1',X>, 'Init', 'DHKEA' >)+ ]->+ [ Init_DHKEA_1( ~ex, $A, $B, ~ea, X )+ , !Ephk(~ex, ~ex)+ , Out( X ) ]++rule Init_DHKEA_2:+ let KB = 'g'^~eb+ exp = h1( < ~ex, ~ea > )+ kstring = h( < Y^exp, $A, $B, X, Y, 'DHKEA' > )+ key = second( kstring )+ conf = h2( < first( kstring ), Y^~ea, 'I', $A, $B, X, Y, 'DHKEA' > )+ confB = h2( < first( kstring ), KB^exp, 'R', $B, $A, Y, X, 'DHKEA' > )+ in+ [ Init_DHKEA_1( ~ex, $A, $B, ~ea, X), !Pk( $B, KB )+ , In( <$B, Y, confB> ) ]+ --[ Accept( ~ex, key)+ , Sid( ~ex, < $A, $B, (<'1',X> + <'2',Y> + <'3',<$A, conf>>), 'Init', 'DHKEA' >)+ ]->+ [ Out( <$A, conf> )+ , !Sessk( ~ex, key) ]++/* DHKEA Responder */+rule Resp_DHKEA_1:+ let KA = 'g'^~lkI+ exp = h1( < ~ey, ~eb > )+ Y = 'g'^exp+ kstring = h( < X^exp, $A, $B, X, Y, 'DHKEA' > )+ key = second( kstring )+ conf = h2( < first( kstring ), X^~eb, 'R', $B, $A, Y, X, 'DHKEA' > )+ confA = h2( < first( kstring ), KA^exp, 'I', $A, $B, X, Y, 'DHKEA' > )+ in+ [ Fr( ~ey ), !Ltk($B, ~eb), !Pk($A, KA)+ , In( X ) ]+ --[ Sid( ~ey, < $B, $A, (<'1',X> + <'2',Y>), 'Respo', 'DHKEA' > )+ ]->+ [ Out( <$B,Y,conf> )+ , Resp_DHKEA_1( ~ey, $B, $A, Y , X, confA, key )+ , !Ephk(~ey, ~ey) ]++rule Resp_DHKEA_2:+ [ Resp_DHKEA_1( ~ey, $B, $A, Y, X, confA, key )+ , In( <$A, confA> ) ]+ --[ Accept( ~ey, key )+ , Sid( ~ey, < $B, $A, (<'1',X> + <'2',Y>+ <'3',<$A,confA>>), 'Respo', 'DHKEA' > )+ ]->+ [ !Sessk( ~ey, key) ]+++/* Key Reveals for the eCK model */+rule Sessk_reveal: + [ !Sessk(~s, k) ] --[ RevealSessk(~s) ]-> [ Out(k) ]++rule Ltk_reveal:+ [ !Ltk($A, ea) ] --[ RevealLtk($A) ]-> [ Out(ea) ]++rule Ephk_reveal:+ [ !Ephk(~s, ~ek) ] --[ RevealEphk(~s) ]-> [ Out(~ek) ]++++axiom RegKeyUnique:+ "All #i #j A. RegKey(A) @ i & RegKey(A) @ j ==> #i = #j"+++/* Security properties */++lemma execution_match_same_key_NAXOS:+ exists-trace+ "Ex #i1 #i2 s1 s2 k A B com role1 role2.+ Accept( s1, k) @ i1+ & Accept( s2, k) @ i2+ & Sid( s1, <A,B,com,role1, 'NAXOS_C'> ) @ i1+ & Sid( s2, <B,A,com,role2, 'NAXOS_C'> ) @ i2+ & not (role1 = role2)"+++lemma eCK_key_secrecy:+ /* + * The property specification is a (logically equivalent) simplified+ * version of the one in the original eCK (ProvSec) paper:+ *+ * If there exists a test session whose key k is known to the+ * Adversary with some session-id, then...+ */+ "(All #i1 #i2 #i3 #i4 test A B k com role proto.+ Accept(test, k) @ i1 & K( k ) @ i2+ & Sid(test, < A, B, com, role, proto> ) @ i1 // we want the last Sid at the same time as Accept+ & Honest(A) @ i3 & Honest(B) @ i4+ ==> ( + /* ... the test session must be "not clean".+ * test is not clean if one of the following has happened:+ */+ /* 1. The adversary has revealed the session key of the test session. */+ (Ex #i3. RevealSessk( test ) @ i3 )+ + /* 2. The adversary has revealed both the longterm key of A and the+ ephemeral key of the test session */+ | (Ex #i5 #i6. RevealLtk ( A ) @ i5 & RevealEphk ( test ) @ i6 )++ /* 3. There is a matching session and */+ | (Ex matchingSession #i3 matchingRole matchingCom.+ ( Sid ( matchingSession, < B, A, matchingCom, matchingRole, proto > ) @ i3 + & not ( matchingRole = role )+ & ((Ex rest. matchingCom + rest = com) | (matchingCom = com))+ & not (Ex #i4 sid. Sid ( matchingSession, sid) @ i4 & #i3 < #i4))+ & (+ /* (a) the adversary has revealed the session key of the matching session, or */+ (Ex #i5. RevealSessk( matchingSession ) @ i5 )++ /* (b) the adversary has revealed the longterm key of B and the ephemeral+ key of the matching session. */+ | (Ex #i5 #i6. RevealLtk ( B ) @ i5 & RevealEphk ( matchingSession ) @ i6 )+ )+ )+ /* 4. There is no matching session and */+ | ( ( not (Ex matchingSession #i3 matchingRole matchingCom.+ Sid ( matchingSession, < B, A, matchingCom, matchingRole, proto > ) @ i3 + & not ( matchingRole = role )+ & ((Ex rest. matchingCom + rest = com) | (matchingCom = com))+ & not (Ex #i4 sid. Sid ( matchingSession, sid) @ i4 & #i3 < #i4)))++ /* the adversary has revealed the longterm key of B. */+ & (Ex #i5. RevealLtk (B) @ i5 & #i5 < #i1)+ )+ )+ )"++end
+ data/examples/ake/dh/NAXOS_eCK.spthy view
@@ -0,0 +1,148 @@+theory NAXOS_eCK+begin++builtins: diffie-hellman++section{* NAXOS *}++/*+ * Protocol: NAXOS+ * Modeler: Cas Cremers, Benedikt Schmidt+ * Date: January 2012/April 2012/October 2012+ * Source: "Stronger Security of Authenticated Key Exchange"+ * LaMacchia, Lauter, Mityagin, 2007+ * Property: eCK security+ *+ * Status: Working+ */++functions: h1/1+functions: h2/1++/* Protocol rules */++/* In the description in the paper, we omitted the sorts. + * In this description they are made explicit.+ * '$A' is equivalent to 'A:pub'+ * '~x' is equivalent to 'x:fresh'+ */++/* Generate long-term keypair */+rule generate_ltk:+ let pkA = 'g'^~ea + in+ [ Fr(~ea) ] + --[ RegKey($A) ]->+ [ !Ltk( $A, ~ea ), !Pk( $A, pkA ), Out( pkA ) ]++/* Initiator */+rule Init_1:+ let X = 'g'^h1(<~ex, ~ea >)+ in+ [ Fr( ~ex ), !Ltk( $A, ~ea ) ]+ -->+ [ Init_1( ~ex, $A, $B, ~ea )+ , !Ephk(~ex, ~ex)+ , Out( X ) ]++rule Init_2:+ let KB = 'g'^~eb+ X = 'g'^h1(<~ex, ~ea >)+ exp = h1(< ~ex, ~ea >)+ key = h2(< Y^~ea, KB^exp, Y^exp, $A, $B >) + in+ [ Init_1( ~ex, $A, $B, ~ea)+ , !Pk( $B, KB ), In( Y ) ]+ --[ Accept( ~ex, key)+ , Sid( ~ex, < $A, $B, X, Y, 'Init' >)+ ]->+ [ !Sessk( ~ex, key) ]++/* Responder */+rule Resp_1:+ let KA = 'g'^~lkI+ exp = h1(< ~ey, ~eb >)+ Y = 'g'^exp+ key = h2(< KA^exp, X^~eb, X^exp, $A, $B >) + in+ [ Fr( ~ey ), !Ltk($B, ~eb), !Pk($A, KA), In( X ) ]+ --[ Accept( ~ey, key )+ , Sid( ~ey, < $B, $A, Y, X, 'Resp' > )+ ]->+ [ Out( Y ),+ !Ephk(~ey, ~ey),+ !Sessk( ~ey, key) ]++/* Key Reveals for the eCK model */+rule Sessk_reveal: + [ !Sessk(~s, k) ] --[ RevealSessk(~s) ]-> [ Out(k) ]++rule Ltk_reveal:+ [ !Ltk($A, ea) ] --[ RevealLtk($A) ]-> [ Out(ea) ]++rule Ephk_reveal:+ [ !Ephk(~s, ~ek) ] --[ RevealEphk(~s) ]-> [ Out(~ek) ]+++/* Security properties */+/*+lemma eCK_same_key:+ " // If every agent registered at most one public key+ (All A #i #j. RegKey(A)@i & RegKey(A)@j ==> (#i = #j))+ ==> // then matching sessions accept the same key+ (not (Ex #i1 #i2 #i3 #i4 s ss k kk A B minfo .+ Accept(s, A, B, k ) @ i1+ & Accept(ss, B, A, kk) @ i2+ & Sid(s, minfo) @ i3+ & Match(ss, minfo) @i4+ & not( k = kk )+ ) )"+*/++lemma eCK_key_secrecy:+ /* + * The property specification is a (logically equivalent) simplified+ * version of the one in the original eCK (ProvSec) paper:+ *+ * If there exists a test session whose key k is known to the+ * Adversary with some session-id, then...+ */+ "(All #i1 #i2 #i3 test A B k sent recvd role.+ Accept(test, k) @ i1 & K( k ) @ i2 & Sid(test, < A, B, sent, recvd, role> ) @ i3+ ==> ( + /* ... the test session must be "not clean".+ * test is not clean if one of the following has happened:+ */+ /* 1. The adversary has revealed the session key of the test session. */+ (Ex #i3. RevealSessk( test ) @ i3 )+ + /* 2. The adversary has revealed both the longterm key of A and the+ ephemeral key of the test session */+ | (Ex #i5 #i6. RevealLtk ( A ) @ i5 & RevealEphk ( test ) @ i6 )++ /* 3. There is a matching session and */+ | (Ex matchingSession #i3 matchingRole.+ ( Sid ( matchingSession, < B, A, recvd, sent, matchingRole > ) @ i3 + & not ( matchingRole = role ) )+ & (+ /* (a) the adversary has revealed the session key of the matching session, or */+ (Ex #i5. RevealSessk( matchingSession ) @ i5 )++ /* (b) the adversary has revealed the longterm key of B and the ephemeral+ key of the matching session. */+ | (Ex #i5 #i6. RevealLtk ( B ) @ i5 & RevealEphk ( matchingSession ) @ i6 )+ )+ )+ /* 4. There is no matching session and */+ | ( ( not(Ex matchingSession #i3 matchingRole.+ ( Sid ( matchingSession, < B, A, recvd, sent, matchingRole > ) @ i3 + & not ( matchingRole = role ) )))++ /* the adversary has revealed the longterm key of B. */+ & ( (Ex #i5. RevealLtk (B) @ i5 )+ )+ )+ )+ )"++end
+ data/examples/ake/dh/NAXOS_eCK_PFS.spthy view
@@ -0,0 +1,149 @@+theory NAXOS_eCK+begin++builtins: diffie-hellman++section{* NAXOS *}++/*+ * Protocol: NAXOS+ * Modeler: Cas Cremers, Benedikt Schmidt+ * Date: January 2012/April 2012/October 2012+ * Source: "Stronger Security of Authenticated Key Exchange"+ * LaMacchia, Lauter, Mityagin, 2007+ * Property: eCK security + PFS+ *+ * Status: Working+ */++functions: h1/1+functions: h2/1++/* Protocol rules */++/* In the description in the paper, we omitted the sorts. + * In this description they are made explicit.+ * '$A' is equivalent to 'A:pub'+ * '~x' is equivalent to 'x:fresh'+ */++/* Generate long-term keypair */+rule generate_ltk:+ let pkA = 'g'^~ea + in+ [ Fr(~ea) ] + --[ RegKey($A) ]->+ [ !Ltk( $A, ~ea ), !Pk( $A, pkA ), Out( pkA ) ]++/* Initiator */+rule Init_1:+ let X = 'g'^h1(<~ex, ~ea >)+ in+ [ Fr( ~ex ), !Ltk( $A, ~ea ) ]+ -->+ [ Init_1( ~ex, $A, $B, ~ea )+ , !Ephk(~ex, ~ex)+ , Out( X ) ]++rule Init_2:+ let KB = 'g'^~eb+ X = 'g'^h1(<~ex, ~ea >)+ exp = h1(< ~ex, ~ea >)+ key = h2(< Y^~ea, KB^exp, Y^exp, $A, $B >) + in+ [ Init_1( ~ex, $A, $B, ~ea)+ , !Pk( $B, KB ), In( Y ) ]+ --[ Accept( ~ex, key)+ , Sid( ~ex, < $A, $B, X, Y, 'Init' >)+ ]->+ [ !Sessk( ~ex, key) ]++/* Responder */+rule Resp_1:+ let KA = 'g'^~lkI+ exp = h1(< ~ey, ~eb >)+ Y = 'g'^exp+ key = h2(< KA^exp, X^~eb, X^exp, $A, $B >) + in+ [ Fr( ~ey ), !Ltk($B, ~eb), !Pk($A, KA), In( X ) ]+ --[ Accept( ~ey, key )+ , Sid( ~ey, < $B, $A, Y, X, 'Resp' > )+ ]->+ [ Out( Y ),+ !Ephk(~ey, ~ey),+ !Sessk( ~ey, key) ]++/* Key Reveals for the eCK model */+rule Sessk_reveal: + [ !Sessk(~s, k) ] --[ RevealSessk(~s) ]-> [ Out(k) ]++rule Ltk_reveal:+ [ !Ltk($A, ea) ] --[ RevealLtk($A) ]-> [ Out(ea) ]++rule Ephk_reveal:+ [ !Ephk(~s, ~ek) ] --[ RevealEphk(~s) ]-> [ Out(~ek) ]+++/* Security properties */+/*+lemma eCK_same_key:+ " // If every agent registered at most one public key+ (All A #i #j. RegKey(A)@i & RegKey(A)@j ==> (#i = #j))+ ==> // then matching sessions accept the same key+ (not (Ex #i1 #i2 #i3 #i4 s ss k kk A B minfo .+ Accept(s, A, B, k ) @ i1+ & Accept(ss, B, A, kk) @ i2+ & Sid(s, minfo) @ i3+ & Match(ss, minfo) @i4+ & not( k = kk )+ ) )"+*/++// This property is not satisfied by NAXOS.+lemma eCK_PFS_key_secrecy:+ /* + * The property specification is a (logically equivalent) simplified+ * version of the one in the original eCK (ProvSec) paper:+ *+ * If there exists a test session whose key k is known to the+ * Adversary with some session-id, then...+ */+ "(All #i1 #i2 #i3 test A B k sent recvd role.+ Accept(test, k) @ i1 & K( k ) @ i2 & Sid(test, < A, B, sent, recvd, role> ) @ i3+ ==> ( + /* ... the test session must be "not clean".+ * test is not clean if one of the following has happened:+ */+ /* 1. The adversary has revealed the session key of the test session. */+ (Ex #i3. RevealSessk( test ) @ i3 )+ + /* 2. The adversary has revealed both the longterm key of A and the+ ephemeral key of the test session */+ | (Ex #i5 #i6. RevealLtk ( A ) @ i5 & RevealEphk ( test ) @ i6 )++ /* 3. There is a matching session and */+ | (Ex matchingSession #i3 matchingRole.+ ( Sid ( matchingSession, < B, A, recvd, sent, matchingRole > ) @ i3 + & not ( matchingRole = role ) )+ & (+ /* (a) the adversary has revealed the session key of the matching session, or */+ (Ex #i5. RevealSessk( matchingSession ) @ i5 )++ /* (b) the adversary has revealed the longterm key of B and the ephemeral+ key of the matching session. */+ | (Ex #i5 #i6. RevealLtk ( B ) @ i5 & RevealEphk ( matchingSession ) @ i6 )+ )+ )+ /* 4. There is no matching session and */+ | ( ( not(Ex matchingSession #i3 matchingRole.+ ( Sid ( matchingSession, < B, A, recvd, sent, matchingRole > ) @ i3 + & not ( matchingRole = role ) )))++ /* the adversary has revealed the longterm key of B before test accepted the key. */+ & ( (Ex #i5. RevealLtk (B) @ i5 & i5 < i1)+ )+ )+ )+ )"++end
+ data/examples/ake/dh/UM_one_pass_attack.spthy view
@@ -0,0 +1,208 @@+theory UM_one_pass_attack+begin++/*+ The one-pass UM protocol. See+ "Combined Security Analysis of the One- and Three-Pass Unified Model Key Agreement Protocols"+ Sanjit Chatterjee, Alfred Menezes and Berkant Ustaoglu++ The last property is not valid for the model since there+ is a flaw in the definition of the model and the proof.+ + The problem is that the session id does not contain the+ role and since this is a one-pass protocol, this means+ that a responder session <A,B,X> can match another+ responder session <B,A,X> if X is replayed.+*/++builtins: diffie-hellman, hashing++/* Key registration */++rule Register_key_honest:+ let pkA = 'g'^~ea+ in+ [ Fr( ~ea ) // select random longterm private+ ] + --[ KeyReg( $A ) ]-> // a key for A has been registered+ [ !Ltk( $A, ~ea ) // ~ea is the longterm private key of A+ , !Pk( $A, pkA ) // pkA = 'g'^~ea is the longterm public key of A+ , Out( pkA ) ] // the adversary can learn the public key ++/* Initiator */+++// Activate the session: choose ephemeral private key, compute ephemeral public key X.+rule I_Activate:+ let X = 'g'^~ex // the ephemeral public key+ sid = <$A, $B, X> // the session id, not unique because there might+ // be responder session with actor B and peer A+ // which receives X+ in+ [ Fr( ~ex ) ] // select random ephemeral private key+ --[ Activate( sid ) ]-> // sid is 'Activate'd after this step+ [ I_Act( ~ex, $A, $B ) // the state of this session, identified by ex (unique)+ , !SessionState( sid, $A, ~ex ) // the session state of sid with actor $A consists only of ex,+ // available for reveals+ ]++// Complete the session: send X, and compute key.+rule I_Complete:+ let X = 'g'^~ex // recompute X+ sid = <$A, $B, X> // recompute sid+ pB = 'g'^~eb // we do not model key registration by adversary,+ // hence key always of this form+ k = h(pB^~ex, pB^~ea, $A, $B) // we do not include the public string+ in+ [ I_Act( ~ex, $A, $B ) // this session was activated+ , !Ltk( $A, ~ea ) // lookup own longterm private key+ , !Pk( $B, pB ) ] // lookup peer's public key+ --[ Complete( sid, 'I', k ) ]-> // sid is 'Complete'd after this step+ [ I_Comp( sid ) // state of this session+ , Out( <$B, $A, X> ) // send message+ , !SessionKey( sid, $A, k ) ] // the session key of sid with actor $A, available+ // for reveals+// Expire the session+rule I_Expire:+ [ I_Comp( sid ) ]+ --[ Expire( sid ) ]-> // sid is expired after this step+ [ ]+++/* Responder */++// R has no Activated state since there is no ephemeral key.+rule R_Complete:+ let pA = 'g'^~ea // we do not model key registration by adversary,+ // hence key always of this form+ sid = <$B, $A, X> // sid is not unique because of initiator sessions with+ // same sid and replay+ k = h(X^~eb, pA^~eb, $A, $B)+ in+ [ In( X )+ , !Ltk( $B, ~eb )+ , !Pk( $A, pA ) ]+ --[ Activate(sid), Complete( sid, 'R', k ) ]-> // sid is 'Complete'd and 'Activate'd after this step+ [ R_Comp( sid )+ , !SessionKey( sid, $B, k )+ ]++rule R_Expire:+ [ R_Comp( sid ) ]+ --[ Expire( sid ) ]-> // sid is expired after this step+ [ ]++/* Corrupt an agent:+ We model corruption by three different rules.+ We do not model static key selection for corrupted agents.+*/++// Corrupt and obtain longterm key+rule Corrupt_Ltk:+ [ !Ltk( $A, ~ea ) ]+ --[ Corrupt( $A ) ]->+ [ Out( ~ea ) ]++// Corrupt and obtain session state. Must occur before complete which+// we ensure with BeforeComplete action and axiom.+rule Corrupt_SessionState:+ [ !SessionState( sid, ~x, $A ) ]+ --[ Corrupt( $A ), BeforeComplete( sid ) ]->+ [ Out( ~x ) ]++// Corrupt and obtain session key. Must occur before expire which+// we ensure with BeforeExpire action and axiom.+rule Corrupt_SessionKey:+ [ !SessionKey( sid, $A, k ) ]+ --[ Corrupt( $A ), BeforeExpire( sid ) ]->+ [ Out( k ) ]++/* Reveals for session state and session key */++rule Reveal_SessionState:+ [ !SessionState( sid, ~x, $A ) ]+ --[SessionStateReveal( sid ), BeforeComplete( sid ) ]->+ [ Out( ~x ) ]++rule Reveal_SessionKey:+ [ !SessionKey( sid, $A, k) ]+ --[ SessionKeyReveal( sid ), BeforeExpire( sid ) ]->+ [ Out( k ) ]++/* We only consider traces which satisfy these axioms */++// we enforce unique sids since the paper states that "At any point in time a session is+// in exactly one of the following states: active, completed, aborted, expired."+axiom sid_unique:+ "All #i #j sid. Activate(sid) @ i & Activate(sid) @ j ==> #i = #j"++// every agent has at most one registered key+axiom keyreg_unique:+ "All #i #j A. KeyReg(A) @ i & KeyReg(A) @ j ==> #i = #j"++// The reveals and the corrupt rules that reveal session state and session key are not performed+// too late.+axiom corrupt_and_reveal_not_too_early:+ " (All #i #j s role_ k_. BeforeComplete( s ) @ i & Complete(s, role_, k_ ) @ j ==> #i < #j)+ & (All #i #j s. BeforeExpire( s ) @ i & Expire( s ) @ j ==> #i < #j)"++// Key agreement for initiator and responder is reachable without any adversary interaction.+lemma key_agreement_reachable:+ exists-trace+ "Ex #i #j sid sidm k.+ Complete( sid , 'I', k ) @ i+ & Complete( sidm, 'R', k ) @ j+ & (not (Ex #j C. Corrupt( C ) @ j))+ & (not (Ex #j s. SessionKeyReveal( s ) @ j))+ & (not (Ex #j s. SessionStateReveal( s ) @ j))"+++lemma CK_secure:+ "(All #i #j role A B X k s sp.+ /* The key of a complete session 's' is known (whose partner is 'sp') */+ Complete( <A,B,X> , role, k ) @ i & K( k ) @ j & s = <A,B,X> & sp = <B,A,X>+ /* then one of the following must have happened */+ ==>+ /* 1. (a) The session key of s was revealed */+ (Ex #k. SessionKeyReveal( s ) @ k)++ /* (b) the session key of some s* was revealed */+ | (Ex #i1. SessionKeyReveal( sp ) @ i1)++ | (/* 2. s is an initiator session */ + (role = 'I') &+ + ( /* (a) A was corrupted before expire*/ + (Ex #k. Corrupt(A) @ k &+ ( (Ex #l. Expire(s) @ l & k < l)+ | not (Ex #l. Expire(s) @ l )))++ | /* (b) A was corrupted and s's session state was revealed */+ (Ex #k #l. SessionStateReveal(s) @ k & Corrupt(A) @ l)++ | /* (c) B was corrupted */+ (Ex #k. Corrupt(B) @ k )))++ | (/* 2. s is a responder session */ + (role = 'R') &++ ( /* (a) A was corrupted */+ Ex #k. Corrupt(A) @ k )++ | /* (b) There is a matching session and */+ (Ex #k k_ role_. Complete( sp, role_, k_ ) @ k+ + /* there is a corrupt B before expire s* */+ & ( (Ex #k. Corrupt(B) @ k & + ( (Ex #l. Expire(sp) @ l & k < l)+ | not (Ex #l. Expire(sp) @ l )))++ /* or both session state reveal s* and corrupt B */+ | (Ex #k #l. SessionStateReveal(sp) @ k & Corrupt(B) @ l )))++ | /* (c) There is no matching session and */+ ( (not (Ex #k k_ role_. Complete( sp, role_, k_) @ k))+ /* there is corrupt B */+ & (Ex #k. Corrupt(B) @ k))))"++end
+ data/examples/ake/dh/UM_one_pass_fix.spthy view
@@ -0,0 +1,224 @@+theory UM_one_pass_fix+begin++/*+ The one-pass UM protocol. See+ "Combined Security Analysis of the One- and Three-Pass Unified Model Key Agreement Protocols"+ Sanjit Chatterjee, Alfred Menezes and Berkant Ustaoglu++ There is a flaw in the definition of the model and the proof.+ + The problem is that the session id does not contain the+ role and since this is a one-pass protocol, this means+ that a responder session <A,B,X> can match another+ responder session <B,A,X> if X is replayed.++ We therefore adapt the definition of clean in the paper+ as follows.+ We change+ 3. A is the responder and one of the following holds:+ (a) M issued Corrupt(A)+ (b) s* exists and M issued either Corrupt(B) before Expire(s*) + or both Corrupt(B) and SessionStateReveal(s*)+ (c) s* does not exist and M issued CORRUPT( B ).+ To+ 3. A is the responder and one of the following holds:+ (a) M issued Corrupt(A)+ (b) _An initiator session_+ s* exists and M issued either Corrupt(B) before Expire(s*) + or both Corrupt(B) and SessionStateReveal(s*)+ (c) _No initiator session_ s* exists and M issued CORRUPT( B ).++*/++builtins: diffie-hellman, hashing++/* Key registration */++rule Register_key_honest:+ let pkA = 'g'^~ea+ in+ [ Fr( ~ea ) // select random longterm private+ ] + --[ KeyReg( $A ) ]-> // a key for A has been registered+ [ !Ltk( $A, ~ea ) // ~ea is the longterm private key of A+ , !Pk( $A, pkA ) // pkA = 'g'^~ea is the longterm public key of A+ , Out( pkA ) ] // the adversary can learn the public key ++/* Initiator */+++// Activate the session: choose ephemeral private key, compute ephemeral public key X.+rule I_Activate:+ let X = 'g'^~ex // the ephemeral public key+ sid = <$A, $B, X> // the session id, not unique because there might+ // be responder session with actor B and peer A+ // which receives X+ in+ [ Fr( ~ex ) ] // select random ephemeral private key+ --[ Activate( sid ) ]-> // sid is 'Activate'd after this step+ [ I_Act( ~ex, $A, $B ) // the state of this session, identified by ex (unique)+ , !SessionState( sid, $A, ~ex ) // the session state of sid with actor $A consists only of ex,+ // available for reveals+ ]++// Complete the session: send X, and compute key.+rule I_Complete:+ let X = 'g'^~ex // recompute X+ sid = <$A, $B, X> // recompute sid+ pB = 'g'^~eb // we do not model key registration by adversary,+ // hence key always of this form+ k = h(pB^~ex, pB^~ea, $A, $B) // we do not include the public string+ in+ [ I_Act( ~ex, $A, $B ) // this session was activated+ , !Ltk( $A, ~ea ) // lookup own longterm private key+ , !Pk( $B, pB ) ] // lookup peer's public key+ --[ Complete( sid, 'I', k ) ]-> // sid is 'Complete'd after this step+ [ I_Comp( sid ) // state of this session+ , Out( <$B, $A, X> ) // send message+ , !SessionKey( sid, $A, k ) ] // the session key of sid with actor $A, available+ // for reveals+// Expire the session+rule I_Expire:+ [ I_Comp( sid ) ]+ --[ Expire( sid ) ]-> // sid is expired after this step+ [ ]+++/* Responder */++// R has no Activated state since there is no ephemeral key.+rule R_Complete:+ let pA = 'g'^~ea // we do not model key registration by adversary,+ // hence key always of this form+ sid = <$B, $A, X> // sid is not unique because of initiator sessions with+ // same sid and replay+ k = h(X^~eb, pA^~eb, $A, $B )+ in+ [ In( X )+ , !Ltk( $B, ~eb )+ , !Pk( $A, pA ) ]+ --[ Activate(sid), Complete( sid, 'R', k ) ]-> // sid is 'Complete'd and 'Activate'd after this step+ [ R_Comp( sid )+ , !SessionKey( sid, $B, k )+ ]++rule R_Expire:+ [ R_Comp( sid ) ]+ --[ Expire( sid ) ]-> // sid is expired after this step+ [ ]++/* Corrupt an agent:+ We model corruption by three different rules.+ We do not model static key selection for corrupted agents.+*/++// Corrupt and obtain longterm key+rule Corrupt_Ltk:+ [ !Ltk( $A, ~ea ) ]+ --[ Corrupt( $A ) ]->+ [ Out( ~ea ) ]++// Corrupt and obtain session state. Must occur before complete which+// we ensure with BeforeComplete action and axiom.+rule Corrupt_SessionState:+ [ !SessionState( sid, ~x, $A ) ]+ --[ Corrupt( $A ), BeforeComplete( sid ) ]->+ [ Out( ~x ) ]++// Corrupt and obtain session key. Must occur before expire which+// we ensure with BeforeExpire action and axiom.+rule Corrupt_SessionKey:+ [ !SessionKey( sid, $A, k ) ]+ --[ Corrupt( $A ), BeforeExpire( sid ) ]->+ [ Out( k ) ]++/* Reveals for session state and session key */++rule Reveal_SessionState:+ [ !SessionState( sid, ~x, $A ) ]+ --[SessionStateReveal( sid ), BeforeComplete( sid ) ]->+ [ Out( ~x ) ]++rule Reveal_SessionKey:+ [ !SessionKey( sid, $A, k) ]+ --[ SessionKeyReveal( sid ), BeforeExpire( sid ) ]->+ [ Out( k ) ]++/* We only consider traces which satisfy these axioms */++// we enforce unique sids since the paper states that "At any point in time a session is+// in exactly one of the following states: active, completed, aborted, expired."+axiom sid_unique:+ "All #i #j sid. Activate(sid) @ i & Activate(sid) @ j ==> #i = #j"++// every agent has at most one registered key+axiom keyreg_unique:+ "All #i #j A. KeyReg(A) @ i & KeyReg(A) @ j ==> #i = #j"++// The reveals and the corrupt rules that reveal session state and session key are not performed+// too late.+axiom corrupt_and_reveal_not_too_early:+ " (All #i #j s role_ k_. BeforeComplete( s ) @ i & Complete(s, role_, k_ ) @ j ==> #i < #j)+ & (All #i #j s. BeforeExpire( s ) @ i & Expire( s ) @ j ==> #i < #j)"++// Key agreement for initiator and responder is reachable without any adversary interaction.+lemma key_agreement_reachable:+ exists-trace+ "Ex #i #j sid sidm k.+ Complete( sid , 'I', k ) @ i+ & Complete( sidm, 'R', k ) @ j+ & (not (Ex #j C. Corrupt( C ) @ j))+ & (not (Ex #j s. SessionKeyReveal( s ) @ j))+ & (not (Ex #j s. SessionStateReveal( s ) @ j))"+++lemma CK_secure:+ "(All #i #j role A B X k s sp.+ /* The key of a complete session 's' is known (whose partner is 'sp') */+ Complete( <A,B,X> , role, k ) @ i & K( k ) @ j & s = <A,B,X> & sp = <B,A,X>+ /* then one of the following must have happened */+ ==>+ /* 1. (a) The session key of s was revealed */+ (Ex #k. SessionKeyReveal( s ) @ k)++ /* (b) the session key of some s* was revealed */+ | (Ex #i1. SessionKeyReveal( sp ) @ i1)++ | (/* 2. s is an initiator session */ + (role = 'I') &+ + ( /* (a) A was corrupted before expire*/ + (Ex #k. Corrupt(A) @ k &+ ( (Ex #l. Expire(s) @ l & k < l)+ | not (Ex #l. Expire(s) @ l )))++ | /* (b) A was corrupted and s's session state was revealed */+ (Ex #k #l. SessionStateReveal(s) @ k & Corrupt(A) @ l)++ | /* (c) B was corrupted */+ (Ex #k. Corrupt(B) @ k )))++ | (/* 2. s is a responder session */ + (role = 'R') &++ ( /* (a) A was corrupted */+ Ex #k. Corrupt(A) @ k )++ | /* (b) There is a matching initiator session and */+ (Ex #k k_. Complete( sp, 'I', k_ ) @ k+ + /* there is a corrupt B before expire s* */+ & ( (Ex #k. Corrupt(B) @ k & + ( (Ex #l. Expire(sp) @ l & k < l)+ | not (Ex #l. Expire(sp) @ l )))++ /* or both session state reveal s* and corrupt B */+ | (Ex #k #l. SessionStateReveal(sp) @ k & Corrupt(B) @ l )))++ | /* (c) There is no matching initiator session and */+ ( (not (Ex #k k_ . Complete( sp, 'I', k_) @ k))+ /* there is corrupt B */+ & (Ex #k. Corrupt(B) @ k))))"++end
+ data/examples/ake/dh/UM_three_pass.spthy view
@@ -0,0 +1,244 @@+theory UM_three_pass+begin++/*+ The three-pass UM protocol. See+ "Combined Security Analysis of the One- and Three-Pass Unified Model Key Agreement Protocols"+ Sanjit Chatterjee, Alfred Menezes and Berkant Ustaoglu+*/++builtins: diffie-hellman, hashing, multiset+functions: MAC/2, first/1, second/1, concat/2+equations: concat(first(x), second(x)) = x++/* Key registration */++rule Register_key_honest:+ let pkA = 'g'^~ea+ in+ [ Fr( ~ea ) ] // select random longterm private+ --[ KeyReg( $A ) ]-> // a key for A has been registered+ [ !Ltk( $A, ~ea ) // ~ea is the longterm private key of A+ , !Pk( $A, pkA ) // pkA = 'g'^~ea is the longterm public key of A+ , Out( pkA ) ] // the adversary can learn the public key +++/* Initiator */++// UM3 session creation for initiator:+// choose ephemeral private key, compute ephemeral public key X, and send+rule I_Activate:+ let X = 'g'^~ex // the ephemeral public key+ sid = <'UM3', $A, $B, X> // the session id is unique+ in+ [ Fr( ~ex ) ] // select random ephemeral private key+ --[ Activate( sid )+ , Sid( sid )+ , Agents($A,$B) ]-> // sid is 'Activate'd after this step+ [ I_Act( ~ex, $A, $B ) // the state of this session, identified by ~ex (unique)+ , !SessionState( sid, $A, ~ex ) // the session state of sid with actor $A consists only of ex,+ // available for reveals+ , Out( X ) // send message+ ]++// UM3 session update for initiator:+// receive key confirmation and Y, compute key, check key confirmation.+rule I_Complete:+ let X = 'g'^~ex // recompute X + pB = 'g'^~eb // we do not model key registration by adversary,+ // hence key always of this form+ kstring = h(Y^~ex, pB^~ea, $A, $B, X, Y) // we do not include the public string Lambda+ key = second(kstring)+ conf = MAC(first(kstring), <'R', $B, $A, Y, X>) // we do not include Lambda_1+ confB = MAC(first(kstring), <'I', $A, $B, X, Y>) // we do not include Lambda_2+ sidOld = <'UM3',$A, $B, <'1',X>>+ sid = <'UM3',$A, $B, <'1',X> + <'2', <Y,confB>> + <'3', conf> > // new sid+ in+ [ I_Act( ~ex, $A, $B ) // this session was activated+ , In( <Y, confB> )+ , !Ltk( $A, ~ea ) // lookup own longterm private key+ , !Pk( $B, pB ) ] // lookup peer's public key+ --[ Complete( sid, 'I', key ) // sid is 'Complete'd after this step+ , SidUpdated( sidOld )+ , Sid( sid ) ]-> + [ I_Comp( sid ) // state of this session+ , Out( conf )+ , !SessionKey( sid, $A, key ) ] // the session key of sid with actor $A, available+ // for reveals+// UM3 session expiration+rule I_Expire:+ [ I_Comp( sid ) ]+ --[ Expire( sid ) ]-> // sid is expired after this step+ [ ]+++/* Responder */+// Session creation:+rule R_Activate:+ let pA = 'g'^~ea // we do not model key registration by adversary,+ // hence key always of this form+ Y = 'g'^~ey+ kstring = h(X^~ey, pA^~eb, $A, $B, X, Y )+ key = second(kstring)+ conf = MAC(first(kstring), <'I', $A, $B, X, Y>) // we do not include Lambda_2+ sid = <'UM3', $B, $A, <'1',X> + <'2',<Y, conf>> > // sid is unique+++ in+ [ Fr( ~ey )+ , In( X )+ , !Ltk( $B, ~eb )+ , !Pk( $A, pA ) ]+ --[ Activate(sid)+ , Sid( sid )+ , Agents($A,$B) ]-> + [ Out( <Y,conf>)+ , R_Act( ~ey, $B, $A, X )+ , !SessionState( sid, $A, ~ey )+ ]++// Session update:+rule R_Complete:+ let pA = 'g'^~ea+ Y = 'g'^~ey+ kstring = h(X^~ey, pA^~eb, $A, $B, X, Y )+ key = second(kstring)+ confA = MAC(first(kstring), <'R', $B, $A, Y, X>) // we do not include Lambda_1+ conf = MAC(first(kstring), <'I', $A, $B, X, Y>) // we do not include Lambda_2+ sidOld = <'UM3', $B, $A, <'1',X> + <'2', <Y, conf>>> // sid is unique+ sid = <'UM3', $B, $A, <'1',X> + <'2', <Y, conf>> + <'3', confA> > // sid is unique+ in+ [ R_Act( ~ey, $B, $A, X )+ , In( confA )+ , !Ltk( $B, ~eb )+ , !Pk( $A, pA )+ ]+ --[ Complete( sid, 'R', key ) // sid is 'Complete'd after this step+ , SidUpdated( sidOld )+ , Sid( sid ) ]->+ [ R_Comp( sid )+ , !SessionKey( sid, $B, key ) ] // the session key of sid with actor $B, available+ // for reveals+ ++rule R_Expire:+ [ R_Comp( sid ) ]+ --[ Expire( sid ) ]->+ [ ]++/* Corrupt an agent:+ We model corruption by three different rules.+ We do not model static key selection for corrupted agents.+*/++// Corrupt and obtain longterm key+rule Corrupt_Ltk:+ [ !Ltk( $A, ~ea ) ]+ --[ Corrupt( $A ) ]->+ [ Out( ~ea ) ]++// Corrupt and obtain session state. Must occur before complete which+// we ensure with BeforeComplete action and axiom.+rule Corrupt_SessionState:+ [ !SessionState( sid, ~x, $A ) ]+ --[ Corrupt( $A ), BeforeComplete( sid ) ]->+ [ Out( ~x ) ]++// Corrupt and obtain session key. Must occur before expire which+// we ensure with BeforeExpire action and axiom.+rule Corrupt_SessionKey:+ [ !SessionKey( sid, $A, k ) ]+ --[ Corrupt( $A ), BeforeExpire( sid ) ]->+ [ Out( k ) ]++/* Reveals for session state and session key */++rule Reveal_SessionState:+ [ !SessionState( sid, ~x, $A ) ]+ --[SessionStateReveal( sid ), BeforeComplete( sid ) ]->+ [ Out( ~x ) ]++rule Reveal_SessionKey:+ [ !SessionKey( sid, $A, k) ]+ --[ SessionKeyReveal( sid ), BeforeExpire( sid ) ]->+ [ Out( k ) ]++/* We only consider traces which satisfy these axioms */++// we enforce unique sids since the paper states that "At any point in time a session is+// in exactly one of the following states: active, completed, aborted, expired."+axiom sid_unique:+ "All #i #j sid. Activate(sid) @ i & Activate(sid) @ j ==> #i = #j"++// every agent has at most one registered key+axiom keyreg_unique:+ "All #i #j A. KeyReg(A) @ i & KeyReg(A) @ j ==> #i = #j"++// this assumption is used in the proof. Without this restriction, a completed+// session with actor and peer A is its own matching session.+//axiom actor_ineq_peer:+// "not (Ex #i A. Agents(A,A) @ i)"++// The reveals and the corrupt rules that reveal session state and session key are not performed+// too late.+axiom corrupt_and_reveal_not_too_early:+ " (All #i #j s role_ k_. BeforeComplete( s ) @ i & Complete(s, role_, k_ ) @ j ==> #i < #j)+ & (All #i #j s. BeforeExpire( s ) @ i & Expire( s ) @ j ==> #i < #j)"++// Key agreement for initiator and responder is reachable without any adversary interaction.+lemma key_agreement_reachable:+ exists-trace+ "Ex #i #j sid sidm k.+ Complete( sid , 'I', k ) @ i+ & Complete( sidm, 'R', k ) @ j+ & (not (Ex #j C. Corrupt( C ) @ j))+ & (not (Ex #j s. SessionKeyReveal( s ) @ j))+ & (not (Ex #j s. SessionStateReveal( s ) @ j))"+++lemma CK_secure_UM3:+ "(All #i #j role A B k s comm.+ /* The key of a complete session 's' is known */+ Complete( <'UM3',A,B,comm> , role, k ) @ i & K( k ) @ j & s = <'UM3',A,B,comm>+ /* then one of the following must have happened */+ ==>+ /* 1. (a) The session key of s was revealed (see 4. for 1. (b)) */+ (Ex #k. SessionKeyReveal( s ) @ k)++ /* 2. Corrupt(A) before Expire(s) */+ | (Ex #k. Corrupt(A) @ k &+ ( not (Ex #l. Expire(s) @ l & l < k)))+ + /* 3. SessionStateReveal(s) and either Corrupt(A) or Corrupt(B) */+ | (Ex #k. SessionStateReveal(s) @ k+ & ((Ex #l. Corrupt(A) @ l) | (Ex #l. Corrupt(B) @ l)))++ /* 4. s* exists and */+ | (Ex #l ms matchingComm.+ Sid(<'UM3',B,A,matchingComm>) @ l+ & ms = <'UM3',B,A,matchingComm>+ & ((Ex rest. matchingComm + rest = comm) | matchingComm = comm)+ // the session has not been updated+ & not (Ex #v. SidUpdated(ms) @ v)++ & (+ /* SessionKeyReveal(s*) (see 1. (b)) */+ (Ex #k. SessionKeyReveal( ms ) @ k)+ /* (a) Corrupt(B) before Expire(s*) */+ | (Ex #k. Corrupt(B) @ k &+ (not (Ex #l. Expire(ms) @ l & l < k)))+ /* (b) SessionStateReveal(s*) and either Corrupt(A) or Corrupt(B) */+ | (Ex #k. SessionStateReveal(ms) @ k+ & ((Ex #l. Corrupt(A) @ l) | (Ex #l. Corrupt(B) @ l)))))++ /* 5. s* does not exist and Corrupt(B) before Expire(s) */+ | ((not (Ex #l matchingComm.+ Sid(<'UM3',B,A,matchingComm>) @ l+ & ((Ex rest. matchingComm + rest = comm) | matchingComm = comm)+ // the session has not been updated+ & not (Ex #v. SidUpdated(<'UM3',B,A,matchingComm>) @ v)))+ + & (Ex #k. Corrupt(B) @ k &+ (not (Ex #l. Expire(s) @ l & l < k)))))"+ +end
+ data/examples/ake/dh/UM_three_pass_combined.spthy view
@@ -0,0 +1,309 @@+theory UM_three_pass_combined+begin++/*+ The three-pass UM protocol. See+ "Combined Security Analysis of the One- and Three-Pass Unified Model Key Agreement Protocols"+ Sanjit Chatterjee, Alfred Menezes and Berkant Ustaoglu+*/++builtins: diffie-hellman, hashing, multiset+functions: MAC/2, first/1, second/1, concat/2+equations: concat(first(x), second(x)) = x++/* Key registration */++rule Register_key_honest:+ let pkA = 'g'^~ea+ in+ [ Fr( ~ea ) ] // select random longterm private+ --[ KeyReg( $A ) ]-> // a key for A has been registered+ [ !Ltk( $A, ~ea ) // ~ea is the longterm private key of A+ , !Pk( $A, pkA ) // pkA = 'g'^~ea is the longterm public key of A+ , Out( pkA ) ] // the adversary can learn the public key +++/* UM3 Initiator */++// UM3 session creation for initiator:+// choose ephemeral private key, compute ephemeral public key X, and send+rule I_Activate:+ let X = 'g'^~ex // the ephemeral public key+ sid = <'UM3', $A, $B, X> // the session id is unique+ in+ [ Fr( ~ex ) ] // select random ephemeral private key+ --[ Activate( sid )+ , Sid( sid )+ , Agents($A,$B) ]-> // sid is 'Activate'd after this step+ [ I_Act( ~ex, $A, $B ) // the state of this session, identified by ~ex (unique)+ , !SessionState( sid, $A, ~ex ) // the session state of sid with actor $A consists only of ex,+ // available for reveals+ , Out( X ) // send message+ ]++// UM3 session update for initiator:+// receive key confirmation and Y, compute key, check key confirmation.+rule I_Complete:+ let X = 'g'^~ex // recompute X + pB = 'g'^~eb // we do not model key registration by adversary,+ // hence key always of this form+ kstring = h(Y^~ex, pB^~ea, $A, $B, X, Y) // we do not include the public string Lambda+ key = second(kstring)+ conf = MAC(first(kstring), <'R', $B, $A, Y, X>) // we do not include Lambda_1+ confB = MAC(first(kstring), <'I', $A, $B, X, Y>) // we do not include Lambda_2+ sidOld = <'UM3',$A, $B, <'1',X>>+ sid = <'UM3',$A, $B, <'1',X> + <'2', <Y,confB>> + <'3', conf> > // new sid+ in+ [ I_Act( ~ex, $A, $B ) // this session was activated+ , In( <Y, confB> )+ , !Ltk( $A, ~ea ) // lookup own longterm private key+ , !Pk( $B, pB ) ] // lookup peer's public key+ --[ Complete( sid, 'I', key ) // sid is 'Complete'd after this step+ , SidUpdated( sidOld )+ , Sid( sid ) ]-> + [ I_Comp( sid ) // state of this session+ , Out( conf )+ , !SessionKey( sid, $A, key ) ] // the session key of sid with actor $A, available+ // for reveals+// UM3 session expiration+rule I_Expire:+ [ I_Comp( sid ) ]+ --[ Expire( sid ) ]-> // sid is expired after this step+ [ ]+++/* UM3_Responder */+// Session creation:+rule R_Activate:+ let pA = 'g'^~ea // we do not model key registration by adversary,+ // hence key always of this form+ Y = 'g'^~ey+ kstring = h(X^~ey, pA^~eb, $A, $B, X, Y )+ key = second(kstring)+ conf = MAC(first(kstring), <'I', $A, $B, X, Y>) // we do not include Lambda_2+ sid = <'UM3', $B, $A, <'1',X> + <'2',<Y, conf>> > // sid is unique+++ in+ [ Fr( ~ey )+ , In( X )+ , !Ltk( $B, ~eb )+ , !Pk( $A, pA ) ]+ --[ Activate(sid)+ , Sid( sid )+ , Agents($A,$B) ]-> + [ Out( <Y,conf>)+ , R_Act( ~ey, $B, $A, X )+ , !SessionState( sid, $A, ~ey )+ ]++// Session update:+rule R_Complete:+ let pA = 'g'^~ea+ Y = 'g'^~ey+ kstring = h(X^~ey, pA^~eb, $A, $B, X, Y )+ key = second(kstring)+ confA = MAC(first(kstring), <'R', $B, $A, Y, X>) // we do not include Lambda_1+ conf = MAC(first(kstring), <'I', $A, $B, X, Y>) // we do not include Lambda_2+ sidOld = <'UM3', $B, $A, <'1',X> + <'2', <Y, conf>>> // sid is unique+ sid = <'UM3', $B, $A, <'1',X> + <'2', <Y, conf>> + <'3', confA> > // sid is unique+ in+ [ R_Act( ~ey, $B, $A, X )+ , In( confA )+ , !Ltk( $B, ~eb )+ , !Pk( $A, pA )+ ]+ --[ Complete( sid, 'R', key ) // sid is 'Complete'd after this step+ , SidUpdated( sidOld )+ , Sid( sid ) ]->+ [ R_Comp( sid )+ , !SessionKey( sid, $B, key ) ] // the session key of sid with actor $B, available+ // for reveals+rule R_Expire:+ [ R_Comp( sid ) ]+ --[ Expire( sid ) ]->+ [ ]+++/* UM1 Initiator */+// We prefix all facts with UM1++// Activate the session: choose ephemeral private key, compute ephemeral public key X.+rule UM1_I_Activate:+ let X = 'g'^~ex // the ephemeral public key+ sid = <$A, $B, X> // the session id, not unique because there might+ // be responder session with actor B and peer A+ // which receives X+ in+ [ Fr( ~ex ) ] // select random ephemeral private key+ --[ UM1_Activate( sid ) ]-> // sid is 'Activate'd after this step+ [ UM1_I_Act( ~ex, $A, $B ) // the state of this session, identified by ex (unique)+ , !SessionState( sid, $A, ~ex ) // the session state of sid with actor $A consists only of ex,+ // available for reveals+ ]++// Complete the session: send X, and compute key.+rule UM1_I_Complete:+ let X = 'g'^~ex // recompute X+ sid = <$A, $B, X> // recompute sid+ pB = 'g'^~eb // we do not model key registration by adversary,+ // hence key always of this form+ k = h(pB^~ex, pB^~ea, $A, $B, X, pB)+ in+ [ UM1_I_Act( ~ex, $A, $B ) // this session was activated+ , !Ltk( $A, ~ea ) // lookup own longterm private key+ , !Pk( $B, pB ) ] // lookup peer's public key+ --[ UM1_Complete( sid, 'I', k ) ]-> // sid is 'Complete'd after this step+ [ UM1_I_Comp( sid ) // state of this session+ , Out( <$B, $A, X> ) // send message+ , !SessionKey( sid, $A, k ) ] // the session key of sid with actor $A, available+ // for reveals+// Expire the session+rule UM1_I_Expire:+ [ UM1_I_Comp( sid ) ]+ --[ UM1_Expire( sid ) ]-> // sid is expired after this step+ [ ]+++/* UM1 Responder */++// R has no Activated state since there is no ephemeral key.+rule UM1_R_Complete:+ let pA = 'g'^~ea // we do not model key registration by adversary,+ // hence key always of this form+ sid = <$B, $A, X> // sid is not unique because of initiator sessions with+ // same sid and replay+ k = h(X^~eb, pA^~eb, $A, $B, X, 'g'^~eb)+ in+ [ In( X )+ , !Ltk( $B, ~eb )+ , !Pk( $A, pA ) ]+ --[ UM1_Activate(sid)+ , UM1_Complete( sid, 'R', k )+ ]-> // sid is 'Complete'd and 'Activate'd after this step+ [ UM1_R_Comp( sid )+ , !SessionKey( sid, $B, k )+ ]++rule UM1_R_Expire:+ [ UM1_R_Comp( sid ) ]+ --[ UM1_Expire( sid ) ]-> // sid is expired after this step+ [ ]+++/* Corrupt an agent:+ We model corruption by three different rules.+ We do not model static key selection for corrupted agents.+*/++// Corrupt and obtain longterm key+rule Corrupt_Ltk:+ [ !Ltk( $A, ~ea ) ]+ --[ Corrupt( $A ) ]->+ [ Out( ~ea ) ]++// Corrupt and obtain session state. Must occur before complete which+// we ensure with BeforeComplete action and axiom.+rule Corrupt_SessionState:+ [ !SessionState( sid, ~x, $A ) ]+ --[ Corrupt( $A ), BeforeComplete( sid ) ]->+ [ Out( ~x ) ]++// Corrupt and obtain session key. Must occur before expire which+// we ensure with BeforeExpire action and axiom.+rule Corrupt_SessionKey:+ [ !SessionKey( sid, $A, k ) ]+ --[ Corrupt( $A ), BeforeExpire( sid ) ]->+ [ Out( k ) ]++/* Reveals for session state and session key */++rule Reveal_SessionState:+ [ !SessionState( sid, ~x, $A ) ]+ --[SessionStateReveal( sid ), BeforeComplete( sid ) ]->+ [ Out( ~x ) ]++rule Reveal_SessionKey:+ [ !SessionKey( sid, $A, k) ]+ --[ SessionKeyReveal( sid ), BeforeExpire( sid ) ]->+ [ Out( k ) ]++/* We only consider traces which satisfy these axioms */++// we enforce unique sids since the paper states that "At any point in time a session is+// in exactly one of the following states: active, completed, aborted, expired."+axiom sid_unique:+ "All #i #j sid. UM1_Activate(sid) @ i & UM1_Activate(sid) @ j ==> #i = #j"++// every agent has at most one registered key+axiom keyreg_unique:+ "All #i #j A. KeyReg(A) @ i & KeyReg(A) @ j ==> #i = #j"++// this assumption is used in the proof. Without this restriction, a completed+// session with actor and peer A is its own matching session.+axiom actor_ineq_peer:+ "not (Ex #i A. Agents(A,A) @ i)"++// The reveals and the corrupt rules that reveal session state and session key are not performed+// too late.+axiom corrupt_and_reveal_not_too_early:+ " (All #i #j s role_ k_. BeforeComplete( s ) @ i & Complete(s, role_, k_ ) @ j ==> #i < #j)+ & (All #i #j s. BeforeExpire( s ) @ i & Expire( s ) @ j ==> #i < #j)"++// Key agreement for initiator and responder is reachable without any adversary interaction.+lemma key_agreement_reachable:+ exists-trace+ "Ex #i #j sid sidm k.+ Complete( sid , 'I', k ) @ i+ & Complete( sidm, 'R', k ) @ j+ & (not (Ex #j C. Corrupt( C ) @ j))+ & (not (Ex #j s. SessionKeyReveal( s ) @ j))+ & (not (Ex #j s. SessionStateReveal( s ) @ j))"+++lemma CK_secure_UM3:+ "(All #i #j role A B k s comm.+ /* The key of a complete session 's' is known */+ Complete( <'UM3',A,B,comm> , role, k ) @ i & K( k ) @ j & s = <'UM3',A,B,comm>+ /* then one of the following must have happened */+ ==>+ /* 1. (a) The session key of s was revealed (see 4. for 1. (b)) */+ (Ex #k. SessionKeyReveal( s ) @ k)++ /* 2. Corrupt(A) before Expire(s) */+ | (Ex #k. Corrupt(A) @ k &+ ( not (Ex #l. Expire(s) @ l & l < k)))+ + /* 3. SessionStateReveal(s) and either Corrupt(A) or Corrupt(B) */+ | (Ex #k. SessionStateReveal(s) @ k+ & ((Ex #l. Corrupt(A) @ l) | (Ex #l. Corrupt(B) @ l)))++ /* 4. s* exists and */+ | (Ex #l ms matchingComm.+ Sid(<'UM3',B,A,matchingComm>) @ l+ & ms = <'UM3',B,A,matchingComm>+ & ((Ex rest. matchingComm + rest = comm) | matchingComm = comm)+ // the session has not been updated+ & not (Ex #v. SidUpdated(ms) @ v)++ & (+ /* SessionKeyReveal(s*) (see 1. (b)) */+ (Ex #k. SessionKeyReveal( ms ) @ k)+ /* (a) Corrupt(B) before Expire(s*) */+ | (Ex #k. Corrupt(B) @ k &+ (not (Ex #l. Expire(ms) @ l & l < k)))+ /* (b) SessionStateReveal(s*) and either Corrupt(A) or Corrupt(B) */+ | (Ex #k. SessionStateReveal(ms) @ k+ & ((Ex #l. Corrupt(A) @ l) | (Ex #l. Corrupt(B) @ l)))))++ /* 5. s* does not exist and Corrupt(B) before Expire(s) */+ | ((not (Ex #l matchingComm.+ Sid(<'UM3',B,A,matchingComm>) @ l+ & ((Ex rest. matchingComm + rest = comm) | matchingComm = comm)+ // the session has not been updated+ & not (Ex #v. SidUpdated(<'UM3',B,A,matchingComm>) @ v)))+ + & (Ex #k. Corrupt(B) @ k &+ (not (Ex #l. Expire(s) @ l & l < k)))))"+ +end
+ data/examples/ake/dh/UM_three_pass_combined_fixed.spthy view
@@ -0,0 +1,356 @@+theory UM_three_pass_combined+begin++/*+ The three-pass UM protocol. See+ "Combined Security Analysis of the One- and Three-Pass Unified Model Key Agreement Protocols"+ Sanjit Chatterjee, Alfred Menezes and Berkant Ustaoglu+*/++builtins: diffie-hellman, hashing, multiset+functions: MAC/2, first/1, second/1, concat/2+equations: concat(first(x), second(x)) = x++/* Key registration */++rule Register_key_honest:+ let pkA = 'g'^~ea+ in+ [ Fr( ~ea ) ] // select random longterm private+ --[ KeyReg( $A ) ]-> // a key for A has been registered+ [ !Ltk( $A, ~ea ) // ~ea is the longterm private key of A+ , !Pk( $A, pkA ) // pkA = 'g'^~ea is the longterm public key of A+ , Out( pkA ) ] // the adversary can learn the public key +++/* UM3 Initiator */++// UM3 session creation for initiator:+// choose ephemeral private key, compute ephemeral public key X, and send+rule I_Activate:+ let X = 'g'^~ex // the ephemeral public key+ sid = <'UM3', $A, $B, X> // the session id is unique+ in+ [ Fr( ~ex ) ] // select random ephemeral private key+ --[ Activate( sid )+ , Sid( sid )+ , Agents($A,$B) ]-> // sid is 'Activate'd after this step+ [ I_Act( ~ex, $A, $B ) // the state of this session, identified by ~ex (unique)+ , !SessionState( sid, $A, ~ex ) // the session state of sid with actor $A consists only of ex,+ // available for reveals+ , Out( X ) // send message+ ]++// UM3 session update for initiator:+// receive key confirmation and Y, compute key, check key confirmation.+rule I_Complete:+ let X = 'g'^~ex // recompute X + pB = 'g'^~eb // we do not model key registration by adversary,+ // hence key always of this form+ kstring = h(Y^~ex, pB^~ea, $A, $B, X, Y, 'UM3') // we do not include the public string Lambda+ key = second(kstring)+ conf = MAC(first(kstring), <'R', $B, $A, Y, X>) // we do not include Lambda_1+ confB = MAC(first(kstring), <'I', $A, $B, X, Y>) // we do not include Lambda_2+ sidOld = <'UM3',$A, $B, <'1',X>>+ sid = <'UM3',$A, $B, <'1',X> + <'2', <Y,confB>> + <'3', conf> > // new sid+ in+ [ I_Act( ~ex, $A, $B ) // this session was activated+ , In( <Y, confB> )+ , !Ltk( $A, ~ea ) // lookup own longterm private key+ , !Pk( $B, pB ) ] // lookup peer's public key+ --[ Complete( sid, 'I', key ) // sid is 'Complete'd after this step+ , SidUpdated( sidOld )+ , Sid( sid ) ]-> + [ I_Comp( sid ) // state of this session+ , Out( conf )+ , !SessionKey( sid, $A, key ) ] // the session key of sid with actor $A, available+ // for reveals+// UM3 session expiration+rule I_Expire:+ [ I_Comp( sid ) ]+ --[ Expire( sid ) ]-> // sid is expired after this step+ [ ]+++/* UM3_Responder */+// Session creation:+rule R_Activate:+ let pA = 'g'^~ea // we do not model key registration by adversary,+ // hence key always of this form+ Y = 'g'^~ey+ kstring = h(X^~ey, pA^~eb, $A, $B, X, Y, 'UM3')+ key = second(kstring)+ conf = MAC(first(kstring), <'I', $A, $B, X, Y>) // we do not include Lambda_2+ sid = <'UM3', $B, $A, <'1',X> + <'2',<Y, conf>> > // sid is unique+++ in+ [ Fr( ~ey )+ , In( X )+ , !Ltk( $B, ~eb )+ , !Pk( $A, pA ) ]+ --[ Activate(sid)+ , Sid( sid )+ , Agents($A,$B) ]-> + [ Out( <Y,conf>)+ , R_Act( ~ey, $B, $A, X )+ , !SessionState( sid, $A, ~ey )+ ]++// Session update:+rule R_Complete:+ let pA = 'g'^~ea+ Y = 'g'^~ey+ kstring = h(X^~ey, pA^~eb, $A, $B, X, Y, 'UM3' )+ key = second(kstring)+ confA = MAC(first(kstring), <'R', $B, $A, Y, X>) // we do not include Lambda_1+ conf = MAC(first(kstring), <'I', $A, $B, X, Y>) // we do not include Lambda_2+ sidOld = <'UM3', $B, $A, <'1',X> + <'2', <Y, conf>>> // sid is unique+ sid = <'UM3', $B, $A, <'1',X> + <'2', <Y, conf>> + <'3', confA> > // sid is unique+ in+ [ R_Act( ~ey, $B, $A, X )+ , In( confA )+ , !Ltk( $B, ~eb )+ , !Pk( $A, pA )+ ]+ --[ Complete( sid, 'R', key ) // sid is 'Complete'd after this step+ , SidUpdated( sidOld )+ , Sid( sid ) ]->+ [ R_Comp( sid )+ , !SessionKey( sid, $B, key ) ] // the session key of sid with actor $B, available+ // for reveals+rule R_Expire:+ [ R_Comp( sid ) ]+ --[ Expire( sid ) ]->+ [ ]+++/* UM1 Initiator */+// We prefix all facts with UM1++// Activate the session: choose ephemeral private key, compute ephemeral public key X.+rule UM1_I_Activate:+ let X = 'g'^~ex // the ephemeral public key+ sid = <$A, $B, X> // the session id, not unique because there might+ // be responder session with actor B and peer A+ // which receives X+ in+ [ Fr( ~ex ) ] // select random ephemeral private key+ --[ UM1_Activate( sid ) ]-> // sid is 'Activate'd after this step+ [ UM1_I_Act( ~ex, $A, $B ) // the state of this session, identified by ex (unique)+ , !SessionState( sid, $A, ~ex ) // the session state of sid with actor $A consists only of ex,+ // available for reveals+ ]++// Complete the session: send X, and compute key.+rule UM1_I_Complete:+ let X = 'g'^~ex // recompute X+ sid = <$A, $B, X> // recompute sid+ pB = 'g'^~eb // we do not model key registration by adversary,+ // hence key always of this form+ k = h(pB^~ex, pB^~ea, $A, $B, X, pB, 'UM1') // we do not include the public string+ in+ [ UM1_I_Act( ~ex, $A, $B ) // this session was activated+ , !Ltk( $A, ~ea ) // lookup own longterm private key+ , !Pk( $B, pB ) ] // lookup peer's public key+ --[ UM1_Complete( sid, 'I', k ) ]-> // sid is 'Complete'd after this step+ [ UM1_I_Comp( sid ) // state of this session+ , Out( <$B, $A, X> ) // send message+ , !SessionKey( sid, $A, k ) ] // the session key of sid with actor $A, available+ // for reveals+// Expire the session+rule UM1_I_Expire:+ [ UM1_I_Comp( sid ) ]+ --[ UM1_Expire( sid ) ]-> // sid is expired after this step+ [ ]+++/* UM1 Responder */++// R has no Activated state since there is no ephemeral key.+rule UM1_R_Complete:+ let pA = 'g'^~ea // we do not model key registration by adversary,+ // hence key always of this form+ sid = <$B, $A, X> // sid is not unique because of initiator sessions with+ // same sid and replay+ k = h(X^~eb, pA^~eb, $A, $B, X, 'g'^~eb, 'UM1' )+ in+ [ In( X )+ , !Ltk( $B, ~eb )+ , !Pk( $A, pA ) ]+ --[ UM1_Activate(sid)+ , UM1_Complete( sid, 'R', k )+ ]-> // sid is 'Complete'd and 'Activate'd after this step+ [ UM1_R_Comp( sid )+ , !SessionKey( sid, $B, k )+ ]++rule UM1_R_Expire:+ [ UM1_R_Comp( sid ) ]+ --[ UM1_Expire( sid ) ]-> // sid is expired after this step+ [ ]+++/* Corrupt an agent:+ We model corruption by three different rules.+ We do not model static key selection for corrupted agents.+*/++// Corrupt and obtain longterm key+rule Corrupt_Ltk:+ [ !Ltk( $A, ~ea ) ]+ --[ Corrupt( $A ) ]->+ [ Out( ~ea ) ]++// Corrupt and obtain session state. Must occur before complete which+// we ensure with BeforeComplete action and axiom.+rule Corrupt_SessionState:+ [ !SessionState( sid, ~x, $A ) ]+ --[ Corrupt( $A ), BeforeComplete( sid ) ]->+ [ Out( ~x ) ]++// Corrupt and obtain session key. Must occur before expire which+// we ensure with BeforeExpire action and axiom.+rule Corrupt_SessionKey:+ [ !SessionKey( sid, $A, k ) ]+ --[ Corrupt( $A ), BeforeExpire( sid ) ]->+ [ Out( k ) ]++/* Reveals for session state and session key */++rule Reveal_SessionState:+ [ !SessionState( sid, ~x, $A ) ]+ --[SessionStateReveal( sid ), BeforeComplete( sid ) ]->+ [ Out( ~x ) ]++rule Reveal_SessionKey:+ [ !SessionKey( sid, $A, k) ]+ --[ SessionKeyReveal( sid ), BeforeExpire( sid ) ]->+ [ Out( k ) ]++/* We only consider traces which satisfy these axioms */++// we enforce unique sids since the paper states that "At any point in time a session is+// in exactly one of the following states: active, completed, aborted, expired."+axiom sid_unique:+ "All #i #j sid. UM1_Activate(sid) @ i & UM1_Activate(sid) @ j ==> #i = #j"++// every agent has at most one registered key+axiom keyreg_unique:+ "All #i #j A. KeyReg(A) @ i & KeyReg(A) @ j ==> #i = #j"++// this assumption is used in the proof. Without this restriction, a completed+// session with actor and peer A is its own matching session.+axiom actor_ineq_peer:+ "not (Ex #i A. Agents(A,A) @ i)"++// The reveals and the corrupt rules that reveal session state and session key are not performed+// too late.+axiom corrupt_and_reveal_not_too_early:+ " (All #i #j s role_ k_. BeforeComplete( s ) @ i & Complete(s, role_, k_ ) @ j ==> #i < #j)+ & (All #i #j s. BeforeExpire( s ) @ i & Expire( s ) @ j ==> #i < #j)"++// Key agreement for initiator and responder is reachable without any adversary interaction.+lemma key_agreement_reachable:+ exists-trace+ "Ex #i #j sid sidm k.+ Complete( sid , 'I', k ) @ i+ & Complete( sidm, 'R', k ) @ j+ & (not (Ex #j C. Corrupt( C ) @ j))+ & (not (Ex #j s. SessionKeyReveal( s ) @ j))+ & (not (Ex #j s. SessionStateReveal( s ) @ j))"+++lemma CK_secure_UM3:+ "(All #i #j role A B k s comm.+ /* The key of a complete session 's' is known */+ Complete( <'UM3',A,B,comm> , role, k ) @ i & K( k ) @ j & s = <'UM3',A,B,comm>+ /* then one of the following must have happened */+ ==>+ /* 1. (a) The session key of s was revealed (see 4. for 1. (b)) */+ (Ex #k. SessionKeyReveal( s ) @ k)++ /* 2. Corrupt(A) before Expire(s) */+ | (Ex #k. Corrupt(A) @ k &+ ( not (Ex #l. Expire(s) @ l & l < k)))+ + /* 3. SessionStateReveal(s) and either Corrupt(A) or Corrupt(B) */+ | (Ex #k. SessionStateReveal(s) @ k+ & ((Ex #l. Corrupt(A) @ l) | (Ex #l. Corrupt(B) @ l)))++ /* 4. s* exists and */+ | (Ex #l ms matchingComm.+ Sid(<'UM3',B,A,matchingComm>) @ l+ & ms = <'UM3',B,A,matchingComm>+ & ((Ex rest. matchingComm + rest = comm) | matchingComm = comm)+ // the session has not been updated+ & not (Ex #v. SidUpdated(ms) @ v)++ & (+ /* SessionKeyReveal(s*) (see 1. (b)) */+ (Ex #k. SessionKeyReveal( ms ) @ k)+ /* (a) Corrupt(B) before Expire(s*) */+ | (Ex #k. Corrupt(B) @ k &+ (not (Ex #l. Expire(ms) @ l & l < k)))+ /* (b) SessionStateReveal(s*) and either Corrupt(A) or Corrupt(B) */+ | (Ex #k. SessionStateReveal(ms) @ k+ & ((Ex #l. Corrupt(A) @ l) | (Ex #l. Corrupt(B) @ l)))))++ /* 5. s* does not exist and Corrupt(B) before Expire(s) */+ | ((not (Ex #l matchingComm.+ Sid(<'UM3',B,A,matchingComm>) @ l+ & ((Ex rest. matchingComm + rest = comm) | matchingComm = comm)+ // the session has not been updated+ & not (Ex #v. SidUpdated(<'UM3',B,A,matchingComm>) @ v)))+ + & (Ex #k. Corrupt(B) @ k &+ (not (Ex #l. Expire(s) @ l & l < k)))))"++lemma CK_secure:+ "(All #i #j role A B X k s sp.+ /* The key of a complete session 's' is known (whose partner is 'sp') */+ UM1_Complete( <A,B,X> , role, k ) @ i & K( k ) @ j & s = <A,B,X> & sp = <B,A,X>+ /* then one of the following must have happened */+ ==>+ /* 1. (a) The session key of s was revealed */+ (Ex #k. SessionKeyReveal( s ) @ k)++ /* (b) the session key of some s* was revealed */+ | (Ex #i1. SessionKeyReveal( sp ) @ i1)++ | (/* 2. s is an initiator session */ + (role = 'I') &+ + ( /* (a) A was corrupted before expire*/ + (Ex #k. Corrupt(A) @ k &+ ( (Ex #l. Expire(s) @ l & k < l)+ | not (Ex #l. Expire(s) @ l )))++ | /* (b) A was corrupted and s's session state was revealed */+ (Ex #k #l. SessionStateReveal(s) @ k & Corrupt(A) @ l)++ | /* (c) B was corrupted */+ (Ex #k. Corrupt(B) @ k )))++ | (/* 2. s is a responder session */ + (role = 'R') &++ ( /* (a) A was corrupted */+ Ex #k. Corrupt(A) @ k )++ | /* (b) There is a matching initiator session and */+ (Ex #k k_. UM1_Complete( sp, 'I', k_ ) @ k+ + /* there is a corrupt B before expire s* */+ & ( (Ex #k. Corrupt(B) @ k & + ( (Ex #l. Expire(sp) @ l & k < l)+ | not (Ex #l. Expire(sp) @ l )))++ /* or both session state reveal s* and corrupt B */+ | (Ex #k #l. SessionStateReveal(sp) @ k & Corrupt(B) @ l )))++ | /* (c) There is no matching initiator session and */+ ( (not (Ex #k k_ . UM1_Complete( sp, 'I', k_) @ k))+ /* there is corrupt B */+ & (Ex #k. Corrupt(B) @ k))))" +end
+ data/examples/ake/dh/client_session_key.aes view
@@ -0,0 +1,1 @@+ÔZÀ[d'ám]ÌNÞÜælÎDùª-vóÃ]§ödTòDÿM}zSÒÕÈS>u¯·ëðU? kdmrõâg@cV42üújâ3kÉõ]PS
+ data/examples/cav13/DH_example.spthy view
@@ -0,0 +1,36 @@+theory ex1 begin++/*+ * Protocol: Diffie-Hellman with MAC+ * Modeler: Benedikt Schmidt+ * Described in: CAV 2013 Submission+ * Date: January 2013+ *+ * Status: Working+ */+++builtins: diffie-hellman+functions: mac/2, g/0, shk/0 [private]++rule Step1:+ [ Fr(tid:fresh), Fr(x:fresh) ]+ --[ ]->+ [ Out(<g^(x:fresh), mac(shk, <g^(x:fresh), A:pub, B:pub>)>)+ , Step1(tid:fresh, A:pub, B:pub, x:fresh) ]++rule Step2:+ [ Step1(tid, A, B, x:fresh), In(<Y, mac(shk, <Y, B, A>)>) ]+ --[ Accept(tid, Y^(x:fresh)) ]-> []++rule RevealKey: [ ] --[ Reveal() ]-> [ Out(shk) ]+++lemma Accept_Secret:+ "∀ #i #j tid key. Accept(tid, key) @ i & K(key) @ j+ ==> ∃ #l. Reveal() @ l & l < i"++lemma Accept_Secret_Counter:+ "∀ #i #j tid key. Accept(tid, key) @ i & K(key) @ j ==> F"++end
+ data/examples/features/multiset/counter.spthy view
@@ -0,0 +1,38 @@+theory counter begin++builtins: multiset, symmetric-encryption, hashing++rule Create:+ [ Fr(~s) ]+ --[ Start(~s) ]->+ [ Counter(~s, '1')]++rule Inc:+ [ Counter( ~s, x ), In( x ) ] // The In(x) could be nicely prevented by ensuring+ --[ Counter( ~s, x ) ]-> // that x never contains names by using the sort+ [ Counter( ~s, x + '1' ) // system.+ , Out( senc( x, ~s ) ) ]+++/* How can I ensure this lemma directly? */+lemma counters_linear_order[reuse,use_induction]:+ "All x y #i #j s.+ Counter(s,x) @ i & Counter(s,y) @ j+ ==> (Ex z. x + z = y) | (Ex z. y + z = x) | y = x"++lemma counter_start[reuse,use_induction]:+ "All #i x s.+ Counter(s,x) @ i ==> Ex #j. Start(s) @ j & #j < #i"++lemma counter_increases[reuse,use_induction]:+ "All x y #i #j s.+ Counter(s,x) @ i & Counter(s,y) @ j ==> #i < #j+ ==> Ex z. x + z = y"++lemma lesser_senc_secret[use_induction]:+ "All x y #i #j s.+ Counter(s,x) @ i & K(senc(h(y),s)) @ j+ ==> (#i < #j | Ex z. y + z = x)"++end+
+ data/examples/features/private_function_symbols/NAXOS_eCK_PFS_private.spthy view
@@ -0,0 +1,147 @@+theory NAXOS_eCK+begin++builtins: diffie-hellman++section{* NAXOS *}++/*+ * Protocol: NAXOS+ * Modeler: Cas Cremers, Benedikt Schmidt+ * Date: January 2012/April 2012/October 2012+ * Source: "Stronger Security of Authenticated Key Exchange"+ * LaMacchia, Lauter, Mityagin, 2007+ * Property: eCK security+ *+ * Status: Working+ */++functions: h1/1+functions: h2/1++/* We use the private function symbol sk to model the longterm secret key of an+ agent. For example, sk('A') is 'A's longterm secret key. The corresponding+ longterm public key is 'g'^sk('A').+*/+functions: sk/1 [private]++/* Protocol rules */++/* In the description in the paper, we omitted the sorts. + * In this description they are made explicit.+ * '$A' is equivalent to 'A:pub'+ * '~x' is equivalent to 'x:fresh'+ */++/* Initiator */+rule Init_1:+ let X = 'g'^h1(<~ex, sk($A) >) // $A uses its own longterm secret key+ in+ [ Fr( ~ex ) ]+ -->+ [ Init_1( ~ex, $A, $B )+ , !Ephk(~ex, ~ex)+ , Out( X ) ]++rule Init_2:+ let KB = 'g'^sk($B) // $A uses $B's longterm public key+ exp = h1(< ~ex, sk($A) >) // and its own longterm secret key+ X = 'g'^exp+ key = h2(< Y^sk($A), KB^exp, Y^exp, $A, $B >) + in+ [ Init_1( ~ex, $A, $B )+ , In( Y ) ]+ --[ Accept( ~ex, key)+ , Sid( ~ex, < $A, $B, X, Y, 'Init' >)+ ]->+ [ !Sessk( ~ex, key) ]++/* Responder */+rule Resp_1:+ let KA = 'g'^sk($A) // $B uses $A's longterm public key+ exp = h1(< ~ey, sk($B) >) // and its own longterm secret key+ Y = 'g'^exp+ key = h2(< KA^exp, X^sk($B), X^exp, $A, $B >) + in+ [ Fr( ~ey ), In( X ) ]+ --[ Accept( ~ey, key )+ , Sid( ~ey, < $B, $A, Y, X, 'Resp' > )+ ]->+ [ Out( Y ),+ !Ephk(~ey, ~ey),+ !Sessk( ~ey, key) ]++/* Key Reveals for the eCK model */+rule Sessk_reveal: + [ !Sessk(~s, k) ] --[ RevealSessk(~s) ]-> [ Out(k) ]++rule Ltk_reveal:+ [ ] --[ RevealLtk($A) ]-> [ Out(sk($A)) ]++rule Ephk_reveal:+ [ !Ephk(~s, ~ek) ] --[ RevealEphk(~s) ]-> [ Out(~ek) ]+++/* Security properties */+/*+lemma eCK_same_key:+ " // If every agent registered at most one public key+ (All A #i #j. RegKey(A)@i & RegKey(A)@j ==> (#i = #j))+ ==> // then matching sessions accept the same key+ (not (Ex #i1 #i2 #i3 #i4 s ss k kk A B minfo .+ Accept(s, A, B, k ) @ i1+ & Accept(ss, B, A, kk) @ i2+ & Sid(s, minfo) @ i3+ & Match(ss, minfo) @i4+ & not( k = kk )+ ) )"+*/++// This property is not satisfied by NAXOS.+lemma eCK_PFS_key_secrecy:+ /* + * The property specification is a (logically equivalent) simplified+ * version of the one in the original eCK (ProvSec) paper:+ *+ * If there exists a test session whose key k is known to the+ * Adversary with some session-id, then...+ */+ "(All #i1 #i2 #i3 test A B k sent recvd role.+ Accept(test, k) @ i1 & K( k ) @ i2 & Sid(test, < A, B, sent, recvd, role> ) @ i3+ ==> ( + /* ... the test session must be "not clean".+ * test is not clean if one of the following has happened:+ */+ /* 1. The adversary has revealed the session key of the test session. */+ (Ex #i3. RevealSessk( test ) @ i3 )+ + /* 2. The adversary has revealed both the longterm key of A and the+ ephemeral key of the test session */+ | (Ex #i5 #i6. RevealLtk ( A ) @ i5 & RevealEphk ( test ) @ i6 )++ /* 3. There is a matching session and */+ | (Ex matchingSession #i3 matchingRole.+ ( Sid ( matchingSession, < B, A, recvd, sent, matchingRole > ) @ i3 + & not ( matchingRole = role ) )+ & (+ /* (a) the adversary has revealed the session key of the matching session, or */+ (Ex #i5. RevealSessk( matchingSession ) @ i5 )++ /* (b) the adversary has revealed the longterm key of B and the ephemeral+ key of the matching session. */+ | (Ex #i5 #i6. RevealLtk ( B ) @ i5 & RevealEphk ( matchingSession ) @ i6 )+ )+ )+ /* 4. There is no matching session and */+ | ( ( not(Ex matchingSession #i3 matchingRole.+ ( Sid ( matchingSession, < B, A, recvd, sent, matchingRole > ) @ i3 + & not ( matchingRole = role ) )))++ /* the adversary has revealed the longterm key of B before test accepted the key. */+ & ( (Ex #i5. RevealLtk (B) @ i5 & i5 < i1)+ )+ )+ )+ )"++end
+ data/examples/features/private_function_symbols/NAXOS_eCK_private.spthy view
@@ -0,0 +1,146 @@+theory NAXOS_eCK+begin++builtins: diffie-hellman++section{* NAXOS *}++/*+ * Protocol: NAXOS+ * Modeler: Cas Cremers, Benedikt Schmidt+ * Date: January 2012/April 2012/October 2012+ * Source: "Stronger Security of Authenticated Key Exchange"+ * LaMacchia, Lauter, Mityagin, 2007+ * Property: eCK security+ *+ * Status: Working+ */++functions: h1/1+functions: h2/1++/* We use the private function symbol sk to model the longterm secret key of an+ agent. For example, sk('A') is 'A's longterm secret key. The corresponding+ longterm public key is 'g'^sk('A').+*/+functions: sk/1 [private]++/* Protocol rules */++/* In the description in the paper, we omitted the sorts. + * In this description they are made explicit.+ * '$A' is equivalent to 'A:pub'+ * '~x' is equivalent to 'x:fresh'+ */++/* Initiator */+rule Init_1:+ let X = 'g'^h1(<~ex, sk($A) >) // $A uses its own longterm secret key+ in+ [ Fr( ~ex ) ]+ -->+ [ Init_1( ~ex, $A, $B )+ , !Ephk(~ex, ~ex)+ , Out( X ) ]++rule Init_2:+ let KB = 'g'^sk($B) // $A uses $B's longterm public key+ exp = h1(< ~ex, sk($A) >) // and its own longterm secret key+ X = 'g'^exp+ key = h2(< Y^sk($A), KB^exp, Y^exp, $A, $B >) + in+ [ Init_1( ~ex, $A, $B )+ , In( Y ) ]+ --[ Accept( ~ex, key)+ , Sid( ~ex, < $A, $B, X, Y, 'Init' >)+ ]->+ [ !Sessk( ~ex, key) ]++/* Responder */+rule Resp_1:+ let KA = 'g'^sk($A) // $B uses $A's longterm public key+ exp = h1(< ~ey, sk($B) >) // and its own longterm secret key+ Y = 'g'^exp+ key = h2(< KA^exp, X^sk($B), X^exp, $A, $B >) + in+ [ Fr( ~ey ), In( X ) ]+ --[ Accept( ~ey, key )+ , Sid( ~ey, < $B, $A, Y, X, 'Resp' > )+ ]->+ [ Out( Y ),+ !Ephk(~ey, ~ey),+ !Sessk( ~ey, key) ]++/* Key Reveals for the eCK model */+rule Sessk_reveal: + [ !Sessk(~s, k) ] --[ RevealSessk(~s) ]-> [ Out(k) ]++rule Ltk_reveal:+ [ ] --[ RevealLtk($A) ]-> [ Out(sk($A)) ]++rule Ephk_reveal:+ [ !Ephk(~s, ~ek) ] --[ RevealEphk(~s) ]-> [ Out(~ek) ]+++/* Security properties */+/*+lemma eCK_same_key:+ " // If every agent registered at most one public key+ (All A #i #j. RegKey(A)@i & RegKey(A)@j ==> (#i = #j))+ ==> // then matching sessions accept the same key+ (not (Ex #i1 #i2 #i3 #i4 s ss k kk A B minfo .+ Accept(s, A, B, k ) @ i1+ & Accept(ss, B, A, kk) @ i2+ & Sid(s, minfo) @ i3+ & Match(ss, minfo) @i4+ & not( k = kk )+ ) )"+*/++lemma eCK_key_secrecy:+ /* + * The property specification is a (logically equivalent) simplified+ * version of the one in the original eCK (ProvSec) paper:+ *+ * If there exists a test session whose key k is known to the+ * Adversary with some session-id, then...+ */+ "(All #i1 #i2 #i3 test A B k sent recvd role.+ Accept(test, k) @ i1 & K( k ) @ i2 & Sid(test, < A, B, sent, recvd, role> ) @ i3+ ==> ( + /* ... the test session must be "not clean".+ * test is not clean if one of the following has happened:+ */+ /* 1. The adversary has revealed the session key of the test session. */+ (Ex #i3. RevealSessk( test ) @ i3 )+ + /* 2. The adversary has revealed both the longterm key of A and the+ ephemeral key of the test session */+ | (Ex #i5 #i6. RevealLtk ( A ) @ i5 & RevealEphk ( test ) @ i6 )++ /* 3. There is a matching session and */+ | (Ex matchingSession #i3 matchingRole.+ ( Sid ( matchingSession, < B, A, recvd, sent, matchingRole > ) @ i3 + & not ( matchingRole = role ) )+ & (+ /* (a) the adversary has revealed the session key of the matching session, or */+ (Ex #i5. RevealSessk( matchingSession ) @ i5 )++ /* (b) the adversary has revealed the longterm key of B and the ephemeral+ key of the matching session. */+ | (Ex #i5 #i6. RevealLtk ( B ) @ i5 & RevealEphk ( matchingSession ) @ i6 )+ )+ )+ /* 4. There is no matching session and */+ | ( ( not(Ex matchingSession #i3 matchingRole.+ ( Sid ( matchingSession, < B, A, recvd, sent, matchingRole > ) @ i3 + & not ( matchingRole = role ) )))++ /* the adversary has revealed the longterm key of B. */+ & ( (Ex #i5. RevealLtk (B) @ i5 )+ )+ )+ )+ )"++end
@@ -223,5 +223,17 @@ "not (Ex #i #j pid sid x otp1 otp2 . Login(pid,sid,x,otp1)@i & Login(pid,sid,x,otp2)@j & not(#i=#j))"++lemma injective_correspondance:+ "All pid sid x otp #t2 . Login(pid,sid,x,otp)@t2 ==>+ ( Ex #t1 . YubiPress(pid,x)@#t1 & #t1<#t2 + & All otp2 #t3 . Login(pid,sid,x,otp2)@t3 ==> #t3=#t2+ )"++lemma Login_invalidates_smaller_counters:+ "All pid otc1 tc1 otc2 tc2 #t1 #t2 #t3 .+ LoginCounter(pid,otc1,tc1)@#t1 & LoginCounter(pid,otc2,tc2)@#t2+ & IsSmaller(tc1,tc2)@t3+ ==> #t1<#t2 " end
@@ -203,7 +203,9 @@ [In(<pid,nonce,senc(<sid,tc,~pr>,k2)>) , !HSM(kh,k), !S_AEAD(pid,aead), S_Counter(pid,otc), !S_sid(pid,sid), !Smaller(otc,tc) ]- --[ Login(pid,sid,tc,senc(<sid,tc,~pr>,k2)) ]->+ --[ Login(pid,sid,tc,senc(<sid,tc,~pr>,k2)),+LoginCounter(pid,otc,tc)+ ]-> [ S_Counter(pid,tc) ] /* The following three axioms are conditions on the traces that make sure@@ -260,18 +262,51 @@ (Ex #t3 #t4 k . K(k)@t3 & MasterKey(k)@t4 & #t3<#t2)" /* Neither of those kinds of keys are ever learned by the adversary */-lemma neither_k_nor_k2_are_ever_leaked_inv[use_induction,reuse]:- "-not( Ex #t1 #t2 k . MasterKey(k)@t1 & K(k)@t2 )-& not (Ex #t5 #t6 k6 pid . Init(pid,k6)@t5 & K(k6)@t6 )+lemma neither_k_nor_k2_are_ever_leaked_inv[use_induction,reuse]: + " +not( Ex #t1 #t2 k . MasterKey(k)@t1 & KU(k)@t2 )+& not (Ex #t5 #t6 k6 pid . Init(pid,k6)@t5 & KU(k6)@t6 ) " // Each succesful login with counter value x was preceeded by a PressButton // event with the same counter value // This lemma cannot be proven at the moment, but it would be a first step // to reach the no_replay result present in Yubikey.spthy-//lemma one_count_foreach_login[reuse,use_induction]:-// "All pid sid x otp #t2 . Login(pid,sid,x,otp)@t2 ==>-// ( Ex #t1 . YubiPress(pid,x)@#t1 & #t1<#t2 )"+lemma one_count_foreach_login[reuse,use_induction]:+ "All pid sid x otp #t2 . Login(pid,sid,x,otp)@t2 ==>+ ( Ex #t1 . YubiPress(pid,x)@#t1 & #t1<#t2 )"+induction+ case empty_trace+ by contradiction // from formulas+next+ case non_empty_trace+ simplify+ solve( !S_AEAD( pid,+ <xorc(senc(keystream(kh, pid), k), <k2, sid>), mac(<k2, sid>, k)>+ ) ▶₂ #t2 )+ case BuyANewYubikey_case_1+ by sorry+ next+ case BuyANewYubikey_case_2+ by sorry+ next+ case write_AEAD+ solve( !KU( xorc(senc(keystream(kh, pid), k), <k2, sid>)+ ) @ #vk.6 )+ case irecv+ by contradiction // cyclic+ next+ case cxorc+ by sorry+ next+ case read_AEAD_case_1+ by sorry+ next+ case read_AEAD_case_2+ by sorry+ qed+ qed+qed+ end
+ data/examples/thesis-benedikt/running-examples/DH_Message_Deduction.spthy view
@@ -0,0 +1,38 @@+theory DH_Message_Deduction+begin+++section{* P_Msg *}++/*+ * Protocol: P_Msg+ * Modeler: Benedikt Schmidt+ * Date: October 2012+ * Source: "Ph.D. Thesis: Formal Analysis of+ * Key Exchange Protocols and Physical+ * Protocols"+ *+ * Status: Working+ */++/* This is an example protocols that is used in the+ the thesis to demonstrate various concepts */++builtins: diffie-hellman++rule Start:+ [ Fr(~x), Fr(~y) ]+ --[ Start() ]->+ [ S(~x), Out(<('g'^~x)^~y,inv(~y)>)]++rule Fin:+ [ S(~x), In(('g'^~x)) ] --[ Fin() ]-> [ ]++lemma key_deducible:+ exists-trace+ "Ex #i #j.+ Start() @ i & Fin() @ j+ & (All #k. Start() @ k ==> #k = #i)+ & (All #k. Fin() @ k ==> #k = #j)"++end
+ data/examples/thesis-benedikt/running-examples/UM_one_pass_eCK_like.spthy view
@@ -0,0 +1,93 @@+theory UM_one_pass_eCK_like+begin++/*+ * Protocol: UM one-pass protocol+ * See+ * "Combined Security Analysis of the One- and Three-Pass Unified Model Key Agreement Protocols"+ * Sanjit Chatterjee, Alfred Menezes, and Berkant Ustaoglu+ * Note that we use a different adversary model.+ *+ * Modeler: Benedikt Schmidt+ * Date: October 2012+ * Source: "Ph.D. Thesis: Formal Analysis of+ * Key Exchange Protocols and Physical+ * Protocols"+ *+ * Status: Working+ * Comment: This is the P_UM example that is used as a running example for my thesis.+ */+++builtins: diffie-hellman, hashing++rule Generate_key:+ let pkA = 'g'^~ea+ in+ [ Fr( ~ea ) ] + --[ ]-> + [ !Ltk( $A, ~ea ), !Pk( $A, pkA ), Out( pkA ) ]++rule Initiator:+ let pB = 'g'^~eb+ X = 'g'^~ex+ sid = <$A, $B, X, 'I'>+ key = h(pB^~ex, pB^~ea, $A, $B, X)+ in+ [ Fr( ~ex ), !Ltk( $A, ~ea ), !Pk( $B, pB ) ]+ --[ Accept( sid, key ) ]->+ [ Out( X ), !Ephk( sid, ~ex ) ]++rule Responder:+ let pA = 'g'^~ea+ sid = <$B, $A, X, 'R'>+ key = h(X^~eb, pA^~eb, $A, $B, X)+ in+ [ In( X ), !Ltk( $B, ~eb ), !Pk( $A, pA ) ]+ --[ Accept( sid, key ) ]->+ []++rule Ephemeral_Reveal:+ [ !Ephk( sid, ~x ) ]+ --[ RevealEphk( sid ) ]->+ [ Out( ~x ) ]++rule Ltk_Reveal:+ [ !Ltk( $A, ~ea ) ]+ --[ RevealLtk( $A ) ]->+ [ Out( ~ea ) ]++/*++lemma UM_executable:+ exists-trace+ "Ex #i #j A B X key.+ // An initiator and session+ Accept( <A,B,X,'I'>, key ) @ i+ // and a matching responder session accept key+ & Accept( <B,A,X,'R'>, key ) @ j+ // and the the adversary did not perform any reveals.+ & (not (Ex #j C. RevealLtk( C ) @ j))+ & (not (Ex #j s. RevealEphk( s ) @ j))"+*/+++lemma UM_secure_responder:+ "All #i #j A B X key msid.+ // If the key of a responder session with matching session msid is known+ Accept( <B,A,X,'R'>, key ) @ i & K( key ) @ j & msid = <A,B,X,'I'>+ // the the session is not clean, i.e., one of the following happened:+ ==>+ // 1. B's longterm key was revealed+ (Ex #k. RevealLtk(B) @ k )++ | // 2. There is am ephemeral key reveal for a matching session and a+ // longterm key reveal for its actor */+ (Ex #k #l. RevealEphk(msid) @ k & RevealLtk(A) @ l)++ | // 3. There is no matching session and a long-term key reveal for the peer+ // of the responder session.+ ((not (Ex #k key_. Accept( msid, key_) @ k)) & (Ex #k. RevealLtk(A) @ k))"+++end
+ data/examples/thesis-benedikt/running-examples/UM_one_pass_private.spthy view
@@ -0,0 +1,70 @@+theory UM_one_pass_private+begin++/*+ * Protocol: UM one-pass protocol using a private channel, derived from UM_one_pass_eCK_like+ * See+ * "Combined Security Analysis of the One- and Three-Pass Unified Model Key Agreement Protocols"+ * Sanjit Chatterjee, Alfred Menezes, and Berkant Ustaoglu+ *+ * Modeler: Benedikt Schmidt+ * Date: October 2012+ * Source: "Ph.D. Thesis: Formal Analysis of+ * Key Exchange Protocols and Physical+ * Protocols"+ *+ * Status: Working+ * Comment: This is the P_UM' example that is used as a running example for my thesis.+ */+++builtins: diffie-hellman, hashing++rule Generate_key:+ let pkA = 'g'^~ea+ in+ [ Fr( ~ea ) ] + --[ ]-> + [ !Ltk( $A, ~ea ), !Pk( $A, pkA ), Out( pkA ) ]++rule Initiator:+ let pB = 'g'^~eb+ X = 'g'^~ex+ sid = <$A, $B, X, 'I'>+ key = h(pB^~ex, pB^~ea, $A, $B, X)+ in+ [ Fr( ~ex ), !Ltk( $A, ~ea ), !Pk( $B, pB ) ]+ --[ Accept( sid, key ) ]->+ [ PChan( X ), !Ephk( sid, ~ex ) ]++rule Responder:+ let pA = 'g'^~ea+ sid = <$B, $A, X, 'R'>+ key = h(X^~eb, pA^~eb, $A, $B, X)+ in+ [ PChan( X ), !Ltk( $B, ~eb ), !Pk( $A, pA ) ]+ --[ Accept( sid, key ) ]->+ []++rule Ephemeral_Reveal:+ [ !Ephk( sid, ~x ) ]+ --[ RevealEphk( sid ) ]->+ [ Out( ~x ) ]++rule Ltk_Reveal:+ [ !Ltk( $A, ~ea ) ]+ --[ RevealLtk( $A ) ]->+ [ Out( ~ea ) ]++lemma UM_executable:+ exists-trace+ "Ex #i #j A B X key.+ // An initiator and session+ Accept( <A,B,X,'I'>, key ) @ i+ // and a matching responder session accept key+ & Accept( <B,A,X,'R'>, key ) @ j+ // and the the adversary did not perform any reveals.+ & (not (Ex #j C. RevealLtk( C ) @ j))+ & (not (Ex #j s. RevealEphk( s ) @ j))"++end
+ data/intruder_variants_bp.spthy view
@@ -0,0 +1,407 @@+rule (modulo AC) cpmult:+ [ !KU( x ), !KU( x.1 ) ]+ --[ !KU( pmult(x.1, x) ) ]->+ [ !KU( pmult(x.1, x) ) ]++rule (modulo AC) cem:+ [ !KU( x ), !KU( x.1 ) ] --[ !KU( em(x, x.1) ) ]-> [ !KU( em(x, x.1) ) ]++rule (modulo AC) dpmult:+ [ !KD( pmult(x.2, x.3) ), !KU( x.1 ) ]+ -->+ [ !KD( pmult((x.1*x.2), x.3) ) ]++rule (modulo AC) dpmult:+ [ !KD( pmult(x.2, x.3) ), !KU( inv(x.2) ) ] --> [ !KD( x.3 ) ]++rule (modulo AC) dpmult:+ [ !KD( pmult(inv(x.2), x.3) ), !KU( x.2 ) ] --> [ !KD( x.3 ) ]++rule (modulo AC) dpmult:+ [ !KD( pmult(inv(x.3), x.4) ), !KU( inv(x.2) ) ]+ -->+ [ !KD( pmult(inv((x.2*x.3)), x.4) ) ]++rule (modulo AC) dpmult:+ [ !KD( pmult(x.2, x.3) ), !KU( inv((x.2*x.4)) ) ]+ -->+ [ !KD( pmult(inv(x.4), x.3) ) ]++rule (modulo AC) dpmult:+ [ !KD( pmult(x.2, x.3) ), !KU( (x.4*inv(x.2)) ) ]+ -->+ [ !KD( pmult(x.4, x.3) ) ]++rule (modulo AC) dpmult:+ [ !KD( pmult(inv(x.2), x.4) ), !KU( (x.2*x.3) ) ]+ -->+ [ !KD( pmult(x.3, x.4) ) ]++rule (modulo AC) dpmult:+ [ !KD( pmult(inv((x.2*x.3)), x.4) ), !KU( x.2 ) ]+ -->+ [ !KD( pmult(inv(x.3), x.4) ) ]++rule (modulo AC) dpmult:+ [ !KD( pmult((x.2*x.3), x.4) ), !KU( inv(x.2) ) ]+ -->+ [ !KD( pmult(x.3, x.4) ) ]++rule (modulo AC) dpmult:+ [ !KD( pmult((x.3*inv(x.2)), x.4) ), !KU( x.2 ) ]+ -->+ [ !KD( pmult(x.3, x.4) ) ]++rule (modulo AC) dpmult:+ [ !KD( pmult(inv(x.2), x.3) ), !KU( (x.4*inv(x.5)) ) ]+ -->+ [ !KD( pmult((x.4*inv((x.2*x.5))), x.3) ) ]++rule (modulo AC) dpmult:+ [ !KD( pmult((x.3*inv(x.4)), x.5) ), !KU( inv(x.2) ) ]+ -->+ [ !KD( pmult((x.3*inv((x.2*x.4))), x.5) ) ]++rule (modulo AC) dpmult:+ [ !KD( pmult(x.2, x.3) ), !KU( (x.4*inv((x.2*x.5))) ) ]+ -->+ [ !KD( pmult((x.4*inv(x.5)), x.3) ) ]++rule (modulo AC) dpmult:+ [ !KD( pmult(inv((x.2*x.4)), x.5) ), !KU( (x.2*x.3) ) ]+ -->+ [ !KD( pmult((x.3*inv(x.4)), x.5) ) ]++rule (modulo AC) dpmult:+ [ !KD( pmult((x.3*x.4), x.5) ), !KU( (x.2*inv(x.3)) ) ]+ -->+ [ !KD( pmult((x.2*x.4), x.5) ) ]++rule (modulo AC) dpmult:+ [ !KD( pmult((x.3*x.4), x.5) ), !KU( inv((x.2*x.3)) ) ]+ -->+ [ !KD( pmult((x.4*inv(x.2)), x.5) ) ]++rule (modulo AC) dpmult:+ [ !KD( pmult((x.4*inv(x.2)), x.5) ), !KU( (x.2*x.3) ) ]+ -->+ [ !KD( pmult((x.3*x.4), x.5) ) ]++rule (modulo AC) dpmult:+ [ !KD( pmult((x.3*inv((x.2*x.4))), x.5) ), !KU( x.2 ) ]+ -->+ [ !KD( pmult((x.3*inv(x.4)), x.5) ) ]++rule (modulo AC) dpmult:+ [ !KD( pmult((x.4*inv(x.5)), x.6) ), !KU( (x.2*inv(x.3)) ) ]+ -->+ [ !KD( pmult((x.2*x.4*inv((x.3*x.5))), x.6) ) ]++rule (modulo AC) dpmult:+ [ !KD( pmult((x.3*inv(x.2)), x.4) ), !KU( (x.2*inv(x.3)) ) ]+ -->+ [ !KD( x.4 ) ]++rule (modulo AC) dpmult:+ [ !KD( pmult(inv((x.2*x.4)), x.5) ), !KU( (x.2*inv(x.3)) ) ]+ -->+ [ !KD( pmult(inv((x.3*x.4)), x.5) ) ]++rule (modulo AC) dpmult:+ [ !KD( pmult((x.3*inv(x.4)), x.5) ), !KU( inv((x.2*x.3)) ) ]+ -->+ [ !KD( pmult(inv((x.2*x.4)), x.5) ) ]++rule (modulo AC) dpmult:+ [ !KD( pmult((x.2*x.3), x.4) ), !KU( (x.5*inv((x.2*x.6))) ) ]+ -->+ [ !KD( pmult((x.3*x.5*inv(x.6)), x.4) ) ]++rule (modulo AC) dpmult:+ [ !KD( pmult((x.4*inv((x.2*x.5))), x.6) ), !KU( (x.2*x.3) ) ]+ -->+ [ !KD( pmult((x.3*x.4*inv(x.5)), x.6) ) ]++rule (modulo AC) dpmult:+ [ !KD( pmult((x.3*x.4*inv(x.2)), x.5) ), !KU( (x.2*inv(x.3)) ) ]+ -->+ [ !KD( pmult(x.4, x.5) ) ]++rule (modulo AC) dpmult:+ [ !KD( pmult((x.4*inv(x.2)), x.5) ), !KU( (x.2*x.3*inv(x.4)) ) ]+ -->+ [ !KD( pmult(x.3, x.5) ) ]++rule (modulo AC) dpmult:+ [ !KD( pmult(inv((x.2*x.5)), x.6) ), !KU( (x.2*x.3*inv(x.4)) ) ]+ -->+ [ !KD( pmult((x.3*inv((x.4*x.5))), x.6) ) ]++rule (modulo AC) dpmult:+ [ !KD( pmult((x.3*x.4*inv(x.5)), x.6) ), !KU( inv((x.2*x.3)) ) ]+ -->+ [ !KD( pmult((x.4*inv((x.2*x.5))), x.6) ) ]++rule (modulo AC) dpmult:+ [ !KD( pmult((x.3*inv((x.2*x.4))), x.5) ), !KU( (x.2*inv(x.3)) ) ]+ -->+ [ !KD( pmult(inv(x.4), x.5) ) ]++rule (modulo AC) dpmult:+ [ !KD( pmult((x.2*inv(x.3)), x.4) ), !KU( (x.3*inv((x.2*x.5))) ) ]+ -->+ [ !KD( pmult(inv(x.5), x.4) ) ]++rule (modulo AC) dpmult:+ [ !KD( pmult((x.4*x.5*inv(x.2)), x.6) ), !KU( (x.2*x.3*inv(x.4)) ) ]+ -->+ [ !KD( pmult((x.3*x.5), x.6) ) ]++rule (modulo AC) dpmult:+ [ !KD( pmult((x.2*inv(x.3)), x.4) ), !KU( (x.5*inv((x.2*x.6))) ) ]+ -->+ [ !KD( pmult((x.5*inv((x.3*x.6))), x.4) ) ]++rule (modulo AC) dpmult:+ [ !KD( pmult((x.4*inv((x.2*x.5))), x.6) ), !KU( (x.2*inv(x.3)) ) ]+ -->+ [ !KD( pmult((x.4*inv((x.3*x.5))), x.6) ) ]++rule (modulo AC) dpmult:+ [ !KD( pmult((x.4*inv((x.2*x.5))), x.6) ), !KU( (x.2*x.3*inv(x.4)) ) ]+ -->+ [ !KD( pmult((x.3*inv(x.5)), x.6) ) ]++rule (modulo AC) dpmult:+ [ !KD( pmult((x.4*x.5*inv(x.2)), x.6) ), !KU( (x.2*inv((x.3*x.4))) ) ]+ -->+ [ !KD( pmult((x.5*inv(x.3)), x.6) ) ]++rule (modulo AC) dpmult:+ [ !KD( pmult((x.2*inv(x.3)), x.4) ), !KU( (x.3*x.5*inv((x.2*x.6))) ) ]+ -->+ [ !KD( pmult((x.5*inv(x.6)), x.4) ) ]++rule (modulo AC) dpmult:+ [ !KD( pmult((x.3*x.4*inv((x.2*x.5))), x.6) ), !KU( (x.2*inv(x.3)) ) ]+ -->+ [ !KD( pmult((x.4*inv(x.5)), x.6) ) ]++rule (modulo AC) dpmult:+ [ !KD( pmult((x.5*inv((x.2*x.6))), x.7) ), !KU( (x.2*x.3*inv(x.4)) ) ]+ -->+ [ !KD( pmult((x.3*x.5*inv((x.4*x.6))), x.7) ) ]++rule (modulo AC) dpmult:+ [ !KD( pmult((x.4*x.5*inv(x.6)), x.7) ), !KU( (x.2*inv((x.3*x.4))) ) ]+ -->+ [ !KD( pmult((x.2*x.5*inv((x.3*x.6))), x.7) ) ]++rule (modulo AC) dpmult:+ [ !KD( pmult((x.4*inv((x.2*x.5))), x.6) ), !KU( (x.2*inv((x.3*x.4))) ) ]+ -->+ [ !KD( pmult(inv((x.3*x.5)), x.6) ) ]++rule (modulo AC) dpmult:+ [ !KD( pmult((x.4*x.5*inv((x.2*x.6))), x.7) ), !KU( (x.2*x.3*inv(x.4)) )+ ]+ -->+ [ !KD( pmult((x.3*x.5*inv(x.6)), x.7) ) ]++rule (modulo AC) dpmult:+ [ !KD( pmult((x.2*x.3*inv(x.4)), x.5) ), !KU( (x.4*x.6*inv((x.2*x.7))) )+ ]+ -->+ [ !KD( pmult((x.3*x.6*inv(x.7)), x.5) ) ]++rule (modulo AC) dpmult:+ [+ !KD( pmult((x.5*inv((x.2*x.6))), x.7) ), !KU( (x.2*x.3*inv((x.4*x.5))) )+ ]+ -->+ [ !KD( pmult((x.3*inv((x.4*x.6))), x.7) ) ]++rule (modulo AC) dpmult:+ [+ !KD( pmult((x.4*x.5*inv((x.2*x.6))), x.7) ), !KU( (x.2*inv((x.3*x.4))) )+ ]+ -->+ [ !KD( pmult((x.5*inv((x.3*x.6))), x.7) ) ]++rule (modulo AC) dpmult:+ [+ !KD( pmult((x.5*x.6*inv((x.2*x.7))), x.8) ),+ !KU( (x.2*x.3*inv((x.4*x.5))) )+ ]+ -->+ [ !KD( pmult((x.3*x.6*inv((x.4*x.7))), x.8) ) ]++rule (modulo AC) dem:+ [ !KD( pmult(x.2, x.3) ), !KU( x.1 ) ] --> [ !KD( em(x.1, x.3)^x.2 ) ]++rule (modulo AC) dem:+ [ !KU( x ), !KD( pmult(x.2, x.3) ) ] --> [ !KD( em(x, x.3)^x.2 ) ]++rule (modulo AC) dem:+ [ !KD( pmult(x.2, x.3) ), !KD( pmult(x.4, x.5) ) ]+ -->+ [ !KD( em(x.3, x.5)^(x.2*x.4) ) ]++rule (modulo AC) dem:+ [ !KD( pmult(x.2, x.3) ), !KD( pmult(inv(x.2), x.4) ) ]+ -->+ [ !KD( em(x.3, x.4) ) ]++rule (modulo AC) dem:+ [ !KD( pmult(inv(x.2), x.3) ), !KD( pmult(inv(x.4), x.5) ) ]+ -->+ [ !KD( em(x.3, x.5)^inv((x.2*x.4)) ) ]++rule (modulo AC) dem:+ [ !KD( pmult(x.2, x.3) ), !KD( pmult(inv((x.2*x.4)), x.5) ) ]+ -->+ [ !KD( em(x.3, x.5)^inv(x.4) ) ]++rule (modulo AC) dem:+ [ !KD( pmult(x.2, x.3) ), !KD( pmult((x.4*inv(x.2)), x.5) ) ]+ -->+ [ !KD( em(x.3, x.5)^x.4 ) ]++rule (modulo AC) dem:+ [ !KD( pmult(inv(x.2), x.3) ), !KD( pmult((x.2*x.4), x.5) ) ]+ -->+ [ !KD( em(x.3, x.5)^x.4 ) ]++rule (modulo AC) dem:+ [ !KD( pmult(inv(x.2), x.3) ), !KD( pmult((x.4*inv(x.5)), x.6) ) ]+ -->+ [ !KD( em(x.3, x.6)^(x.4*inv((x.2*x.5))) ) ]++rule (modulo AC) dem:+ [ !KD( pmult(x.2, x.3) ), !KD( pmult((x.4*inv((x.2*x.5))), x.6) ) ]+ -->+ [ !KD( em(x.3, x.6)^(x.4*inv(x.5)) ) ]++rule (modulo AC) dem:+ [ !KD( pmult(inv((x.2*x.5)), x.6) ), !KD( pmult((x.2*x.3), x.4) ) ]+ -->+ [ !KD( em(x.4, x.6)^(x.3*inv(x.5)) ) ]++rule (modulo AC) dem:+ [ !KD( pmult((x.2*x.3), x.4) ), !KD( pmult((x.5*inv(x.2)), x.6) ) ]+ -->+ [ !KD( em(x.4, x.6)^(x.3*x.5) ) ]++rule (modulo AC) dem:+ [ !KD( pmult((x.2*inv(x.3)), x.4) ), !KD( pmult((x.5*inv(x.6)), x.7) ) ]+ -->+ [ !KD( em(x.4, x.7)^(x.2*x.5*inv((x.3*x.6))) ) ]++rule (modulo AC) dem:+ [ !KD( pmult((x.2*inv(x.3)), x.4) ), !KD( pmult((x.3*inv(x.2)), x.5) ) ]+ -->+ [ !KD( em(x.4, x.5) ) ]++rule (modulo AC) dem:+ [ !KD( pmult(inv((x.2*x.3)), x.4) ), !KD( pmult((x.3*inv(x.5)), x.6) ) ]+ -->+ [ !KD( em(x.4, x.6)^inv((x.2*x.5)) ) ]++rule (modulo AC) dem:+ [ !KD( pmult((x.2*x.3), x.4) ), !KD( pmult((x.5*inv((x.2*x.6))), x.7) ) ]+ -->+ [ !KD( em(x.4, x.7)^(x.3*x.5*inv(x.6)) ) ]++rule (modulo AC) dem:+ [+ !KD( pmult((x.3*x.5*inv(x.2)), x.6) ), !KD( pmult((x.2*inv(x.3)), x.4) )+ ]+ -->+ [ !KD( em(x.4, x.6)^x.5 ) ]++rule (modulo AC) dem:+ [+ !KD( pmult(inv((x.2*x.3)), x.4) ), !KD( pmult((x.3*x.5*inv(x.6)), x.7) )+ ]+ -->+ [ !KD( em(x.4, x.7)^(x.5*inv((x.2*x.6))) ) ]++rule (modulo AC) dem:+ [+ !KD( pmult((x.3*inv((x.2*x.5))), x.6) ),+ !KD( pmult((x.2*inv(x.3)), x.4) )+ ]+ -->+ [ !KD( em(x.4, x.6)^inv(x.5) ) ]++rule (modulo AC) dem:+ [+ !KD( pmult((x.2*x.3*inv(x.4)), x.5) ),+ !KD( pmult((x.4*x.6*inv(x.2)), x.7) )+ ]+ -->+ [ !KD( em(x.5, x.7)^(x.3*x.6) ) ]++rule (modulo AC) dem:+ [+ !KD( pmult((x.2*inv(x.3)), x.4) ),+ !KD( pmult((x.5*inv((x.2*x.6))), x.7) )+ ]+ -->+ [ !KD( em(x.4, x.7)^(x.5*inv((x.3*x.6))) ) ]++rule (modulo AC) dem:+ [+ !KD( pmult((x.4*inv((x.2*x.6))), x.7) ),+ !KD( pmult((x.2*x.3*inv(x.4)), x.5) )+ ]+ -->+ [ !KD( em(x.5, x.7)^(x.3*inv(x.6)) ) ]++rule (modulo AC) dem:+ [+ !KD( pmult((x.3*x.5*inv((x.2*x.6))), x.7) ),+ !KD( pmult((x.2*inv(x.3)), x.4) )+ ]+ -->+ [ !KD( em(x.4, x.7)^(x.5*inv(x.6)) ) ]++rule (modulo AC) dem:+ [+ !KD( pmult((x.2*x.3*inv(x.4)), x.5) ),+ !KD( pmult((x.6*inv((x.2*x.7))), x.8) )+ ]+ -->+ [ !KD( em(x.5, x.8)^(x.3*x.6*inv((x.4*x.7))) ) ]++rule (modulo AC) dem:+ [+ !KD( pmult((x.2*inv((x.3*x.4))), x.5) ),+ !KD( pmult((x.4*inv((x.2*x.6))), x.7) )+ ]+ -->+ [ !KD( em(x.5, x.7)^inv((x.3*x.6)) ) ]++rule (modulo AC) dem:+ [+ !KD( pmult((x.4*x.6*inv((x.2*x.7))), x.8) ),+ !KD( pmult((x.2*x.3*inv(x.4)), x.5) )+ ]+ -->+ [ !KD( em(x.5, x.8)^(x.3*x.6*inv(x.7)) ) ]++rule (modulo AC) dem:+ [+ !KD( pmult((x.2*inv((x.3*x.4))), x.5) ),+ !KD( pmult((x.4*x.6*inv((x.2*x.7))), x.8) )+ ]+ -->+ [ !KD( em(x.5, x.8)^(x.6*inv((x.3*x.7))) ) ]++rule (modulo AC) dem:+ [+ !KD( pmult((x.2*x.3*inv((x.4*x.5))), x.6) ),+ !KD( pmult((x.5*x.7*inv((x.2*x.8))), x.9) )+ ]+ -->+ [ !KD( em(x.6, x.9)^(x.3*x.7*inv((x.4*x.8))) ) ]
data/intruder_variants_dh.spthy view
@@ -19,27 +19,22 @@ [ !KD( x.3^inv((x.2*x.4)) ) ] rule (modulo AC) dexp:- [ !KD( x.3^inv((x.2*x.4)) ), !KU( x.2 ) ] --> [ !KD( x.3^inv(x.4) ) ]--rule (modulo AC) dexp:- [ !KD( x.3^(x.2*x.4) ), !KU( inv(x.2) ) ] --> [ !KD( x.3^x.4 ) ]+ [ !KD( x.2^x.3 ), !KU( inv((x.3*x.4)) ) ] --> [ !KD( x.2^inv(x.4) ) ] rule (modulo AC) dexp:- [ !KD( x.3^(x.4*inv(x.2)) ), !KU( x.2 ) ] --> [ !KD( x.3^x.4 ) ]+ [ !KD( x.2^x.3 ), !KU( (x.4*inv(x.3)) ) ] --> [ !KD( x.2^x.4 ) ] rule (modulo AC) dexp:- [ !KD( x.2^x.3 ), !KU( inv((x.3*x.4)) ) ] --> [ !KD( x.2^inv(x.4) ) ]+ [ !KD( x.4^inv(x.2) ), !KU( (x.2*x.3) ) ] --> [ !KD( x.4^x.3 ) ] rule (modulo AC) dexp:- [ !KD( x.2^x.3 ), !KU( (x.4*inv(x.3)) ) ] --> [ !KD( x.2^x.4 ) ]+ [ !KD( x.3^inv((x.2*x.4)) ), !KU( x.2 ) ] --> [ !KD( x.3^inv(x.4) ) ] rule (modulo AC) dexp:- [ !KD( x.4^inv(x.3) ), !KU( (x.2*x.3) ) ] --> [ !KD( x.4^x.2 ) ]+ [ !KD( x.3^(x.2*x.4) ), !KU( inv(x.2) ) ] --> [ !KD( x.3^x.4 ) ] rule (modulo AC) dexp:- [ !KD( x.3^(x.4*inv(x.5)) ), !KU( inv(x.2) ) ]- -->- [ !KD( x.3^(x.4*inv((x.2*x.5))) ) ]+ [ !KD( x.3^(x.4*inv(x.2)) ), !KU( x.2 ) ] --> [ !KD( x.3^x.4 ) ] rule (modulo AC) dexp: [ !KD( x.2^inv(x.3) ), !KU( (x.4*inv(x.5)) ) ]@@ -47,19 +42,19 @@ [ !KD( x.2^(x.4*inv((x.3*x.5))) ) ] rule (modulo AC) dexp:- [ !KD( x.3^(x.4*inv((x.2*x.5))) ), !KU( x.2 ) ]+ [ !KD( x.3^(x.4*inv(x.5)) ), !KU( inv(x.2) ) ] -->- [ !KD( x.3^(x.4*inv(x.5)) ) ]+ [ !KD( x.3^(x.4*inv((x.2*x.5))) ) ] rule (modulo AC) dexp:- [ !KD( x.4^inv((x.3*x.5)) ), !KU( (x.2*x.3) ) ]+ [ !KD( x.2^x.3 ), !KU( (x.4*inv((x.3*x.5))) ) ] -->- [ !KD( x.4^(x.2*inv(x.5)) ) ]+ [ !KD( x.2^(x.4*inv(x.5)) ) ] rule (modulo AC) dexp:- [ !KD( x.4^(x.3*x.5) ), !KU( inv((x.2*x.3)) ) ]+ [ !KD( x.4^inv((x.2*x.5)) ), !KU( (x.2*x.3) ) ] -->- [ !KD( x.4^(x.5*inv(x.2)) ) ]+ [ !KD( x.4^(x.3*inv(x.5)) ) ] rule (modulo AC) dexp: [ !KD( x.4^(x.3*x.5) ), !KU( (x.2*inv(x.3)) ) ]@@ -67,16 +62,21 @@ [ !KD( x.4^(x.2*x.5) ) ] rule (modulo AC) dexp:- [ !KD( x.4^(x.5*inv(x.3)) ), !KU( (x.2*x.3) ) ]+ [ !KD( x.4^(x.3*x.5) ), !KU( inv((x.2*x.3)) ) ] -->- [ !KD( x.4^(x.2*x.5) ) ]+ [ !KD( x.4^(x.5*inv(x.2)) ) ] rule (modulo AC) dexp:- [ !KD( x.2^x.3 ), !KU( (x.4*inv((x.3*x.5))) ) ]+ [ !KD( x.4^(x.5*inv(x.2)) ), !KU( (x.2*x.3) ) ] -->- [ !KD( x.2^(x.4*inv(x.5)) ) ]+ [ !KD( x.4^(x.3*x.5) ) ] rule (modulo AC) dexp:+ [ !KD( x.3^(x.4*inv((x.2*x.5))) ), !KU( x.2 ) ]+ -->+ [ !KD( x.3^(x.4*inv(x.5)) ) ]++rule (modulo AC) dexp: [ !KD( x.4^(x.5*inv(x.6)) ), !KU( (x.2*inv(x.3)) ) ] --> [ !KD( x.4^(x.2*x.5*inv((x.3*x.6))) ) ]@@ -85,24 +85,24 @@ [ !KD( x.4^(x.3*inv(x.2)) ), !KU( (x.2*inv(x.3)) ) ] --> [ !KD( x.4 ) ] rule (modulo AC) dexp:- [ !KD( x.4^(x.3*inv(x.5)) ), !KU( inv((x.2*x.3)) ) ]+ [ !KD( x.4^inv((x.2*x.5)) ), !KU( (x.2*inv(x.3)) ) ] -->- [ !KD( x.4^inv((x.2*x.5)) ) ]+ [ !KD( x.4^inv((x.3*x.5)) ) ] rule (modulo AC) dexp:- [ !KD( x.4^inv((x.2*x.5)) ), !KU( (x.2*inv(x.3)) ) ]+ [ !KD( x.4^(x.3*inv(x.5)) ), !KU( inv((x.2*x.3)) ) ] -->- [ !KD( x.4^inv((x.3*x.5)) ) ]+ [ !KD( x.4^inv((x.2*x.5)) ) ] rule (modulo AC) dexp:- [ !KD( x.4^(x.5*inv((x.3*x.6))) ), !KU( (x.2*x.3) ) ]+ [ !KD( x.2^(x.3*x.4) ), !KU( (x.5*inv((x.3*x.6))) ) ] -->- [ !KD( x.4^(x.2*x.5*inv(x.6)) ) ]+ [ !KD( x.2^(x.4*x.5*inv(x.6)) ) ] rule (modulo AC) dexp:- [ !KD( x.2^(x.3*x.4) ), !KU( (x.5*inv((x.4*x.6))) ) ]+ [ !KD( x.4^(x.5*inv((x.2*x.6))) ), !KU( (x.2*x.3) ) ] -->- [ !KD( x.2^(x.3*x.5*inv(x.6)) ) ]+ [ !KD( x.4^(x.3*x.5*inv(x.6)) ) ] rule (modulo AC) dexp: [ !KD( x.4^(x.3*x.5*inv(x.2)) ), !KU( (x.2*inv(x.3)) ) ]@@ -110,19 +110,19 @@ [ !KD( x.4^x.5 ) ] rule (modulo AC) dexp:- [ !KD( x.5^(x.4*inv(x.3)) ), !KU( (x.2*x.3*inv(x.4)) ) ]+ [ !KD( x.5^(x.4*inv(x.2)) ), !KU( (x.2*x.3*inv(x.4)) ) ] -->- [ !KD( x.5^x.2 ) ]+ [ !KD( x.5^x.3 ) ] rule (modulo AC) dexp:- [ !KD( x.4^(x.3*x.5*inv(x.6)) ), !KU( inv((x.2*x.3)) ) ]+ [ !KD( x.5^inv((x.2*x.6)) ), !KU( (x.2*x.3*inv(x.4)) ) ] -->- [ !KD( x.4^(x.5*inv((x.2*x.6))) ) ]+ [ !KD( x.5^(x.3*inv((x.4*x.6))) ) ] rule (modulo AC) dexp:- [ !KD( x.5^inv((x.3*x.6)) ), !KU( (x.2*x.3*inv(x.4)) ) ]+ [ !KD( x.4^(x.3*x.5*inv(x.6)) ), !KU( inv((x.2*x.3)) ) ] -->- [ !KD( x.5^(x.2*inv((x.4*x.6))) ) ]+ [ !KD( x.4^(x.5*inv((x.2*x.6))) ) ] rule (modulo AC) dexp: [ !KD( x.4^(x.3*inv((x.2*x.5))) ), !KU( (x.2*inv(x.3)) ) ]@@ -135,14 +135,14 @@ [ !KD( x.2^inv(x.5) ) ] rule (modulo AC) dexp:- [ !KD( x.2^(x.3*inv(x.4)) ), !KU( (x.5*inv((x.3*x.6))) ) ]+ [ !KD( x.5^(x.4*x.6*inv(x.2)) ), !KU( (x.2*x.3*inv(x.4)) ) ] -->- [ !KD( x.2^(x.5*inv((x.4*x.6))) ) ]+ [ !KD( x.5^(x.3*x.6) ) ] rule (modulo AC) dexp:- [ !KD( x.5^(x.4*x.6*inv(x.3)) ), !KU( (x.2*x.3*inv(x.4)) ) ]+ [ !KD( x.2^(x.3*inv(x.4)) ), !KU( (x.5*inv((x.3*x.6))) ) ] -->- [ !KD( x.5^(x.2*x.6) ) ]+ [ !KD( x.2^(x.5*inv((x.4*x.6))) ) ] rule (modulo AC) dexp: [ !KD( x.4^(x.5*inv((x.2*x.6))) ), !KU( (x.2*inv(x.3)) ) ]@@ -150,34 +150,34 @@ [ !KD( x.4^(x.5*inv((x.3*x.6))) ) ] rule (modulo AC) dexp:- [ !KD( x.2^(x.3*inv(x.4)) ), !KU( (x.4*x.5*inv((x.3*x.6))) ) ]+ [ !KD( x.5^(x.4*inv((x.2*x.6))) ), !KU( (x.2*x.3*inv(x.4)) ) ] -->- [ !KD( x.2^(x.5*inv(x.6)) ) ]+ [ !KD( x.5^(x.3*inv(x.6)) ) ] rule (modulo AC) dexp:- [ !KD( x.4^(x.3*x.5*inv((x.2*x.6))) ), !KU( (x.2*inv(x.3)) ) ]+ [ !KD( x.5^(x.4*x.6*inv(x.2)) ), !KU( (x.2*inv((x.3*x.4))) ) ] -->- [ !KD( x.4^(x.5*inv(x.6)) ) ]+ [ !KD( x.5^(x.6*inv(x.3)) ) ] rule (modulo AC) dexp:- [ !KD( x.5^(x.4*inv((x.3*x.6))) ), !KU( (x.2*x.3*inv(x.4)) ) ]+ [ !KD( x.2^(x.3*inv(x.4)) ), !KU( (x.4*x.5*inv((x.3*x.6))) ) ] -->- [ !KD( x.5^(x.2*inv(x.6)) ) ]+ [ !KD( x.2^(x.5*inv(x.6)) ) ] rule (modulo AC) dexp:- [ !KD( x.5^(x.4*x.6*inv(x.2)) ), !KU( (x.2*inv((x.3*x.4))) ) ]+ [ !KD( x.4^(x.3*x.5*inv((x.2*x.6))) ), !KU( (x.2*inv(x.3)) ) ] -->- [ !KD( x.5^(x.6*inv(x.3)) ) ]+ [ !KD( x.4^(x.5*inv(x.6)) ) ] rule (modulo AC) dexp:- [ !KD( x.5^(x.4*x.6*inv(x.7)) ), !KU( (x.2*inv((x.3*x.4))) ) ]+ [ !KD( x.5^(x.6*inv((x.2*x.7))) ), !KU( (x.2*x.3*inv(x.4)) ) ] -->- [ !KD( x.5^(x.2*x.6*inv((x.3*x.7))) ) ]+ [ !KD( x.5^(x.3*x.6*inv((x.4*x.7))) ) ] rule (modulo AC) dexp:- [ !KD( x.5^(x.6*inv((x.3*x.7))) ), !KU( (x.2*x.3*inv(x.4)) ) ]+ [ !KD( x.5^(x.4*x.6*inv(x.7)) ), !KU( (x.2*inv((x.3*x.4))) ) ] -->- [ !KD( x.5^(x.2*x.6*inv((x.4*x.7))) ) ]+ [ !KD( x.5^(x.2*x.6*inv((x.3*x.7))) ) ] rule (modulo AC) dexp: [ !KD( x.5^(x.4*inv((x.2*x.6))) ), !KU( (x.2*inv((x.3*x.4))) ) ]@@ -185,19 +185,19 @@ [ !KD( x.5^inv((x.3*x.6)) ) ] rule (modulo AC) dexp:- [ !KD( x.2^(x.3*x.4*inv(x.5)) ), !KU( (x.5*x.6*inv((x.4*x.7))) ) ]+ [ !KD( x.5^(x.4*x.6*inv((x.2*x.7))) ), !KU( (x.2*x.3*inv(x.4)) ) ] -->- [ !KD( x.2^(x.3*x.6*inv(x.7)) ) ]+ [ !KD( x.5^(x.3*x.6*inv(x.7)) ) ] rule (modulo AC) dexp:- [ !KD( x.5^(x.4*x.6*inv((x.3*x.7))) ), !KU( (x.2*x.3*inv(x.4)) ) ]+ [ !KD( x.2^(x.3*x.4*inv(x.5)) ), !KU( (x.5*x.6*inv((x.3*x.7))) ) ] -->- [ !KD( x.5^(x.2*x.6*inv(x.7)) ) ]+ [ !KD( x.2^(x.4*x.6*inv(x.7)) ) ] rule (modulo AC) dexp:- [ !KD( x.6^(x.5*inv((x.3*x.7))) ), !KU( (x.2*x.3*inv((x.4*x.5))) ) ]+ [ !KD( x.6^(x.5*inv((x.2*x.7))) ), !KU( (x.2*x.3*inv((x.4*x.5))) ) ] -->- [ !KD( x.6^(x.2*inv((x.4*x.7))) ) ]+ [ !KD( x.6^(x.3*inv((x.4*x.7))) ) ] rule (modulo AC) dexp: [ !KD( x.5^(x.4*x.6*inv((x.2*x.7))) ), !KU( (x.2*inv((x.3*x.4))) ) ]@@ -205,9 +205,9 @@ [ !KD( x.5^(x.6*inv((x.3*x.7))) ) ] rule (modulo AC) dexp:- [ !KD( x.6^(x.5*x.7*inv((x.3*x.8))) ), !KU( (x.2*x.3*inv((x.4*x.5))) ) ]+ [ !KD( x.6^(x.5*x.7*inv((x.2*x.8))) ), !KU( (x.2*x.3*inv((x.4*x.5))) ) ] -->- [ !KD( x.6^(x.2*x.7*inv((x.4*x.8))) ) ]+ [ !KD( x.6^(x.3*x.7*inv((x.4*x.8))) ) ] rule (modulo AC) dinv: [ !KD( inv(x.1) ) ] --> [ !KD( x.1 ) ]
src/Main/Console.hs view
@@ -162,6 +162,7 @@ , modeNames = [name] , modeValue = [] , modeCheck = updateArg "mode" name+ , modeExpandAt = False , modeReform = const Nothing-- no reform possibility , modeHelp = help , modeHelpSuffix = []
src/Main/Mode/Intruder.hs view
@@ -11,18 +11,18 @@ intruderMode ) where -import Control.Basics import Control.Monad.Reader import System.Console.CmdArgs.Explicit as CmdArgs import System.FilePath import Theory+ import Theory.Tools.IntruderRules import Main.Console import Main.Environment-import Main.TheoryLoader (intruderVariantsFile)+import Main.TheoryLoader (dhIntruderVariantsFile,bpIntruderVariantsFile) import Main.Utils @@ -39,33 +39,28 @@ } outputFlags =- [ flagOpt "" ["output","o"] (updateArg "outFile") "FILE" "Output file"- , flagOpt "" ["Output","O"] (updateArg "outDir") "DIR" "Output directory"+ [ flagOpt "" ["Output","O"] (updateArg "outDir") "DIR" "Output directory" ] -- | Compute the intruder variants. run :: TamarinMode -> Arguments -> IO () run _thisMode as = do _ <- ensureMaude as- hnd <- startMaude (maudePath as) dhMaudeSig- let rules = dhIntruderRules `runReader` hnd- rulesString = renderDoc $ prettyIntruderVariants rules- putStrLn rulesString- writeRules rulesString+ dhHnd <- startMaude (maudePath as) dhMaudeSig+ bpHnd <- startMaude (maudePath as) bpMaudeSig+ let dhRules = dhIntruderRules `runReader` dhHnd+ bpRules = bpIntruderRules `runReader` bpHnd+ dhS = renderDoc . prettyIntruderVariants $ dhRules+ bpS = renderDoc . prettyIntruderVariants $ bpRules++ putStrLn (dhS++bpS)+ writeRules dhS bpS where -- output generation -------------------- - writeRules rulesString = case optOutPath of- Just outPath -> writeFileWithDirs outPath rulesString- Nothing -> return ()-- -- Output file name, if output is desired.- optOutPath :: Maybe FilePath- optOutPath =- do outFile <- findArg "outFile" as- guard (outFile /= "")- return outFile- <|>- do outDir <- findArg "outDir" as- return $ outDir </> intruderVariantsFile+ writeRules dhS bpS = case findArg "outDir" as of+ Just outDir ->+ do writeFileWithDirs (outDir </> dhIntruderVariantsFile) dhS+ writeFileWithDirs (outDir </> bpIntruderVariantsFile) bpS+ Nothing -> return ()
src/Main/TheoryLoader.hs view
@@ -24,8 +24,9 @@ , closeThy - -- ** Message deduction variants- , intruderVariantsFile+ -- ** Cached Message Deduction Rule Variants+ , dhIntruderVariantsFile+ , bpIntruderVariantsFile , addMessageDeductionRuleVariants ) where@@ -49,7 +50,8 @@ import Theory.Text.Parser import Theory.Text.Pretty import Theory.Tools.AbstractInterpretation (EvaluationStyle(..))-import Theory.Tools.IntruderRules (specialIntruderRules, subtermIntruderRules)+import Theory.Tools.IntruderRules (specialIntruderRules, subtermIntruderRules+ , multisetIntruderRules) import Theory.Tools.Wellformedness import Main.Console@@ -77,9 +79,6 @@ , flagOpt "s" ["heuristic"] (updateArg "heuristic") "(s|S|c|C)+" "Sequence of goal rankings to use (default 's')" - --, flagOpt "" ["intruder","i"] (updateArg "intruderVariants") "FILE"- -- "Cached intruder rules to use"- , flagOpt "summary" ["partial-evaluation"] (updateArg "partialEvaluation") "SUMMARY|VERBOSE" "Partially evaluate multiset rewriting system"@@ -221,11 +220,49 @@ Just other -> error $ "unknown stop-on-trace method: " ++ other + ------------------------------------------------------------------------------ -- Message deduction variants cached in files ------------------------------------------------------------------------------ -- | The name of the intruder variants file.+dhIntruderVariantsFile :: FilePath+dhIntruderVariantsFile = "intruder_variants_dh.spthy"++-- | The name of the intruder variants file.+bpIntruderVariantsFile :: FilePath+bpIntruderVariantsFile = "intruder_variants_bp.spthy"++-- | Add the variants of the message deduction rule. Uses the cached version+-- of the @"intruder_variants_dh.spthy"@ file for the variants of the message+-- deduction rules for Diffie-Hellman exponentiation.+addMessageDeductionRuleVariants :: OpenTheory -> IO OpenTheory+addMessageDeductionRuleVariants thy0+ | enableBP msig = addIntruderVariants [ dhIntruderVariantsFile+ , bpIntruderVariantsFile ]+ | enableDH msig = addIntruderVariants [ dhIntruderVariantsFile ]+ | otherwise = return thy+ where+ msig = get (sigpMaudeSig . thySignature) thy0+ rules = subtermIntruderRules msig ++ specialIntruderRules+ ++ if enableMSet msig then multisetIntruderRules else []+ thy = addIntrRuleACs rules thy0+ addIntruderVariants files = do+ ruless <- mapM loadRules files+ return $ addIntrRuleACs (concat ruless) thy+ where+ loadRules file = do+ variantsFile <- getDataFileName file+ ifM (doesFileExist variantsFile)+ (parseIntruderRules msig variantsFile)+ (error $ "could not find intruder message deduction theory '"+ ++ variantsFile ++ "'")+{-+------------------------------------------------------------------------------+-- Message deduction variants cached in files+------------------------------------------------------------------------------++-- | The name of the intruder variants file. intruderVariantsFile :: FilePath intruderVariantsFile = "intruder_variants_dh.spthy" @@ -247,3 +284,4 @@ msig = get (sigpMaudeSig . thySignature) thy0 rules = subtermIntruderRules msig ++ specialIntruderRules thy = addIntrRuleACs rules thy0+-}
tamarin-prover.cabal view
@@ -1,7 +1,7 @@ cabal-version: >= 1.8 build-type: Simple name: tamarin-prover-version: 0.8.2.1+version: 0.8.4.0 license: GPL license-file: LICENSE category: Theorem Provers@@ -48,8 +48,9 @@ AUTHORS CHANGES - -- cached intruder variants for DH-exponentiation+ -- cached intruder variants for DH and BP intruder_variants_dh.spthy+ intruder_variants_bp.spthy -- files for the web-frontend img/*.ico@@ -75,6 +76,40 @@ examples/classic/NSLPK3.spthy examples/classic/NSPK3.spthy + -- features+ examples/features/multiset/counter.spthy+ examples/features/private_function_symbols/NAXOS_eCK_PFS_private.spthy+ examples/features/private_function_symbols/NAXOS_eCK_private.spthy++ -- newer AKE examples+ examples/ake/dh/client_session_key.aes+ examples/ake/dh/DHKEA_NAXOS_C_eCK_PFS_keyreg_partially_matching.spthy+ examples/ake/dh/DHKEA_NAXOS_C_eCK_PFS_partially_matching.spthy+ examples/ake/dh/NAXOS_eCK.spthy+ examples/ake/dh/NAXOS_eCK_PFS.spthy+ examples/ake/dh/UM_one_pass_attack.spthy+ examples/ake/dh/UM_one_pass_fix.spthy+ examples/ake/dh/UM_three_pass.spthy+ examples/ake/dh/UM_three_pass_combined.spthy+ examples/ake/dh/UM_three_pass_combined_fixed.spthy+ examples/ake/bilinear/Chen_Kudla.spthy+ examples/ake/bilinear/Chen_Kudla_eCK.spthy+ examples/ake/bilinear/Joux.spthy+ examples/ake/bilinear/Joux_EphkRev.spthy+ examples/ake/bilinear/README+ examples/ake/bilinear/RYY.spthy+ examples/ake/bilinear/RYY_PFS.spthy+ examples/ake/bilinear/Scott.spthy+ examples/ake/bilinear/Scott_EphkRev.spthy+ examples/ake/bilinear/TAK1.spthy+ examples/ake/bilinear/TAK1_eCK_like.spthy++ -- running examples from papers/documentation+ examples/cav13/DH_example.spthy+ examples/thesis-benedikt/running-examples/DH_Message_Deduction.spthy+ examples/thesis-benedikt/running-examples/UM_one_pass_eCK_like.spthy+ examples/thesis-benedikt/running-examples/UM_one_pass_private.spthy+ -- loops examples/loops/Minimal_Crypto_API.spthy examples/loops/Minimal_KeyRenegotiation.spthy@@ -177,7 +212,7 @@ -- Parallelize by default. Only activated for GHC 7.4, as this flag was -- unstable in earlier -- versions; i.e., it resulted in command-line -- parsing errors.- if impl(ghc >= 7.4)+ if impl(ghc >= 7.4) && flag(threaded) ghc-options: -with-rtsopts=-N hs-source-dirs: src@@ -218,7 +253,7 @@ , containers >= 0.4.2 && < 0.5 , dlist == 0.5.* , mtl == 2.0.*- , cmdargs == 0.9.*+ , cmdargs == 0.10.* , filepath >= 1.1 && < 1.4 , directory >= 1.0 && < 1.2 , process == 1.1.*@@ -234,9 +269,9 @@ , parallel == 3.2.* , HUnit == 1.2.* - , tamarin-prover-utils >= 0.8.2 && < 0.9- , tamarin-prover-term >= 0.8.2 && < 0.9- , tamarin-prover-theory >= 0.8.2 && < 0.9+ , tamarin-prover-utils >= 0.8.4 && < 0.9+ , tamarin-prover-term >= 0.8.4 && < 0.9+ , tamarin-prover-theory >= 0.8.4 && < 0.9 other-modules: