diff --git a/data/CHANGES b/data/CHANGES --- a/data/CHANGES +++ b/data/CHANGES @@ -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. diff --git a/data/examples/ake/bilinear/Chen_Kudla.spthy b/data/examples/ake/bilinear/Chen_Kudla.spthy new file mode 100644 --- /dev/null +++ b/data/examples/ake/bilinear/Chen_Kudla.spthy @@ -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 diff --git a/data/examples/ake/bilinear/Chen_Kudla_eCK.spthy b/data/examples/ake/bilinear/Chen_Kudla_eCK.spthy new file mode 100644 --- /dev/null +++ b/data/examples/ake/bilinear/Chen_Kudla_eCK.spthy @@ -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 diff --git a/data/examples/ake/bilinear/Joux.spthy b/data/examples/ake/bilinear/Joux.spthy new file mode 100644 --- /dev/null +++ b/data/examples/ake/bilinear/Joux.spthy @@ -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( ) + ] + +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 diff --git a/data/examples/ake/bilinear/Joux_EphkRev.spthy b/data/examples/ake/bilinear/Joux_EphkRev.spthy new file mode 100644 --- /dev/null +++ b/data/examples/ake/bilinear/Joux_EphkRev.spthy @@ -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( ) + , !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 diff --git a/data/examples/ake/bilinear/README b/data/examples/ake/bilinear/README new file mode 100644 --- /dev/null +++ b/data/examples/ake/bilinear/README @@ -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. diff --git a/data/examples/ake/bilinear/RYY.spthy b/data/examples/ake/bilinear/RYY.spthy new file mode 100644 --- /dev/null +++ b/data/examples/ake/bilinear/RYY.spthy @@ -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, ) @ i + & Accept(t2, k) @ j + & Sid(t2, ) @ 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, ) @ 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, ) @ 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, ) @ 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 diff --git a/data/examples/ake/bilinear/RYY_PFS.spthy b/data/examples/ake/bilinear/RYY_PFS.spthy new file mode 100644 --- /dev/null +++ b/data/examples/ake/bilinear/RYY_PFS.spthy @@ -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, ) @ i + & Accept(t2, k) @ j + & Sid(t2, ) @ 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, ) @ 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, ) @ 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, ) @ 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 diff --git a/data/examples/ake/bilinear/Scott.spthy b/data/examples/ake/bilinear/Scott.spthy new file mode 100644 --- /dev/null +++ b/data/examples/ake/bilinear/Scott.spthy @@ -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 diff --git a/data/examples/ake/bilinear/Scott_EphkRev.spthy b/data/examples/ake/bilinear/Scott_EphkRev.spthy new file mode 100644 --- /dev/null +++ b/data/examples/ake/bilinear/Scott_EphkRev.spthy @@ -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 diff --git a/data/examples/ake/bilinear/TAK1.spthy b/data/examples/ake/bilinear/TAK1.spthy new file mode 100644 --- /dev/null +++ b/data/examples/ake/bilinear/TAK1.spthy @@ -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, ) + , Sid( ~ex, ) ]-> + // 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 diff --git a/data/examples/ake/bilinear/TAK1_eCK_like.spthy b/data/examples/ake/bilinear/TAK1_eCK_like.spthy new file mode 100644 --- /dev/null +++ b/data/examples/ake/bilinear/TAK1_eCK_like.spthy @@ -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, ) + , Sid( ~ex, ) ]-> + // 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 diff --git a/data/examples/ake/dh/DHKEA_NAXOS_C_eCK_PFS_keyreg_partially_matching.spthy b/data/examples/ake/dh/DHKEA_NAXOS_C_eCK_PFS_keyreg_partially_matching.spthy new file mode 100644 --- /dev/null +++ b/data/examples/ake/dh/DHKEA_NAXOS_C_eCK_PFS_keyreg_partially_matching.spthy @@ -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, ) @ i1 + & Sid( s2, ) @ 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 diff --git a/data/examples/ake/dh/DHKEA_NAXOS_C_eCK_PFS_partially_matching.spthy b/data/examples/ake/dh/DHKEA_NAXOS_C_eCK_PFS_partially_matching.spthy new file mode 100644 --- /dev/null +++ b/data/examples/ake/dh/DHKEA_NAXOS_C_eCK_PFS_partially_matching.spthy @@ -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, ) @ i1 + & Sid( s2, ) @ 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 diff --git a/data/examples/ake/dh/NAXOS_eCK.spthy b/data/examples/ake/dh/NAXOS_eCK.spthy new file mode 100644 --- /dev/null +++ b/data/examples/ake/dh/NAXOS_eCK.spthy @@ -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 diff --git a/data/examples/ake/dh/NAXOS_eCK_PFS.spthy b/data/examples/ake/dh/NAXOS_eCK_PFS.spthy new file mode 100644 --- /dev/null +++ b/data/examples/ake/dh/NAXOS_eCK_PFS.spthy @@ -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 diff --git a/data/examples/ake/dh/UM_one_pass_attack.spthy b/data/examples/ake/dh/UM_one_pass_attack.spthy new file mode 100644 --- /dev/null +++ b/data/examples/ake/dh/UM_one_pass_attack.spthy @@ -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 can match another + responder session 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( , role, k ) @ i & K( k ) @ j & s = & sp = + /* 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 diff --git a/data/examples/ake/dh/UM_one_pass_fix.spthy b/data/examples/ake/dh/UM_one_pass_fix.spthy new file mode 100644 --- /dev/null +++ b/data/examples/ake/dh/UM_one_pass_fix.spthy @@ -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 can match another + responder session 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( , role, k ) @ i & K( k ) @ j & s = & sp = + /* 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 diff --git a/data/examples/ake/dh/UM_three_pass.spthy b/data/examples/ake/dh/UM_three_pass.spthy new file mode 100644 --- /dev/null +++ b/data/examples/ake/dh/UM_three_pass.spthy @@ -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', > + <'3', conf> > // new sid + in + [ I_Act( ~ex, $A, $B ) // this session was activated + , In( ) + , !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',> > // sid is unique + + + in + [ Fr( ~ey ) + , In( X ) + , !Ltk( $B, ~eb ) + , !Pk( $A, pA ) ] + --[ Activate(sid) + , Sid( sid ) + , Agents($A,$B) ]-> + [ Out( ) + , 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', >> // sid is unique + sid = <'UM3', $B, $A, <'1',X> + <'2', > + <'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 diff --git a/data/examples/ake/dh/UM_three_pass_combined.spthy b/data/examples/ake/dh/UM_three_pass_combined.spthy new file mode 100644 --- /dev/null +++ b/data/examples/ake/dh/UM_three_pass_combined.spthy @@ -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', > + <'3', conf> > // new sid + in + [ I_Act( ~ex, $A, $B ) // this session was activated + , In( ) + , !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',> > // sid is unique + + + in + [ Fr( ~ey ) + , In( X ) + , !Ltk( $B, ~eb ) + , !Pk( $A, pA ) ] + --[ Activate(sid) + , Sid( sid ) + , Agents($A,$B) ]-> + [ Out( ) + , 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', >> // sid is unique + sid = <'UM3', $B, $A, <'1',X> + <'2', > + <'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 diff --git a/data/examples/ake/dh/UM_three_pass_combined_fixed.spthy b/data/examples/ake/dh/UM_three_pass_combined_fixed.spthy new file mode 100644 --- /dev/null +++ b/data/examples/ake/dh/UM_three_pass_combined_fixed.spthy @@ -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', > + <'3', conf> > // new sid + in + [ I_Act( ~ex, $A, $B ) // this session was activated + , In( ) + , !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',> > // sid is unique + + + in + [ Fr( ~ey ) + , In( X ) + , !Ltk( $B, ~eb ) + , !Pk( $A, pA ) ] + --[ Activate(sid) + , Sid( sid ) + , Agents($A,$B) ]-> + [ Out( ) + , 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', >> // sid is unique + sid = <'UM3', $B, $A, <'1',X> + <'2', > + <'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( , role, k ) @ i & K( k ) @ j & s = & sp = + /* 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 diff --git a/data/examples/ake/dh/client_session_key.aes b/data/examples/ake/dh/client_session_key.aes new file mode 100644 --- /dev/null +++ b/data/examples/ake/dh/client_session_key.aes @@ -0,0 +1,1 @@ +ÔZÀ[d'•ám]ÌNÞ܄ælΖDù›ª-vóÃ]§ödTòDÿM}zSÒÕÈS>u¯Ž·‘ëðU?…kdm”rõ⚆•šg@cV42üú†jâ3kÉõ]PS diff --git a/data/examples/cav13/DH_example.spthy b/data/examples/cav13/DH_example.spthy new file mode 100644 --- /dev/null +++ b/data/examples/cav13/DH_example.spthy @@ -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()>) + , Step1(tid:fresh, A:pub, B:pub, x:fresh) ] + +rule Step2: + [ Step1(tid, A, B, x:fresh), In()>) ] + --[ 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 diff --git a/data/examples/features/multiset/counter.spthy b/data/examples/features/multiset/counter.spthy new file mode 100644 --- /dev/null +++ b/data/examples/features/multiset/counter.spthy @@ -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 + diff --git a/data/examples/features/private_function_symbols/NAXOS_eCK_PFS_private.spthy b/data/examples/features/private_function_symbols/NAXOS_eCK_PFS_private.spthy new file mode 100644 --- /dev/null +++ b/data/examples/features/private_function_symbols/NAXOS_eCK_PFS_private.spthy @@ -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 diff --git a/data/examples/features/private_function_symbols/NAXOS_eCK_private.spthy b/data/examples/features/private_function_symbols/NAXOS_eCK_private.spthy new file mode 100644 --- /dev/null +++ b/data/examples/features/private_function_symbols/NAXOS_eCK_private.spthy @@ -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 diff --git a/data/examples/related_work/YubiSecure_KS_STM12/Yubikey.spthy b/data/examples/related_work/YubiSecure_KS_STM12/Yubikey.spthy --- a/data/examples/related_work/YubiSecure_KS_STM12/Yubikey.spthy +++ b/data/examples/related_work/YubiSecure_KS_STM12/Yubikey.spthy @@ -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 diff --git a/data/examples/related_work/YubiSecure_KS_STM12/Yubikey_and_YubiHSM.spthy b/data/examples/related_work/YubiSecure_KS_STM12/Yubikey_and_YubiHSM.spthy --- a/data/examples/related_work/YubiSecure_KS_STM12/Yubikey_and_YubiHSM.spthy +++ b/data/examples/related_work/YubiSecure_KS_STM12/Yubikey_and_YubiHSM.spthy @@ -203,7 +203,9 @@ [In(,k2)>) , !HSM(kh,k), !S_AEAD(pid,aead), S_Counter(pid,otc), !S_sid(pid,sid), !Smaller(otc,tc) ] - --[ Login(pid,sid,tc,senc(,k2)) ]-> + --[ Login(pid,sid,tc,senc(,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, + ), mac(, 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), ) + ) @ #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 diff --git a/data/examples/thesis-benedikt/running-examples/DH_Message_Deduction.spthy b/data/examples/thesis-benedikt/running-examples/DH_Message_Deduction.spthy new file mode 100644 --- /dev/null +++ b/data/examples/thesis-benedikt/running-examples/DH_Message_Deduction.spthy @@ -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 diff --git a/data/examples/thesis-benedikt/running-examples/UM_one_pass_eCK_like.spthy b/data/examples/thesis-benedikt/running-examples/UM_one_pass_eCK_like.spthy new file mode 100644 --- /dev/null +++ b/data/examples/thesis-benedikt/running-examples/UM_one_pass_eCK_like.spthy @@ -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( , key ) @ i + // and a matching responder session accept key + & Accept( , 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( , key ) @ i & K( key ) @ j & msid = + // 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 diff --git a/data/examples/thesis-benedikt/running-examples/UM_one_pass_private.spthy b/data/examples/thesis-benedikt/running-examples/UM_one_pass_private.spthy new file mode 100644 --- /dev/null +++ b/data/examples/thesis-benedikt/running-examples/UM_one_pass_private.spthy @@ -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( , key ) @ i + // and a matching responder session accept key + & Accept( , 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 diff --git a/data/intruder_variants_bp.spthy b/data/intruder_variants_bp.spthy new file mode 100644 --- /dev/null +++ b/data/intruder_variants_bp.spthy @@ -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))) ) ] diff --git a/data/intruder_variants_dh.spthy b/data/intruder_variants_dh.spthy --- a/data/intruder_variants_dh.spthy +++ b/data/intruder_variants_dh.spthy @@ -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 ) ] diff --git a/src/Main/Console.hs b/src/Main/Console.hs --- a/src/Main/Console.hs +++ b/src/Main/Console.hs @@ -162,6 +162,7 @@ , modeNames = [name] , modeValue = [] , modeCheck = updateArg "mode" name + , modeExpandAt = False , modeReform = const Nothing-- no reform possibility , modeHelp = help , modeHelpSuffix = [] diff --git a/src/Main/Mode/Intruder.hs b/src/Main/Mode/Intruder.hs --- a/src/Main/Mode/Intruder.hs +++ b/src/Main/Mode/Intruder.hs @@ -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 () diff --git a/src/Main/TheoryLoader.hs b/src/Main/TheoryLoader.hs --- a/src/Main/TheoryLoader.hs +++ b/src/Main/TheoryLoader.hs @@ -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 +-} diff --git a/tamarin-prover.cabal b/tamarin-prover.cabal --- a/tamarin-prover.cabal +++ b/tamarin-prover.cabal @@ -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: