diff --git a/BasicEAC.spthy b/BasicEAC.spthy new file mode 100644 index 0000000000000000000000000000000000000000..53250d1f6acf99f70d6cf038b9aefbff44f9b03a --- /dev/null +++ b/BasicEAC.spthy @@ -0,0 +1,242 @@ +/* +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 +