Add initial classical EAC model

BasicEAC.spthy

+/*
+EAC Protocol
+======================================
+
+Author:  Jonas Mueller
+Date:    November 2023
+
+*/
+
+theory BasicEAC
+begin
+
+builtins: signing, diffie-hellman
+functions: cert/3, cert_pk/1, cert_sig/1, cert_id/1, ca_sk/0 [private]
+functions: mac/2, kdf_mac/2, kdf_enc/2
+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) ]
+  -->
+    [ !Cert(A, certA), Out(certA) ]
+
+rule CA_Sign_dh:
+let
+    certA = cert(pk, sign(<pk, A>, ca_sk), A)
+in
+    [ !PkDH(A, pk) ]
+  -->
+    [ !CertDH(A, certA), Out(certA) ]
+
+
+/* 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(uid, k) ]
+  --[ Revealed(uid) ]->
+    [ Out(k) ]
+
+
+
+/* Terminal Authentication */
+// State machine: TA_INIT_T -> TA_CHALLENGE_C -> TA_RESPONSE_T -> TA_COMPLETE_C
+
+
+rule TA_INIT_T:
+let
+    pkTe = 'g'^~skTe
+    msg1 = <certT, pkTe, 'TA_INIT', '1', 't'>
+in
+    [ !Cert($T, certT), Fr(~skTe), Fr(~iid) ] // skTe is ephemeral session key, iid is instance id of user $T
+  -->
+    [ Out(msg1), TAInitT(<$T, ~iid>, ~skTe) ]
+
+// We generate a fresh IDc to simulate the previous execution of PACE or BAC
+rule TA_CHALLENGE_C:
+let
+    ca_pk = pk(ca_sk)
+    msg1 = <certT, pkTe, 'TA_INIT', '1', 't'>
+    msg2 = <~id_c, ~r1, 'TA_CHALLENGE', '2', 'c'>
+in
+    [ In(msg1), Fr(~r1), Fr(~id_c), Fr(~iid) ]
+  --[ Eq(verify_cert(certT), true) ]->
+    [ Out(msg2), TAChallengeC(<$C, ~iid>, certT, pkTe, ~id_c, ~r1) ]
+
+rule TA_RESPONSE_T:
+let
+    msg2 = <id_c, r1, 'TA_CHALLENGE', '2', 'c'>
+    pkTe = 'g'^skTe
+    s = sign(<id_c, r1, pkTe>, ~skT)
+    msg3 = <s, 'TA_RESPONSE', '3', 't'>
+in
+    [ In(msg2), TAInitT(<$T, iid>, skTe), !Ltk($T, ~skT) ]
+  -->
+    [ Out(msg3), TAResponseT(<$T, iid>, skTe, id_c) ]
+
+rule TA_COMPLETE_C:
+let
+    msg3 = <s, 'TA_RESPONSE', '3', 't'>
+in
+    [ In(msg3), TAChallengeC(<$C, iid>, certT, pkTe, id_c, r1) ]
+  --[ Eq(verify(s, <id_c, r1, pkTe>, cert_pk(certT)), true) ]->
+    [ TACompleteC(<$C, iid>, certT, pkTe, id_c, r1) ]
+
+
+
+/* Chip Authentication */
+// State machine: CA_INIT_C -> CA_INIT_T -> CA_FINISH_C -> CA_FINISH_T
+
+rule CA_INIT_C:
+let
+    msg4 = <certC, 'CA_INIT', '4', 'c'>
+in
+    [ !CertDH($C, certC), Fr(~r2), TACompleteC(<$C, iid>, certT, pkTe, id_c, r1) ]
+  -->
+    [ Out(msg4), CAInitC(<$C, iid>, certT, pkTe, id_c, r1, ~r2) ]
+
+
+rule CA_INIT_T:
+let
+    pkTe = 'g'^skTe
+    msg4 = <certC, 'CA_INIT', '4', 'c'>
+    msg5 = <pkTe, 'CA_COMMIT', '5', 't'>
+in
+    [ In(msg4), TAResponseT(<$T, iid>, skTe, id_c) ]
+  --[ Eq(verify_cert(certC), true) ]->
+    [ Out(msg5), CAInitT(<$T, iid>, skTe, id_c, certC) ]
+
+
+rule CA_FINISH_C:
+let 
+    msg5 = <pkTe_t, 'CA_COMMIT', '5', 't'>
+    k = pkTe^~skC
+    kMac = kdf_mac(k, r2)
+    kEnc = kdf_enc(k, r2)
+    tag = mac(kMac, pkTe)
+    msg6 = <r2, tag, 'CA_RESPONSE', '6', 'c'>
+    sid = <pkTe, pkC, id_c, r2>
+in
+    [ In(msg5), CAInitC(<$C, iid>, certT, pkTe, id_c, r1, r2), !LtkDH($C, ~skC), !PkDH($C, pkC) ]
+  --[ Eq(pkTe_t, pkTe), Completed(<kEnc, kMac>, sid, $C, 'chip', cert_id(certT)) ]->
+    [ Out(msg6), CAFinishC($C, cert_id(certT), kEnc), Out(iid) ]
+
+
+rule CA_FINISH_T:
+let
+    msg6 = <r2, tag, 'CA_RESPONSE', '6', 'c'>
+    pkTe = 'g'^skTe
+    k = cert_pk(certC)^skTe
+    kMac = kdf_mac(k, r2)
+    kEnc = kdf_enc(k, r2)
+    sid = <pkTe, cert_pk(certC), id_c, r2>
+in
+    [ In(msg6), CAInitT(<$T, iid>, skTe, id_c, certC) ]
+  --[ Eq(mac(kMac, pkTe), tag), Completed(<kEnc, kMac>, sid, $T, 'terminal', cert_id(certC)), Finished(sid) ]->
+    [ CAFinishT(cert_id(certC), $T, kEnc), !SessionReveal(<$T, iid>, skTe), Out(iid) ]
+
+
+
+
+restriction Equality:
+    "All x y #i. Eq(x, y) @ i ==> x = y"
+
+// Correctness
+
+/*
+lemma session_exist: exists-trace
+  " Ex C T k sid #i #j.
+     Completed(k, sid, C, 'chip', T) @ #i
+     & Completed(k, sid, T, 'terminal', C) @ #j
+     & #i < #j
+  "
+
+lemma two_session_exist: exists-trace
+  " Ex C T k k2 sid sid2 #i #j #i2 #j2.
+     Completed(k, sid, C, 'chip', T) @ #i
+     & Completed(k, sid, T, 'terminal', C) @ #j
+     & #i < #j
+     & Completed(k2, sid2, C, 'chip', T) @ #i2
+     & Completed(k2, sid2, T, 'terminal', C) @ #j2
+     & #i2 < #j2
+     & not(k=k2)
+  "
+*/
+
+// Authentication
+lemma aliveness:
+  "All k sid A role B #i #t .
+    Completed(k, sid, A, role, B) @ #i
+    & Finished(sid) @ #t
+    & not(Ex #k . Corrupted(B) @ #k)
+    ==> (Ex k2 sid2 role2 C #j .
+        Completed(k2, sid2, B, role2, C) @ #j)
+  "
+
+lemma session_uniqueness:
+  "All A B k sid sid2 role #i #j .
+    Completed(k, sid, A, role, B) @ #i
+    & Completed(k, sid2, A, role, B) @ #j
+    ==> (#i = #j)
+  "
+
+lemma consistency:
+  "All C T k k2 sid #i #j .
+    Completed(k, sid, C, 'chip', T) @ #i
+    & Completed(k2, sid, T, 'terminal', C) @ #j
+    & not(Ex #k . Corrupted(C) @ #k)
+    & not(Ex #k . Corrupted(T) @ #k)
+    ==> (k=k2)
+  "
+
+// Key secrecy
+lemma key_secrecy[reuse]:
+  "All C T role k sid #j .
+    Completed(k, sid, C, role, T) @ #j
+    & not(Ex #m . Corrupted(T) @ #m)
+    & not(Ex #m . Corrupted(C) @ #m)
+    & not(Ex iid #m . Revealed(<T, iid>) @ #m)
+    & not(Ex iid #m . Revealed(<C, iid>) @ #m)
+    ==> not(Ex #m . K(k) @ #m)
+  "
+
+end
+