diff --git a/ClassicEAC.spthy b/ClassicEAC.spthy index 87d968871719123f6e0e377aa73465e8fb042ba9..33173fc4703e1a921b93aa097a160985a13ccc79 100644 --- a/ClassicEAC.spthy +++ b/ClassicEAC.spthy @@ -10,73 +10,16 @@ Date: November 2023 theory ClassicEAC begin +#define CLASSIC + builtins: signing, diffie-hellman functions: mac/2, kdf_mac/2, kdf_enc/2 -functions: cert/3, cert_pk/1, cert_sig/1, cert_id/1, ca_sk/0 [private] -equations: cert_pk(cert(pk, s, id)) = pk, cert_sig(cert(pk, s, id)) = s, cert_id(cert(pk, s, id)) = id -macros: verify_cert(cert) = verify(cert_sig(cert), <cert_pk(cert), cert_id(cert)>, pk(ca_sk)) - - - -rule Publish_ca_pk: - [ ] - --> - [ Out(pk(ca_sk)) ] - - -// Registering a static long-term key for terminal -rule Generate_static_ltk: -let - pk = pk(~ltk) -in - [ Fr(~ltk) ] - --> - [ !Pk($A, pk), !Ltk($A, ~ltk), Out(pk) ] - -// Registering a static diffie-hellman key for chip -rule Generate_static_dh: -let - pk = 'g'^~ltk -in - [ Fr(~ltk) ] - --> - [ !PkDH($A, pk), !LtkDH($A, ~ltk), Out(pk) ] - -rule CA_Sign_ltk: -let - certA = cert(pk, sign(<pk, A>, ca_sk), A) -in - [ !Pk(A, pk) ] - --[ Registered(A) ]-> - [ !Cert(A, certA), Out(certA) ] - -rule CA_Sign_dh: -let - certA = cert(pk, sign(<pk, A>, ca_sk), A) -in - [ !PkDH(A, pk) ] - --[ Registered(A) ]-> - [ !CertDH(A, certA), Out(certA) ] +insert(include/setup.spthy) -/* Attacker model */ - -rule Reveal_ltk: - [ !Ltk($A, ltk) ] - --[ Corrupted($A) ]-> - [ Out(ltk) ] - -rule Reveal_dh: - [ !LtkDH($A, ltk) ] - --[ Corrupted($A) ]-> - [ Out(ltk) ] - -rule Reveal_session: - [ !SessionReveal(sid, k) ] - --[ Revealed(sid) ]-> - [ Out(k) ] +insert(include/attacker.spthy) /* Terminal Authentication */ @@ -88,7 +31,7 @@ let pkTe = 'g'^~skTe msg1 = <certT, pkTe, '1', 't'> in - [ !Cert($T, certT), Fr(~skTe), Fr(~iid) ] // skTe is ephemeral session key, iid is instance id of user $T + [ !Cert($T, certT, 'terminal'), Fr(~skTe), Fr(~iid) ] // skTe is ephemeral session key, iid is instance id of user $T --> [ Out(msg1), Out(~iid), TAInitT(<$T, ~iid>, ~skTe) ] // Publish T's iid as its identity gets revealed through certT @@ -99,7 +42,7 @@ let msg2 = <~id_c, ~r1, '2', 'c'> in [ In(msg1), Fr(~r1), Fr(~id_c), Fr(~iid) ] - --[ Eq(verify_cert(certT), true) ]-> + --[ Eq(verify_cert(certT, 'terminal'), true) ]-> [ Out(msg2), TAChallengeC(<$C, ~iid>, certT, pkTe, ~id_c, ~r1) ] rule TA_RESPONSE_T: @@ -109,7 +52,7 @@ let s = sign(<id_c, r1, pkTe>, ~skT) msg3 = <s, '3', 't'> in - [ In(msg2), TAInitT(<$T, iid>, skTe), !Ltk($T, ~skT) ] + [ In(msg2), TAInitT(<$T, iid>, skTe), !Ltk($T, ~skT, 'terminal') ] --[ Computed($T, 'terminal', s) ]-> [ Out(msg3), TAResponseT(<$T, iid>, skTe, id_c) ] @@ -128,9 +71,9 @@ in rule CA_INIT_C: let - msg4 = <certC, '4', 'c'> + msg4 = <certC, ~r2, '4', 'c'> in - [ !CertDH($C, certC), Fr(~r2), TACompleteC(<$C, iid>, certT, pkTe, id_c, r1) ] + [ !Cert($C, certC, 'chip'), Fr(~r2), TACompleteC(<$C, iid>, certT, pkTe, id_c, r1) ] --> [ Out(msg4), Out(iid), CAInitC(<$C, iid>, certT, pkTe, id_c, r1, ~r2) ] // Publish C's iid as its identity gets revealed through certC @@ -138,11 +81,11 @@ in rule CA_INIT_T: let pkTe = 'g'^skTe - msg4 = <certC, '4', 'c'> + msg4 = <certC, r2, '4', 'c'> msg5 = <pkTe, '5', 't'> in [ In(msg4), TAResponseT(<$T, iid>, skTe, id_c) ] - --[ Eq(verify_cert(certC), true) ]-> + --[ Eq(verify_cert(certC, 'chip'), true) ]-> [ Out(msg5), CAInitT(<$T, iid>, skTe, id_c, certC) ] @@ -156,7 +99,7 @@ let msg6 = <r2, tag, '6', 'c'> sid = <certT, certC, pkTe, 'g'^~skC, id_c, r2> in - [ In(msg5), CAInitC(<$C, iid>, certT, pkTe, id_c, r1, r2), !LtkDH($C, ~skC), !CertDH($C, certC) ] + [ In(msg5), CAInitC(<$C, iid>, certT, pkTe, id_c, r1, r2), !Ltk($C, ~skC, 'chip'), !Cert($C, certC, 'chip') ] --[ Eq(pkTe_t, pkTe), Computed($C, 'chip', <k, kMac, kEnc, tag>), Completed(<kEnc, kMac>, sid, $C, 'chip', cert_id(certT)) ]-> [ Out(msg6), CAFinishC($C, cert_id(certT), kEnc) ] @@ -172,19 +115,12 @@ let tag_T = mac(pkTe, kMac) sid = <certT, certC, pkTe, pkC, id_c, r2> in - [ In(msg6), CAInitT(<$T, iid>, skTe, id_c, certC), !Cert($T, certT) ] + [ In(msg6), CAInitT(<$T, iid>, skTe, id_c, certC), !Cert($T, certT, 'terminal') ] --[ Eq(tag, tag_T), Computed($T, 'terminal', <k, kMac, kEnc, tag_T>), Completed(<kEnc, kMac>, sid, $T, 'terminal', cert_id(certC)), Finished(sid) ]-> [ CAFinishT(cert_id(certC), $T, kEnc), !SessionReveal(sid, <kEnc, kMac>) ] -restriction OneCertPerIdentity: - "All id #i #j. Registered(id) @ #i & Registered(id) @ #j ==> #i = #j" - -restriction Equality: - "All x y #i. Eq(x, y) @ i ==> x = y" - - -insert(lemmas.spthy) +insert(include/lemmas.spthy) end diff --git a/FastKemPQEAC.spthy b/FastKemPQEAC.spthy index 186c1f40d3dfb6c46cf1debefa93ba64f9fef000..91ad6f0d0a0d247414d04b18955a4e6a3c9f1ccb 100644 --- a/FastKemPQEAC.spthy +++ b/FastKemPQEAC.spthy @@ -15,47 +15,10 @@ functions: mac/2, kdf/2 functions: encaps/2, decaps/2 equations: decaps((encaps(k, pk(sk))), sk) = k -functions: cert/3, cert_pk/1, cert_sig/1, cert_id/1, ca_sk/0 [private] -equations: cert_pk(cert(pk, s, id)) = pk, cert_sig(cert(pk, s, id)) = s, cert_id(cert(pk, s, id)) = id -macros: verify_cert(cert) = verify(cert_sig(cert), <cert_pk(cert), cert_id(cert)>, pk(ca_sk)) +insert(include/setup.spthy) - -rule Publish_ca_pk: - [ ] - --> - [ Out(pk(ca_sk)) ] - - -// Registering a static long-term key for terminal -rule Generate_static_ltk: -let - pk = pk(~ltk) -in - [ Fr(~ltk) ] - --> - [ !Pk($A, pk), !Ltk($A, ~ltk), Out(pk) ] - -rule CA_Sign_ltk: -let - certA = cert(pk, sign(<pk, A>, ca_sk), A) -in - [ !Pk(A, pk) ] - --> - [ !Cert(A, certA), Out(certA) ] - - -/* Attacker model */ - -rule Reveal_ltk: - [ !Ltk($A, ltk) ] - --[ Corrupted($A) ]-> - [ Out(ltk) ] - -rule Reveal_session: - [ !SessionReveal(sid, k) ] - --[ Revealed(sid) ]-> - [ Out(k) ] +insert(include/attacker.spthy) @@ -67,7 +30,7 @@ rule TA_INIT_T: let msg1 = <certT, '1', 't'> in - [ !Cert($T, certT), Fr(~iid) ] + [ !Cert($T, certT, 'terminal'), Fr(~iid) ] --> [ Out(msg1), Out(~iid), TAInitT(<$T, ~iid>) ] @@ -82,8 +45,8 @@ let cCA = senc(<certC, ~r2, pk(~skCe)>, kTENC) msg2 = <~id_c, ~r1, cTA, cCA, '2', 'c'> in - [ In(msg1), Fr(~r1), Fr(~id_c), Fr(~kTA), Fr(~r2), Fr(~skCe), Fr(~iid), !Cert($C, certC) ] - --[ Eq(verify_cert(certT), true) ]-> + [ In(msg1), Fr(~r1), Fr(~id_c), Fr(~kTA), Fr(~r2), Fr(~skCe), Fr(~iid), !Cert($C, certC, 'chip') ] + --[ Eq(verify_cert(certT, 'terminal'), true) ]-> [ Out(msg2), Out(~iid), TAChallengeC(<$C, ~iid>, certT, ~id_c, ~r1, ~r2, ~skCe, kTMAC, kTCNF) ] #else rule TA_CHALLENGE_C: @@ -96,8 +59,8 @@ let cCA = senc(<certC, ~r2>, kTENC) msg2 = <~id_c, ~r1, cTA, cCA, '2', 'c'> in - [ In(msg1), Fr(~r1), Fr(~id_c), Fr(~kTA), Fr(~r2), Fr(~iid), !Cert($C, certC) ] - --[ Eq(verify_cert(certT), true) ]-> + [ In(msg1), Fr(~r1), Fr(~id_c), Fr(~kTA), Fr(~r2), Fr(~iid), !Cert($C, certC, 'chip') ] + --[ Eq(verify_cert(certT, 'terminal'), true) ]-> [ Out(msg2), Out(~iid), TAChallengeC(<$C, ~iid>, certT, ~id_c, ~r1, ~r2, kTMAC, kTCNF) ] #endif @@ -120,8 +83,8 @@ let s = mac(<'CA', sid>, kTMAC) msg3 = <kTCNF, cip, s, cipe, '3', 't'> in - [ In(msg2), Fr(~k), Fr(~ke), TAInitT(<$T, iid>), !Ltk($T, ~skT), !Cert($T, certT) ] - --[ Eq(verify_cert(certC), true) ]-> + [ In(msg2), Fr(~k), Fr(~ke), TAInitT(<$T, iid>), !Ltk($T, ~skT, 'terminal'), !Cert($T, certT, 'terminal') ] + --[ Eq(verify_cert(certC, 'chip'), true) ]-> [ Out(msg3), TAResponseT(<$T, iid>, id_c, certC, r2, <~k, cip>, <~ke, cipe>, pkCe) ] #else rule TA_RESPONSE_T: @@ -140,8 +103,8 @@ let s = mac(<'CA', sid>, kTMAC) msg3 = <kTCNF, cip, s, '3', 't'> in - [ In(msg2), Fr(~k), TAInitT(<$T, iid>), !Ltk($T, ~skT), !Cert($T, certT) ] - --[ Eq(verify_cert(certC), true) ]-> + [ In(msg2), Fr(~k), TAInitT(<$T, iid>), !Ltk($T, ~skT, 'terminal'), !Cert($T, certT, 'terminal') ] + --[ Eq(verify_cert(certC, 'chip'), true) ]-> [ Out(msg3), TAResponseT(<$T, iid>, id_c, certC, r2, <~k, cip>) ] #endif @@ -156,7 +119,7 @@ let kKEY = kdf(<'KEY', sid>, <k, ke>) msg4 = <kCNF, '4', 'c'> in - [ In(msg3), TAChallengeC(<$C, iid>, certT, id_c, r1, r2, skCe, kTMAC, kTCNF), !Ltk($C, ~skC), !Cert($C, certC) ] + [ In(msg3), TAChallengeC(<$C, iid>, certT, id_c, r1, r2, skCe, kTMAC, kTCNF), !Ltk($C, ~skC, 'chip'), !Cert($C, certC, 'chip') ] --[ Eq(kTCNF_T, kTCNF), Eq(s, mac(<'CA', sid>, kTMAC)), CompletedTA($C, iid, cert_id(certT)), Completed(kKEY, sid, $C, 'chip', cert_id(certT)), Completed(kKEY, sid, $C, 'chip', cert_id(certT)) ]-> [ Out(msg4), TACompleteC(<$C, iid>, kKEY) ] #else @@ -169,7 +132,7 @@ let kKEY = kdf(<'KEY', sid>, k) msg4 = <kCNF, '4', 'c'> in - [ In(msg3), TAChallengeC(<$C, iid>, certT, id_c, r1, r2, kTMAC, kTCNF), !Ltk($C, ~skC), !Cert($C, certC) ] + [ In(msg3), TAChallengeC(<$C, iid>, certT, id_c, r1, r2, kTMAC, kTCNF), !Ltk($C, ~skC, 'chip'), !Cert($C, certC, 'chip') ] --[ Eq(kTCNF_T, kTCNF), Eq(s, mac(<'CA', sid>, kTMAC)), CompletedTA($C, iid, cert_id(certT)), Completed(kKEY, sid, $C, 'chip', cert_id(certT)), Completed(kKEY, sid, $C, 'chip', cert_id(certT)) ]-> [ Out(msg4), TACompleteC(<$C, iid>, kKEY) ] #endif @@ -182,7 +145,7 @@ let kCNF = kdf(<'CNF', sid>, <k, ke>) kKEY = kdf(<'KEY', sid>, <k, ke>) in - [ In(msg4), TAResponseT(<$T, iid>, id_c, certC, r2, <k, cip>, <ke, cipe>, pkCe), !Cert($T, certT) ] + [ In(msg4), TAResponseT(<$T, iid>, id_c, certC, r2, <k, cip>, <ke, cipe>, pkCe), !Cert($T, certT, 'terminal') ] --[ Eq(kCNF, kCNF_C), Completed(kKEY, sid, $T, 'terminal', cert_id(certC)), Finished(sid) ]-> [ CAFinishT(cert_id(certC), $T, kKEY), !SessionReveal(sid, kKEY) ] #else @@ -201,10 +164,6 @@ in - -restriction Equality: - "All x y #i. Eq(x, y) @ i ==> x = y" - -insert(lemmas.spthy) +insert(include/lemmas.spthy) end diff --git a/FastSigPQEAC.spthy b/FastSigPQEAC.spthy index 48a3cad0f28fb681852d668b0f6b205850b9048b..0e101cd4c2de739f73c6d4c60062840c411ca05f 100644 --- a/FastSigPQEAC.spthy +++ b/FastSigPQEAC.spthy @@ -15,48 +15,10 @@ functions: kdf/2 functions: encaps/2, decaps/2 equations: decaps((encaps(k, pk(sk))), sk) = k -functions: cert/3, cert_pk/1, cert_sig/1, cert_id/1, ca_sk/0 [private] -equations: cert_pk(cert(pk, s, id)) = pk, cert_sig(cert(pk, s, id)) = s, cert_id(cert(pk, s, id)) = id -macros: verify_cert(cert) = verify(cert_sig(cert), <cert_pk(cert), cert_id(cert)>, pk(ca_sk)) +insert(include/setup.spthy) - -rule Publish_ca_pk: - [ ] - --> - [ Out(pk(ca_sk)) ] - - -// Registering a static long-term key for terminal -rule Generate_static_ltk: -let - pk = pk(~ltk) -in - [ Fr(~ltk) ] - --> - [ !Pk($A, pk), !Ltk($A, ~ltk), Out(pk) ] - -rule CA_Sign_ltk: -let - certA = cert(pk, sign(<pk, A>, ca_sk), A) -in - [ !Pk(A, pk) ] - --> - [ !Cert(A, certA), Out(certA) ] - - -/* Attacker model */ - -rule Reveal_ltk: - [ !Ltk($A, ltk) ] - --[ Corrupted($A) ]-> - [ Out(ltk) ] - -rule Reveal_session: - [ !SessionReveal(sid, k) ] - --[ Revealed(sid) ]-> - [ Out(k) ] - +insert(include/attacker.spthy) /* Terminal Authentication */ @@ -67,7 +29,7 @@ rule TA_INIT_T: let msg1 = <certT, '1', 't'> in - [ !Cert($T, certT), Fr(~iid) ] + [ !Cert($T, certT, 'terminal'), Fr(~iid) ] --> [ Out(msg1), Out(~iid), TAInitT(<$T, ~iid>) ] @@ -77,8 +39,8 @@ let msg1 = <certT, '1', 't'> msg2 = <~id_c, ~r1, certC, ~r2, pk(~skCe), '2', 'c'> in - [ In(msg1), Fr(~r1), Fr(~id_c), Fr(~iid), Fr(~skCe), Fr(~r2), !Cert($C, certC) ] - --[ Eq(verify_cert(certT), true) ]-> + [ In(msg1), Fr(~r1), Fr(~id_c), Fr(~iid), Fr(~skCe), Fr(~r2), !Cert($C, certC, 'chip') ] + --[ Eq(verify_cert(certT, 'terminal'), true) ]-> [ Out(msg2), Out(~iid), TAChallengeC(<$C, ~iid>, certT, ~id_c, ~r1, ~skCe, ~r2) ] #else rule TA_CHALLENGE_C: @@ -86,8 +48,8 @@ let msg1 = <certT, '1', 't'> msg2 = <~id_c, ~r1, certC, ~r2, '2', 'c'> in - [ In(msg1), Fr(~r1), Fr(~id_c), Fr(~iid), Fr(~r2), !Cert($C, certC) ] - --[ Eq(verify_cert(certT), true) ]-> + [ In(msg1), Fr(~r1), Fr(~id_c), Fr(~iid), Fr(~r2), !Cert($C, certC, 'chip') ] + --[ Eq(verify_cert(certT, 'terminal'), true) ]-> [ Out(msg2), Out(~iid), TAChallengeC(<$C, ~iid>, certT, ~id_c, ~r1, ~r2) ] #endif @@ -103,8 +65,8 @@ let s2 = sign(<'CA', sid>, ~skT) msg3 = <cip, cipe, s1, s2, '3', 't'> in - [ In(msg2), TAInitT(<$T, iid>), !Ltk($T, ~skT), !Cert($T, certT), Fr(~k), Fr(~ke) ] - --[ Eq(verify_cert(certC), true) ]-> + [ In(msg2), TAInitT(<$T, iid>), !Ltk($T, ~skT, 'terminal'), !Cert($T, certT, 'terminal'), Fr(~k), Fr(~ke) ] + --[ Eq(verify_cert(certC, 'chip'), true) ]-> [ Out(msg3), CAInitT(<$T, iid>, id_c, certC, r2, <~k, cip>, <~ke, cipe>, pkCe) ] #else rule TA_RESPONSE_T: @@ -117,8 +79,8 @@ let s2 = sign(<'CA', sid>, ~skT) msg3 = <cip, s1, s2, '3', 't'> in - [ In(msg2), TAInitT(<$T, iid>), !Ltk($T, ~skT), !Cert($T, certT), Fr(~k) ] - --[ Eq(verify_cert(certC), true) ]-> + [ In(msg2), TAInitT(<$T, iid>), !Ltk($T, ~skT, 'terminal'), !Cert($T, certT, 'terminal'), Fr(~k) ] + --[ Eq(verify_cert(certC, 'chip'), true) ]-> [ Out(msg3), CAInitT(<$T, iid>, id_c, certC, r2, <~k, cip>) ] #endif @@ -133,7 +95,7 @@ let kKEY = kdf(<'KEY', sid>, <k, ke>) msg4 = <kCNF, '4', 'c'> in - [ In(msg3), TAChallengeC(<$C, iid>, certT, id_c, r1, skCe, r2), !Ltk($C, ~skC), !Cert($C, certC) ] + [ In(msg3), TAChallengeC(<$C, iid>, certT, id_c, r1, skCe, r2), !Ltk($C, ~skC, 'chip'), !Cert($C, certC, 'chip') ] --[ Eq(verify(s1, <'TA', id_c, r1>, cert_pk(certT)), true), Eq(verify(s2, <'CA', sid>, cert_pk(certT)), true), CompletedTA($C, iid, cert_id(certT)), Completed(kKEY, sid, $C, 'chip', cert_id(certT)) ]-> [ Out(msg4), TACompleteC(<$C, iid>, certT, id_c, r1, skCe, r2) ] #else @@ -146,7 +108,7 @@ let kKEY = kdf(<'KEY', sid>, k) msg4 = <kCNF, '4', 'c'> in - [ In(msg3), TAChallengeC(<$C, iid>, certT, id_c, r1, r2), !Ltk($C, ~skC), !Cert($C, certC) ] + [ In(msg3), TAChallengeC(<$C, iid>, certT, id_c, r1, r2), !Ltk($C, ~skC, 'chip'), !Cert($C, certC, 'chip') ] --[ Eq(verify(s1, <'TA', id_c, r1>, cert_pk(certT)), true), Eq(verify(s2, <'CA', sid>, cert_pk(certT)), true), CompletedTA($C, iid, cert_id(certT)), Completed(kKEY, sid, $C, 'chip', cert_id(certT)) ]-> [ Out(msg4), TACompleteC(<$C, iid>, certT, id_c, r1, r2) ] #endif @@ -159,7 +121,7 @@ let kCNF = kdf(<'CNF', sid>, <k, ke>) kKEY = kdf(<'KEY', sid>, <k, ke>) in - [ In(msg4), CAInitT(<$T, iid>, id_c, certC, r2, <k, cip>, <ke, cipe>, pkCe), !Cert($T, certT) ] + [ In(msg4), CAInitT(<$T, iid>, id_c, certC, r2, <k, cip>, <ke, cipe>, pkCe), !Cert($T, certT, 'terminal') ] --[ Eq(kCNF, kCNF_C), Completed(kKEY, sid, $T, 'terminal', cert_id(certC)), Finished(sid) ]-> [ CAFinishT(cert_id(certC), $T, kKEY), !SessionReveal(sid, kKEY) ] #else @@ -170,17 +132,13 @@ let kCNF = kdf(<'CNF', sid>, k) kKEY = kdf(<'KEY', sid>, k) in - [ In(msg4), CAInitT(<$T, iid>, id_c, certC, r2, <k, cip>), !Cert($T, certT) ] + [ In(msg4), CAInitT(<$T, iid>, id_c, certC, r2, <k, cip>), !Cert($T, certT, 'terminal') ] --[ Eq(kCNF, kCNF_C), Completed(kKEY, sid, $T, 'terminal', cert_id(certC)), Finished(sid) ]-> [ CAFinishT(cert_id(certC), $T, kKEY), !SessionReveal(sid, kKEY) ] #endif - -restriction Equality: - "All x y #i. Eq(x, y) @ i ==> x = y" - -insert(lemmas.spthy) +insert(include/lemmas.spthy) end diff --git a/KemPQEAC.spthy b/KemPQEAC.spthy index 227f0cfc7a9382ec8a93f6d97a0dee0d64bf8c45..f17d6b454a28b5ff72d8eac6bd24ce052dd1b54b 100644 --- a/KemPQEAC.spthy +++ b/KemPQEAC.spthy @@ -15,47 +15,10 @@ functions: mac/2, kdf/2 functions: encaps/2, decaps/2 equations: decaps((encaps(k, pk(sk))), sk) = k -functions: cert/3, cert_pk/1, cert_sig/1, cert_id/1, ca_sk/0 [private] -equations: cert_pk(cert(pk, s, id)) = pk, cert_sig(cert(pk, s, id)) = s, cert_id(cert(pk, s, id)) = id -macros: verify_cert(cert) = verify(cert_sig(cert), <cert_pk(cert), cert_id(cert)>, pk(ca_sk)) +insert(include/setup.spthy) - -rule Publish_ca_pk: - [ ] - --> - [ Out(pk(ca_sk)) ] - - -// Registering a static long-term key for terminal -rule Generate_static_ltk: -let - pk = pk(~ltk) -in - [ Fr(~ltk) ] - --> - [ !Pk($A, pk), !Ltk($A, ~ltk), Out(pk) ] - -rule CA_Sign_ltk: -let - certA = cert(pk, sign(<pk, A>, ca_sk), A) -in - [ !Pk(A, pk) ] - --> - [ !Cert(A, certA), Out(certA) ] - - -/* Attacker model */ - -rule Reveal_ltk: - [ !Ltk($A, ~ltk) ] - --[ Corrupted($A) ]-> - [ Out(~ltk) ] - -rule Reveal_session: - [ !SessionReveal(sid, k) ] - --[ Revealed(sid) ]-> - [ Out(k) ] +insert(include/attacker.spthy) @@ -67,7 +30,7 @@ rule TA_INIT_T: let msg1 = <certT, '1', 't'> in - [ !Cert($T, certT), Fr(~iid) ] + [ !Cert($T, certT, 'terminal'), Fr(~iid) ] --> [ Out(msg1), Out(~iid), TAInitT(<$T, ~iid>) ] @@ -79,7 +42,7 @@ let msg2 = <~id_c, ~r1, cTA, '2', 'c'> in [ In(msg1), Fr(~r1), Fr(~id_c), Fr(~kTA), Fr(~iid) ] - --[ Eq(verify_cert(certT), true) ]-> + --[ Eq(verify_cert(certT, 'terminal'), true) ]-> [ Out(msg2), TAChallengeC(<$C, ~iid>, certT, ~id_c, ~r1, <~kTA, cTA>) ] rule TA_RESPONSE_T: @@ -91,7 +54,7 @@ let kTCNF = kdf(<'TCNF', r1>, kTA) msg3 = <kTCNF, '3', 't'> in - [ In(msg2), TAInitT(<$T, iid>), !Ltk($T, ~skT) ] + [ In(msg2), TAInitT(<$T, iid>), !Ltk($T, ~skT, 'terminal') ] --> [ Out(msg3), TAResponseT(<$T, iid>, id_c, kTMAC, kTENC) ] @@ -117,7 +80,7 @@ let cCA = senc(<certC, ~r2, pk(~skCe)>, kTENC) msg4 = <cCA, '4', 'c'> in - [ !Cert($C, certC), Fr(~r2), Fr(~skCe), TACompleteC(<$C, iid>, certT, id_c, r1, <kTA, cTA>, kTMAC, kTENC) ] + [ !Cert($C, certC, 'chip'), Fr(~r2), Fr(~skCe), TACompleteC(<$C, iid>, certT, id_c, r1, <kTA, cTA>, kTMAC, kTENC) ] --> [ Out(msg4), Out(iid), CAInitC(<$C, iid>, certT, id_c, r1, <kTA, cTA>, kTMAC, kTENC, ~r2, ~skCe) ] #else @@ -126,7 +89,7 @@ let cCA = senc(<certC, ~r2>, kTENC) msg4 = <cCA, '4', 'c'> in - [ !Cert($C, certC), Fr(~r2), TACompleteC(<$C, iid>, certT, id_c, r1, <kTA, cTA>, kTMAC, kTENC) ] + [ !Cert($C, certC, 'chip'), Fr(~r2), TACompleteC(<$C, iid>, certT, id_c, r1, <kTA, cTA>, kTMAC, kTENC) ] --> [ Out(msg4), Out(iid), CAInitC(<$C, iid>, certT, id_c, r1, <kTA, cTA>, kTMAC, kTENC, ~r2) ] #endif @@ -147,8 +110,8 @@ let s = mac(<'CA', sid>, kTMAC) msg5 = <cip, s, cipe, '5', 't'> in - [ In(msg4), TAResponseT(<$T, iid>, id_c, kTMAC, kTENC), !Cert($T, certT), Fr(~k), Fr(~ke) ] - --[ Eq(verify_cert(certC), true) ]-> + [ In(msg4), TAResponseT(<$T, iid>, id_c, kTMAC, kTENC), !Cert($T, certT, 'terminal'), Fr(~k), Fr(~ke) ] + --[ Eq(verify_cert(certC, 'chip'), true) ]-> [ Out(msg5), CAInitT(<$T, iid>, id_c, kTMAC, kTENC, certC, r2, <~k, cip>, <~ke, cipe>, pkCe) ] #else rule CA_INIT_T: @@ -163,8 +126,8 @@ let s = mac(<'CA', sid>, kTMAC) msg5 = <cip, s, '5', 't'> in - [ In(msg4), TAResponseT(<$T, iid>, id_c, kTMAC, kTENC), !Cert($T, certT), Fr(~k) ] - --[ Eq(verify_cert(certC), true) ]-> + [ In(msg4), TAResponseT(<$T, iid>, id_c, kTMAC, kTENC), !Cert($T, certT, 'terminal'), Fr(~k) ] + --[ Eq(verify_cert(certC, 'chip'), true) ]-> [ Out(msg5), CAInitT(<$T, iid>, id_c, kTMAC, kTENC, certC, r2, <~k, cip>) ] #endif @@ -180,7 +143,7 @@ let kKEY = kdf(<'KEY', sid>, <k, ke>) msg6 = <kCNF, '6', 'c'> in - [ In(msg5), CAInitC(<$C, iid>, certT, id_c, r1, <kTA, cTA>, kTMAC, kTENC, r2, skCe), !Ltk($C, ~skC), !Cert($C, certC) ] + [ In(msg5), CAInitC(<$C, iid>, certT, id_c, r1, <kTA, cTA>, kTMAC, kTENC, r2, skCe), !Ltk($C, ~skC, 'chip'), !Cert($C, certC, 'chip') ] --[ Eq(s, mac(<'CA', sid>, kTMAC)), Completed(kKEY, sid, $C, 'chip', cert_id(certT)) ]-> [ Out(msg6), CAFinishC($C, cert_id(certT), kKEY) ] #else @@ -193,7 +156,7 @@ let kKEY = kdf(<'KEY', sid>, k) msg6 = <kCNF, '6', 'c'> in - [ In(msg5), CAInitC(<$C, iid>, certT, id_c, r1, <kTA, cTA>, kTMAC, kTENC, r2), !Ltk($C, ~skC), !Cert($C, certC) ] + [ In(msg5), CAInitC(<$C, iid>, certT, id_c, r1, <kTA, cTA>, kTMAC, kTENC, r2), !Ltk($C, ~skC, 'chip'), !Cert($C, certC, 'chip') ] --[ Eq(s, mac(<'CA', sid>, kTMAC)), Completed(kKEY, sid, $C, 'chip', cert_id(certT)) ]-> [ Out(msg6), CAFinishC($C, cert_id(certT), kKEY) ] #endif @@ -207,7 +170,7 @@ let kCNF = kdf(<'CNF', sid>, <k, ke>) kKEY = kdf(<'KEY', sid>, <k, ke>) in - [ In(msg6), CAInitT(<$T, iid>, id_c, kTMAC, kTENC, certC, r2, <k, cip>, <ke, cipe>, pkCe), !Cert($T, certT) ] + [ In(msg6), CAInitT(<$T, iid>, id_c, kTMAC, kTENC, certC, r2, <k, cip>, <ke, cipe>, pkCe), !Cert($T, certT, 'terminal') ] --[ Eq(kCNF, kCNF_c), Completed(kKEY, sid, $T, 'terminal', cert_id(certC)), Finished(sid) ]-> [ CAFinishT(cert_id(certC), $T, kKEY), !SessionReveal(sid, kKEY) ] #else @@ -218,16 +181,13 @@ let kCNF = kdf(<'CNF', sid>, k) kKEY = kdf(<'KEY', sid>, k) in - [ In(msg6), CAInitT(<$T, iid>, id_c, kTMAC, kTENC, certC, r2, <k, cip>), !Cert($T, certT) ] + [ In(msg6), CAInitT(<$T, iid>, id_c, kTMAC, kTENC, certC, r2, <k, cip>), !Cert($T, certT, 'terminal') ] --[ Eq(kCNF, kCNF_c), Completed(kKEY, sid, $T, 'terminal', cert_id(certC)), Finished(sid) ]-> [ CAFinishT(cert_id(certC), $T, kKEY), !SessionReveal(sid, kKEY) ] #endif -restriction Equality: - "All x y #i. Eq(x, y) @ i ==> x = y" - -insert(lemmas.spthy) +insert(include/lemmas.spthy) end diff --git a/SigPQEAC.spthy b/SigPQEAC.spthy index 2150cf6566d100ea4d11a9080da49ca73faf580f..6ef2ee1817450f35c3a672e81ef1dded6a0a1551 100644 --- a/SigPQEAC.spthy +++ b/SigPQEAC.spthy @@ -15,47 +15,10 @@ functions: kdf/2 functions: encaps/2, decaps/2 equations: decaps((encaps(k, pk(sk))), sk) = k -functions: cert/3, cert_pk/1, cert_sig/1, cert_id/1, ca_sk/0 [private] -equations: cert_pk(cert(pk, s, id)) = pk, cert_sig(cert(pk, s, id)) = s, cert_id(cert(pk, s, id)) = id -macros: verify_cert(cert) = verify(cert_sig(cert), <cert_pk(cert), cert_id(cert)>, pk(ca_sk)) +insert(include/setup.spthy) - -rule Publish_ca_pk: - [ ] - --> - [ Out(pk(ca_sk)) ] - - -// Registering a static long-term key for terminal -rule Generate_static_ltk: -let - pk = pk(~ltk) -in - [ Fr(~ltk) ] - --> - [ !Pk($A, pk), !Ltk($A, ~ltk), Out(pk) ] - -rule CA_Sign_ltk: -let - certA = cert(pk, sign(<pk, A>, ca_sk), A) -in - [ !Pk(A, pk) ] - --> - [ !Cert(A, certA), Out(certA) ] - - -/* Attacker model */ - -rule Reveal_ltk: - [ !Ltk($A, ltk) ] - --[ Corrupted($A) ]-> - [ Out(ltk) ] - -rule Reveal_session: - [ !SessionReveal(sid, k) ] - --[ Revealed(sid) ]-> - [ Out(k) ] +insert(include/attacker.spthy) @@ -67,7 +30,7 @@ rule TA_INIT_T: let msg1 = <certT, '1', 't'> in - [ !Cert($T, certT), Fr(~iid) ] + [ !Cert($T, certT, 'terminal'), Fr(~iid) ] --> [ Out(msg1), Out(~iid), TAInitT(<$T, ~iid>) ] @@ -78,7 +41,7 @@ let msg2 = <~id_c, ~r1, '2', 'c'> in [ In(msg1), Fr(~r1), Fr(~id_c), Fr(~iid) ] - --[ Eq(verify_cert(certT), true) ]-> + --[ Eq(verify_cert(certT, 'terminal'), true) ]-> [ Out(msg2), TAChallengeC(<$C, ~iid>, certT, ~id_c, ~r1) ] rule TA_RESPONSE_T: @@ -87,7 +50,7 @@ let s = sign(<'TA', id_c, r1>, ~skT) msg3 = <s, '3', 't'> in - [ In(msg2), TAInitT(<$T, iid>), !Ltk($T, ~skT) ] + [ In(msg2), TAInitT(<$T, iid>), !Ltk($T, ~skT, 'terminal') ] --> [ Out(msg3), TAResponseT(<$T, iid>, id_c) ] @@ -109,7 +72,7 @@ rule CA_INIT_C: let msg4 = <certC, ~r2, pk(~skCe), '4', 'c'> in - [ Fr(~r2), Fr(~skCe), TACompleteC(<$C, iid>, certT, id_c, r1), !Cert($C, certC) ] + [ Fr(~r2), Fr(~skCe), TACompleteC(<$C, iid>, certT, id_c, r1), !Cert($C, certC, 'chip') ] --> [ Out(msg4), Out(iid), CAInitC(<$C, iid>, certT, id_c, r1, ~r2, ~skCe) ] #else @@ -117,7 +80,7 @@ rule CA_INIT_C: let msg4 = <certC, ~r2, '4', 'c'> in - [ Fr(~r2), TACompleteC(<$C, iid>, certT, id_c, r1), !Cert($C, certC) ] + [ Fr(~r2), TACompleteC(<$C, iid>, certT, id_c, r1), !Cert($C, certC, 'chip') ] --> [ Out(msg4), Out(iid), CAInitC(<$C, iid>, certT, id_c, r1, ~r2) ] #endif @@ -134,8 +97,8 @@ let s = sign(<'CA', sid>, ~skT) msg5 = <cip, s, cipe, '5', 't'> in - [ In(msg4), Fr(~k), Fr(~ke), TAResponseT(<$T, iid>, id_c), !Ltk($T, ~skT), !Cert($T, certT) ] - --[ Eq(verify_cert(certC), true) ]-> + [ In(msg4), Fr(~k), Fr(~ke), TAResponseT(<$T, iid>, id_c), !Ltk($T, ~skT, 'terminal'), !Cert($T, certT, 'terminal') ] + --[ Eq(verify_cert(certC, 'chip'), true) ]-> [ Out(msg5), CAInitT(<$T, iid>, id_c, certC, r2, <~k, cip>, <~ke, cipe>, pkCe) ] #else rule CA_INIT_T: @@ -147,8 +110,8 @@ let s = sign(<'CA', sid>, ~skT) msg5 = <cip, s, '5', 't'> in - [ In(msg4), Fr(~k), TAResponseT(<$T, iid>, id_c), !Ltk($T, ~skT), !Cert($T, certT) ] - --[ Eq(verify_cert(certC), true) ]-> + [ In(msg4), Fr(~k), TAResponseT(<$T, iid>, id_c), !Ltk($T, ~skT, 'terminal'), !Cert($T, certT, 'terminal') ] + --[ Eq(verify_cert(certC, 'chip'), true) ]-> [ Out(msg5), CAInitT(<$T, iid>, id_c, certC, r2, <~k, cip>) ] #endif @@ -164,7 +127,7 @@ let kKEY = kdf(<'KEY', sid>, <k, ke>) msg6 = <kCNF, '6', 'c'> in - [ In(msg5), CAInitC(<$C, iid>, certT, id_c, r1, r2, skCe), !Ltk($C, ~skC), !Cert($C, certC) ] + [ In(msg5), CAInitC(<$C, iid>, certT, id_c, r1, r2, skCe), !Ltk($C, ~skC, 'chip'), !Cert($C, certC, 'chip') ] --[ Eq(verify(s, <'CA', sid>, cert_pk(certT)), true), Completed(kKEY, sid, $C, 'chip', cert_id(certT)) ]-> [ Out(msg6), CAFinishC($C, cert_id(certT), kKEY) ] #else @@ -177,7 +140,7 @@ let kKEY = kdf(<'KEY', sid>, k) msg6 = <kCNF, '6', 'c'> in - [ In(msg5), CAInitC(<$C, iid>, certT, id_c, r1, r2), !Ltk($C, ~skC), !Cert($C, certC) ] + [ In(msg5), CAInitC(<$C, iid>, certT, id_c, r1, r2), !Ltk($C, ~skC, 'chip'), !Cert($C, certC, 'chip') ] --[ Eq(verify(s, <'CA', sid>, cert_pk(certT)), true), Completed(kKEY, sid, $C, 'chip', cert_id(certT)) ]-> [ Out(msg6), CAFinishC($C, cert_id(certT), kKEY) ] #endif @@ -190,7 +153,7 @@ let kCNF = kdf(<'CNF', sid>, <k, ke>) kKEY = kdf(<'KEY', sid>, <k, ke>) in - [ In(msg6), CAInitT(<$T, iid>, id_c, certC, r2, <k, cip>, <ke, cipe>, pkCe), !Cert($T, certT) ] + [ In(msg6), CAInitT(<$T, iid>, id_c, certC, r2, <k, cip>, <ke, cipe>, pkCe), !Cert($T, certT, 'terminal') ] --[ Eq(kCNF, kCNF_C), Completed(kKEY, sid, $T, 'terminal', cert_id(certC)), Finished(sid) ]-> [ CAFinishT(cert_id(certC), $T, kKEY), !SessionReveal(sid, kKEY) ] #else @@ -201,7 +164,7 @@ let kCNF = kdf(<'CNF', sid>, k) kKEY = kdf(<'KEY', sid>, k) in - [ In(msg6), CAInitT(<$T, iid>, id_c, certC, r2, <k, cip>), !Cert($T, certT) ] + [ In(msg6), CAInitT(<$T, iid>, id_c, certC, r2, <k, cip>), !Cert($T, certT, 'terminal') ] --[ Eq(kCNF, kCNF_c), Completed(kKEY, sid, $T, 'terminal', cert_id(certC)), Finished(sid) ]-> [ CAFinishT(cert_id(certC), $T, kKEY), !SessionReveal(sid, kKEY) ] #endif @@ -209,9 +172,6 @@ in -restriction Equality: - "All x y #i. Eq(x, y) @ i ==> x = y" - -insert(lemmas.spthy) +insert(include/lemmas.spthy) end diff --git a/include/attacker.spthy b/include/attacker.spthy new file mode 100644 index 0000000000000000000000000000000000000000..c535652ab631dca1d1866e8014ec69312fba526e --- /dev/null +++ b/include/attacker.spthy @@ -0,0 +1,12 @@ +/* Attacker model */ +// We extend the Dolev-Yao attack model in tamarin with Reveal and Corrupt capabilities + +rule Corrupt_ltk: + [ !Ltk($A, ltk, role) ] + --[ Corrupted($A) ]-> + [ Out(<ltk, role>) ] + +rule Reveal_session: + [ !SessionReveal(sid, k) ] + --[ Revealed(sid) ]-> + [ Out(k) ] diff --git a/lemmas.spthy b/include/lemmas.spthy similarity index 88% rename from lemmas.spthy rename to include/lemmas.spthy index 41cde129e8fc8c5559186124c1f5b294b51ee7b5..1ab016157b511509ad9960cf1ca99917b6ab7997 100644 --- a/lemmas.spthy +++ b/include/lemmas.spthy @@ -1,3 +1,9 @@ +/* Contains the restrictions and lemmas for all EAC models */ + +restriction Equality: + "All x y #i. Eq(x, y) @ i ==> x = y" + + // Correctness lemma session_exist: exists-trace @@ -103,15 +109,14 @@ lemma chip_hiding: | (Ex #m . (K(iid) @ #m & #i < #m)) " -/* -lemma nonRepudiation: - "All sid #n . - Finished(sid) @ #n - ==> (Ex T data #m . Computed(T, 'terminal', data) @ #m - & not(Ex #k . K(data) @ #k & #k < #m) - & not(Ex #k . Corrupted(T) @ #k)) +lemma nonRepudiation: exists-trace + "Ex C T k sid #i #j . + Completed(k, sid, C, 'chip', T) @ #i + & Completed(k, sid, T, 'terminal', C) @ #j + & not(Ex #n . Corrupted(C) @ #n) + & (All data #m . Computed(C, 'chip', data) @ #m + ==> (Ex #k . K(data) @ #k & #k < #m)) " -*/ // Perfect forward secrecy lemma pfs: @@ -123,4 +128,3 @@ lemma pfs: ==> (not(Ex #m . K(k) @ #m) | (Ex #m . Revealed(sid) @ #m)) " - diff --git a/include/setup.spthy b/include/setup.spthy new file mode 100644 index 0000000000000000000000000000000000000000..79031874c7f21e8549ad24b5fa0fb6ca1eb6563c --- /dev/null +++ b/include/setup.spthy @@ -0,0 +1,49 @@ +/* Key setup and Certificate model for all EAC models */ + + +functions: cert/3, cert_pk/1, cert_sig/1, cert_id/1, ca_sk/0 [private] +equations: cert_pk(cert(pk, s, id)) = pk, cert_sig(cert(pk, s, id)) = s, cert_id(cert(pk, s, id)) = id + +macros: verify_cert(cert, role) = verify(cert_sig(cert), <cert_pk(cert), cert_id(cert), role>, pk(ca_sk)) + + +rule Publish_ca_pk: + [ ] + --> + [ Out(pk(ca_sk)) ] + +// Generate long-term key pair for the chip. Classic version needs dh key pair +#ifdef CLASSIC +rule Generate_chip_key_pair: +let + pk = 'g'^~ltk +in + [ Fr(~ltk) ] + --[ TestMe() ]-> + [ !Pk($A, pk, 'chip'), !Ltk($A, ~ltk, 'chip'), Out(pk) ] +#else +rule Generate_chip_key_pair: +let + pk = pk(~ltk) +in + [ Fr(~ltk) ] + --> + [ !Pk($A, pk, 'chip'), !Ltk($A, ~ltk, 'chip'), Out(pk) ] +#endif + +// Generate static long-term key pair for the terminal. +rule Generate_terminal_key_pair: +let + pk = pk(~ltk) +in + [ Fr(~ltk) ] + --> + [ !Pk($A, pk, 'terminal'), !Ltk($A, ~ltk, 'terminal'), Out(pk) ] + +rule CA_Sign_ltk: +let + certA = cert(pk, sign(<pk, A, role>, ca_sk), A) +in + [ !Pk(A, pk, role) ] + --> + [ !Cert(A, certA, role), Out(certA) ]