Skip to content
Snippets Groups Projects
Commit 856dd764 authored by Müller, Jonas's avatar Müller, Jonas
Browse files

Add all variants and python script to insert lemmas

parent de79838b
No related branches found
No related tags found
No related merge requests found
Show whitespace changes
Inline Side-by-side
BasicEAC.spthy → ClassicEAC.spthy
+ 190
− 0
View file @ 856dd764
/*
EAC Protocol
Classic EAC Protocol in tamarin
======================================
Author: Jonas Mueller
......@@ -7,12 +7,13 @@ Date: November 2023
*/
theory BasicEAC
theory ClassicEAC
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
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))
......@@ -47,7 +48,7 @@ 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:
......@@ -55,7 +56,7 @@ let
certA = cert(pk, sign(<pk, A>, ca_sk), A)
in
[ !PkDH(A, pk) ]
-->
--[ Registered(A) ]->
[ !CertDH(A, certA), Out(certA) ]
......@@ -72,8 +73,8 @@ rule Reveal_dh:
[ Out(ltk) ]
rule Reveal_session:
[ !SessionReveal(uid, k) ]
--[ Revealed(uid) ]->
[ !SessionReveal(sid, k) ]
--[ Revealed(sid) ]->
[ Out(k) ]
......@@ -85,7 +86,7 @@ rule Reveal_session:
rule TA_INIT_T:
let
pkTe = 'g'^~skTe
msg1 = <certT, pkTe, 'TA_INIT', '1', 't'>
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
-->
......@@ -94,9 +95,8 @@ in
// 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'>
msg1 = <certT, pkTe, '1', 't'>
msg2 = <~id_c, ~r1, '2', 'c'>
in
[ In(msg1), Fr(~r1), Fr(~id_c), Fr(~iid) ]
--[ Eq(verify_cert(certT), true) ]->
......@@ -104,18 +104,18 @@ in
rule TA_RESPONSE_T:
let
msg2 = <id_c, r1, 'TA_CHALLENGE', '2', 'c'>
msg2 = <id_c, r1, '2', 'c'>
pkTe = 'g'^skTe
s = sign(<id_c, r1, pkTe>, ~skT)
msg3 = <s, 'TA_RESPONSE', '3', 't'>
msg3 = <s, '3', 't'>
in
[ In(msg2), TAInitT(<$T, iid>, skTe), !Ltk($T, ~skT) ]
-->
--[ Computed($T, 'terminal', s) ]->
[ Out(msg3), TAResponseT(<$T, iid>, skTe, id_c) ]
rule TA_COMPLETE_C:
let
msg3 = <s, 'TA_RESPONSE', '3', 't'>
msg3 = <s, '3', 't'>
in
[ In(msg3), TAChallengeC(<$C, iid>, certT, pkTe, id_c, r1) ]
--[ Eq(verify(s, <id_c, r1, pkTe>, cert_pk(certT)), true), CompletedTA($C, iid, cert_id(certT)) ]->
......@@ -128,7 +128,7 @@ in
rule CA_INIT_C:
let
msg4 = <certC, 'CA_INIT', '4', 'c'>
msg4 = <certC, '4', 'c'>
in
[ !CertDH($C, certC), Fr(~r2), TACompleteC(<$C, iid>, certT, pkTe, id_c, r1) ]
-->
......@@ -138,8 +138,8 @@ in
rule CA_INIT_T:
let
pkTe = 'g'^skTe
msg4 = <certC, 'CA_INIT', '4', 'c'>
msg5 = <pkTe, 'CA_COMMIT', '5', 't'>
msg4 = <certC, '4', 'c'>
msg5 = <pkTe, '5', 't'>
in
[ In(msg4), TAResponseT(<$T, iid>, skTe, id_c) ]
--[ Eq(verify_cert(certC), true) ]->
......@@ -148,161 +148,43 @@ in
rule CA_FINISH_C:
let
msg5 = <pkTe_t, 'CA_COMMIT', '5', 't'>
msg5 = <pkTe_t, '5', 't'>
k = pkTe^~skC
kMac = kdf_mac(k, r2)
kEnc = kdf_enc(k, r2)
tag = mac(pkTe, kMac)
msg6 = <r2, tag, 'CA_RESPONSE', '6', 'c'>
sid = <certT, certC, pkTe, 'g'^~skC, id_c, r2, k>
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) ]
--[ Eq(pkTe_t, pkTe), Completed(<kEnc, kMac>, sid, $C, 'chip', cert_id(certT)) ]->
--[ 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) ]
rule CA_FINISH_T:
let
msg6 = <r2, tag, 'CA_RESPONSE', '6', 'c'>
msg6 = <r2, tag, '6', 'c'>
pkTe = 'g'^skTe
pkC = cert_pk(certC)
k = pkC^skTe
kMac = kdf_mac(k, r2)
kEnc = kdf_enc(k, r2)
tag_T = mac(pkTe, kMac)
sid = <certT, certC, pkTe, pkC, id_c, r2, k>
sid = <certT, certC, pkTe, pkC, id_c, r2>
in
[ In(msg6), CAInitT(<$T, iid>, skTe, id_c, certC), !Cert($T, certT) ]
--[ Eq(tag, tag_T), Completed(<kEnc, kMac>, sid, $T, 'terminal', cert_id(certC)), Finished(sid) ]->
[ CAFinishT(cert_id(certC), $T, kEnc), !SessionReveal(<$T, iid>, skTe) ]
--[ 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"
// 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)
"
*/
// Agreement
lemma weak_agreement_C:
"All k sid C T #i #t .
Completed(k, sid, C, 'chip', T) @ #i
& Finished(sid) @ #t
==> (Ex k2 sid2 #j .
Completed(k2, sid2, T, 'terminal', C) @ #j)
| (Ex #k . Corrupted(C) @ #k)
| (Ex #k . Corrupted(T) @ #k)
"
lemma weak_agreement_T:
"All k sid C T #i #t .
Completed(k, sid, T, 'terminal', C) @ #i
& Finished(sid) @ #t
==> (Ex k2 sid2 #j .
Completed(k2, sid2, C, 'chip', T) @ #j)
| (Ex #k . Corrupted(C) @ #k)
| (Ex #k . Corrupted(T) @ #k)
"
lemma agreement_C:
"All k sid C T #i #t .
Completed(k, sid, C, 'chip', T) @ #i
& Finished(sid) @ #t
==> (Ex #j .
Completed(k, sid, T, 'terminal', C) @ #j)
| (Ex #k . Corrupted(C) @ #k)
| (Ex #k . Corrupted(T) @ #k)
"
lemma agreement_T:
"All k sid C T #i #t .
Completed(k, sid, T, 'terminal', C) @ #i
& Finished(sid) @ #t
==> (Ex #j .
Completed(k, sid, C, 'chip', T) @ #j)
| (Ex #k . Corrupted(C) @ #k)
| (Ex #k . Corrupted(T) @ #k)
"
/*
lemma aliveness:
"All k sid A role B #i #t .
Completed(k, sid, A, role, B) @ #i
& Finished(sid) @ #t
==> (Ex k2 sid2 role2 C #j .
Completed(k2, sid2, B, role2, C) @ #j)
| (Ex #k . Corrupted(B) @ #k)
"
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) & (sid = sid2)
"
// Sole purpose of static key of T is authentication
// The final keys k/k2 are only derived from pkC/skC, pkTe/skTe and r2
lemma consistency:
"All C T k k2 sid #i #j .
Completed(k, sid, C, 'chip', T) @ #i
& Completed(k2, sid, T, 'terminal', C) @ #j
==> (k=k2)
| (Ex #m . Corrupted(C) @ #m)
"
// Key secrecy
lemma key_secrecy:
"All C T k sid #i #j .
Completed(k, sid, C, 'chip', T) @ #i
& Completed(k, sid, T, 'terminal', C) @ #j
==> not(Ex #m . K(k) @ #m)
| (Ex iid #m . Revealed(<T, iid>) @ #m)
| (Ex #m . Corrupted(C) @ #m)
"
// Cannot track chip after TA
lemma chip_hiding:
"All C T iid #i .
CompletedTA(C, iid, T) @ #i
==> not(Ex #m . K(iid) @ #m)
| (Ex #m . (K(iid) @ #m & #i < #m))
"
// Perfect forward secrecy
lemma pfs:
"All A k sid role B #i #j .
Corrupted(A) @ #i
& Completed(k, sid, A, role, B) @ #j
& #j < #i
==> not(Ex #m . K(k) @ #m)
| (Ex #m . (Corrupted(A) @ #m & #m < #j))
| (Ex #m . Corrupted(B) @ #m)
| (Ex iid #m . Revealed(<B, iid>) @ #m)
| (Ex iid #m . Revealed(<A, iid>) @ #m)
"
*/
insert(lemmas.spthy)
end
FastKemPQEAC.spthy 0 → 100644
+ 210
− 0
View file @ 856dd764
/*
PQ-EAC with Terminal Authentication through Long-Term KEM with reduced round-trip
======================================
Author: Jonas Mueller
Date: May 2024
*/
theory FastKemPQEAC
begin
builtins: signing, symmetric-encryption
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))
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) ]
/* Terminal Authentication */
// State machine: TA_INIT_T -> TA_CHALLENGE_C -> TA_RESPONSE_T -> TA_COMPLETE_C
rule TA_INIT_T:
let
msg1 = <certT, '1', 't'>
in
[ !Cert($T, certT), Fr(~iid) ]
-->
[ Out(msg1), Out(~iid), TAInitT(<$T, ~iid>) ]
#ifdef PFS
rule TA_CHALLENGE_C:
let
msg1 = <certT, '1', 't'>
cTA = encaps(~kTA, cert_pk(certT))
kTMAC = kdf(<'TMAC', ~r1>, ~kTA)
kTENC = kdf(<'TENC', ~r1>, ~kTA)
kTCNF = kdf(<'TCNF', ~r1>, ~kTA)
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) ]->
[ Out(msg2), Out(~iid), TAChallengeC(<$C, ~iid>, certT, ~id_c, ~r1, ~r2, ~skCe, kTMAC, kTCNF) ]
#else
rule TA_CHALLENGE_C:
let
msg1 = <certT, '1', 't'>
cTA = encaps(~kTA, cert_pk(certT))
kTMAC = kdf(<'TMAC', ~r1>, ~kTA)
kTENC = kdf(<'TENC', ~r1>, ~kTA)
kTCNF = kdf(<'TCNF', ~r1>, ~kTA)
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) ]->
[ Out(msg2), Out(~iid), TAChallengeC(<$C, ~iid>, certT, ~id_c, ~r1, ~r2, kTMAC, kTCNF) ]
#endif
#ifdef PFS
rule TA_RESPONSE_T:
let
msg2 = <id_c, r1, cTA, cCA, '2', 'c'>
kTA = decaps(cTA, ~skT)
kTMAC = kdf(<'TMAC', r1>, kTA)
kTENC = kdf(<'TENC', r1>, kTA)
kTCNF = kdf(<'TCNF', r1>, kTA)
dmesg = sdec(cCA, kTENC)
certC = fst(dmesg)
r2 = fst(snd(dmesg))
pkCe = snd(snd(dmesg))
pkC = cert_pk(certC)
cip = encaps(~k, pkC)
cipe = encaps(~ke, pkCe)
sid = <certT, certC, r2, cip, pkCe, cipe>
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) ]->
[ Out(msg3), TAResponseT(<$T, iid>, id_c, certC, r2, <~k, cip>, <~ke, cipe>, pkCe) ]
#else
rule TA_RESPONSE_T:
let
msg2 = <id_c, r1, cTA, cCA, '2', 'c'>
kTA = decaps(cTA, ~skT)
kTMAC = kdf(<'TMAC', r1>, kTA)
kTENC = kdf(<'TENC', r1>, kTA)
kTCNF = kdf(<'TCNF', r1>, kTA)
dmesg = sdec(cCA, kTENC)
certC = fst(dmesg)
r2 = snd(dmesg)
pkC = cert_pk(certC)
cip = encaps(~k, pkC)
sid = <certT, certC, r2, cip>
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) ]->
[ Out(msg3), TAResponseT(<$T, iid>, id_c, certC, r2, <~k, cip>) ]
#endif
#ifdef PFS
rule TA_COMPLETE_C:
let
msg3 = <kTCNF_T, cip, s, cipe, '3', 't'>
sid = <certT, certC, r2, cip, pk(skCe), cipe>
k = decaps(cip, ~skC)
ke = decaps(cipe, skCe)
kCNF = kdf(<'CNF', sid>, <k, ke>)
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) ]
--[ 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
rule TA_COMPLETE_C:
let
msg3 = <kTCNF_T, cip, s, '3', 't'>
sid = <certT, certC, r2, cip>
k = decaps(cip, ~skC)
kCNF = kdf(<'CNF', sid>, k)
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) ]
--[ 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
#ifdef PFS
rule CA_FINISH_T:
let
msg4 = <kCNF_C, '4', 'c'>
sid = <certT, certC, r2, cip, pkCe, cipe>
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) ]
--[ Eq(kCNF, kCNF_C), Completed(kKEY, sid, $T, 'terminal', cert_id(certC)), Finished(sid) ]->
[ CAFinishT(cert_id(certC), $T, kKEY), !SessionReveal(sid, kKEY) ]
#else
rule CA_FINISH_T:
let
msg4 = <kCNF_C, '4', 'c'>
sid = <certT, certC, r2, cip>
kCNF = kdf(<'CNF', sid>, k)
kKEY = kdf(<'KEY', sid>, k)
in
[ In(msg4), TAResponseT(<$T, iid>, id_c, certC, r2, <k, cip>), !Cert($T, certT) ]
--[ 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)
end
FastSigPQEAC.spthy 0 → 100644
+ 186
− 0
View file @ 856dd764
/*
PQ-EAC with Terminal Signatures and reduced round-trip
======================================
Author: Jonas Mueller
Date: May 2024
*/
theory FastSigPQEAC
begin
builtins: signing
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))
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) ]
/* Terminal Authentication */
// State machine: TA_INIT_T -> TA_CHALLENGE_C -> TA_RESPONSE_T -> TA_COMPLETE_C
rule TA_INIT_T:
let
msg1 = <certT, '1', 't'>
in
[ !Cert($T, certT), Fr(~iid) ]
-->
[ Out(msg1), Out(~iid), TAInitT(<$T, ~iid>) ]
#ifdef PFS
rule TA_CHALLENGE_C:
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) ]->
[ Out(msg2), Out(~iid), TAChallengeC(<$C, ~iid>, certT, ~id_c, ~r1, ~skCe, ~r2) ]
#else
rule TA_CHALLENGE_C:
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) ]->
[ Out(msg2), Out(~iid), TAChallengeC(<$C, ~iid>, certT, ~id_c, ~r1, ~r2) ]
#endif
#ifdef PFS
rule TA_RESPONSE_T:
let
msg2 = <id_c, r1, certC, r2, pkCe, '2', 'c'>
s1 = sign(<'TA', id_c, r1>, ~skT)
pkC = cert_pk(certC)
cip = encaps(~k, pkC)
cipe = encaps(~ke, pkCe)
sid = <certT, certC, r2, cip, pkCe, cipe>
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) ]->
[ Out(msg3), CAInitT(<$T, iid>, id_c, certC, r2, <~k, cip>, <~ke, cipe>, pkCe) ]
#else
rule TA_RESPONSE_T:
let
msg2 = <id_c, r1, certC, r2, '2', 'c'>
s1 = sign(<'TA', id_c, r1>, ~skT)
pkC = cert_pk(certC)
cip = encaps(~k, pkC)
sid = <certT, certC, r2, cip>
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) ]->
[ Out(msg3), CAInitT(<$T, iid>, id_c, certC, r2, <~k, cip>) ]
#endif
#ifdef PFS
rule TA_COMPLETE_C:
let
msg3 = <cip, cipe, s1, s2, '3', 't'>
sid = <certT, certC, r2, cip, pk(skCe), cipe>
k = decaps(cip, ~skC)
ke = decaps(cipe, skCe)
kCNF = kdf(<'CNF', sid>, <k, ke>)
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) ]
--[ 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
rule TA_COMPLETE_C:
let
msg3 = <cip, s1, s2, '3', 't'>
sid = <certT, certC, r2, cip>
k = decaps(cip, ~skC)
kCNF = kdf(<'CNF', sid>, k)
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) ]
--[ 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
#ifdef PFS
rule CA_FINISH_T:
let
msg4 = <kCNF_C, '4', 'c'>
sid = <certT, certC, r2, cip, pkCe, cipe>
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) ]
--[ Eq(kCNF, kCNF_C), Completed(kKEY, sid, $T, 'terminal', cert_id(certC)), Finished(sid) ]->
[ CAFinishT(cert_id(certC), $T, kKEY), !SessionReveal(sid, kKEY) ]
#else
rule CA_FINISH_T:
let
msg4 = <kCNF_C, '4', 'c'>
sid = <certT, certC, r2, cip>
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) ]
--[ 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)
end
InsertLemmas.py 0 → 100644
+ 13
− 0
View file @ 856dd764
import sys, re
pattern = re.compile(r"insert\((.*)\)")
out = open('tmp.spthy', 'w')
for i, line in enumerate(open(sys.argv[1])):
match = re.search(pattern, line)
if match:
for line in open(match.group(1)):
out.write(line)
else:
out.write(line)
KemPQEAC.spthy 0 → 100644
+ 233
− 0
View file @ 856dd764
/*
PQ-EAC with Terminal Authentication through Long-Term KEM
======================================
Author: Jonas Mueller
Date: May 2024
*/
theory KemPQEAC
begin
builtins: signing, symmetric-encryption
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))
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) ]
/* Terminal Authentication */
// State machine: TA_INIT_T -> TA_CHALLENGE_C -> TA_RESPONSE_T -> TA_COMPLETE_C
rule TA_INIT_T:
let
msg1 = <certT, '1', 't'>
in
[ !Cert($T, certT), Fr(~iid) ]
-->
[ Out(msg1), Out(~iid), TAInitT(<$T, ~iid>) ]
// We generate a fresh IDc to simulate the previous execution of PACE or BAC
rule TA_CHALLENGE_C:
let
msg1 = <certT, '1', 't'>
cTA = encaps(~kTA, cert_pk(certT))
msg2 = <~id_c, ~r1, cTA, '2', 'c'>
in
[ In(msg1), Fr(~r1), Fr(~id_c), Fr(~kTA), Fr(~iid) ]
--[ Eq(verify_cert(certT), true) ]->
[ Out(msg2), TAChallengeC(<$C, ~iid>, certT, ~id_c, ~r1, <~kTA, cTA>) ]
rule TA_RESPONSE_T:
let
msg2 = <id_c, r1, cTA, '2', 'c'>
kTA = decaps(cTA, ~skT)
kTMAC = kdf(<'TMAC', r1>, kTA)
kTENC = kdf(<'TENC', r1>, kTA)
kTCNF = kdf(<'TCNF', r1>, kTA)
msg3 = <kTCNF, '3', 't'>
in
[ In(msg2), TAInitT(<$T, iid>), !Ltk($T, ~skT) ]
-->
[ Out(msg3), TAResponseT(<$T, iid>, id_c, kTMAC, kTENC) ]
rule TA_COMPLETE_C:
let
msg3 = <kTCNF_T, '3', 't'>
kTMAC = kdf(<'TMAC', r1>, kTA)
kTENC = kdf(<'TENC', r1>, kTA)
kTCNF = kdf(<'TCNF', r1>, kTA)
in
[ In(msg3), TAChallengeC(<$C, iid>, certT, id_c, r1, <kTA, cTA>) ]
--[ Eq(kTCNF_T, kTCNF), CompletedTA($C, iid, cert_id(certT)) ]->
[ TACompleteC(<$C, iid>, certT, id_c, r1, <kTA, cTA>, kTMAC, kTENC) ]
/* Chip Authentication */
// State machine: CA_INIT_C -> CA_INIT_T -> CA_FINISH_C -> CA_FINISH_T
#ifdef PFS
rule CA_INIT_C:
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) ]
-->
[ Out(msg4), Out(iid), CAInitC(<$C, iid>, certT, id_c, r1, <kTA, cTA>, kTMAC, kTENC, ~r2, ~skCe) ]
#else
rule CA_INIT_C:
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) ]
-->
[ Out(msg4), Out(iid), CAInitC(<$C, iid>, certT, id_c, r1, <kTA, cTA>, kTMAC, kTENC, ~r2) ]
#endif
#ifdef PFS
rule CA_INIT_T:
let
msg4 = <cCA, '4', 'c'>
dmesg = sdec(cCA, kTENC)
certC = fst(dmesg)
r2 = fst(snd(dmesg))
pkCe = snd(snd(dmesg))
pkC = cert_pk(certC)
cip = encaps(~k, pkC)
cipe = encaps(~ke, pkCe)
sid = <certT, certC, r2, cip, pkCe, cipe>
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) ]->
[ Out(msg5), CAInitT(<$T, iid>, id_c, kTMAC, kTENC, certC, r2, <~k, cip>, <~ke, cipe>, pkCe) ]
#else
rule CA_INIT_T:
let
msg4 = <cCA, 'CA_INIT', '4', 'c'>
dmesg = sdec(cCA, kTENC)
certC = fst(dmesg)
r2 = snd(dmesg)
pkC = cert_pk(certC)
cip = encaps(~k, pkC)
sid = <certT, certC, r2, cip>
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) ]->
[ Out(msg5), CAInitT(<$T, iid>, id_c, kTMAC, kTENC, certC, r2, <~k, cip>) ]
#endif
#ifdef PFS
rule CA_FINISH_C:
let
msg5 = <cip, s, cipe, '5', 't'>
sid = <certT, certC, r2, cip, pk(skCe), cipe>
k = decaps(cip, ~skC)
ke = decaps(cipe, skCe)
kCNF = kdf(<'CNF', sid>, <k, ke>)
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) ]
--[ Eq(s, mac(<'CA', sid>, kTMAC)), Completed(kKEY, sid, $C, 'chip', cert_id(certT)) ]->
[ Out(msg6), CAFinishC($C, cert_id(certT), kKEY) ]
#else
rule CA_FINISH_C:
let
msg5 = <cip, s, '5', 't'>
sid = <certT, certC, r2, cip>
k = decaps(cip, ~skC)
kCNF = kdf(<'CNF', sid>, k)
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) ]
--[ Eq(s, mac(<'CA', sid>, kTMAC)), Completed(kKEY, sid, $C, 'chip', cert_id(certT)) ]->
[ Out(msg6), CAFinishC($C, cert_id(certT), kKEY) ]
#endif
#ifdef PFS
rule CA_FINISH_T:
let
msg6 = <kCNF_c, '6', 'c'>
sid = <certT, certC, r2, cip, pkCe, cipe>
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) ]
--[ Eq(kCNF, kCNF_c), Completed(kKEY, sid, $T, 'terminal', cert_id(certC)), Finished(sid) ]->
[ CAFinishT(cert_id(certC), $T, kKEY), !SessionReveal(sid, kKEY) ]
#else
rule CA_FINISH_T:
let
msg6 = <kCNF_c, '6', 'c'>
sid = <certT, certC, r2, cip>
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) ]
--[ 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)
end
SigPQEAC.spthy 0 → 100644
+ 217
− 0
View file @ 856dd764
/*
PQ-EAC with Terminal Signatures
======================================
Author: Jonas Mueller
Date: May 2024
*/
theory SigPQEAC
begin
builtins: signing
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))
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) ]
/* Terminal Authentication */
// State machine: TA_INIT_T -> TA_CHALLENGE_C -> TA_RESPONSE_T -> TA_COMPLETE_C
rule TA_INIT_T:
let
msg1 = <certT, '1', 't'>
in
[ !Cert($T, certT), Fr(~iid) ]
-->
[ Out(msg1), Out(~iid), TAInitT(<$T, ~iid>) ]
// We generate a fresh IDc to simulate the previous execution of PACE or BAC
rule TA_CHALLENGE_C:
let
msg1 = <certT, '1', 't'>
msg2 = <~id_c, ~r1, '2', 'c'>
in
[ In(msg1), Fr(~r1), Fr(~id_c), Fr(~iid) ]
--[ Eq(verify_cert(certT), true) ]->
[ Out(msg2), TAChallengeC(<$C, ~iid>, certT, ~id_c, ~r1) ]
rule TA_RESPONSE_T:
let
msg2 = <id_c, r1, '2', 'c'>
s = sign(<'TA', id_c, r1>, ~skT)
msg3 = <s, '3', 't'>
in
[ In(msg2), TAInitT(<$T, iid>), !Ltk($T, ~skT) ]
-->
[ Out(msg3), TAResponseT(<$T, iid>, id_c) ]
rule TA_COMPLETE_C:
let
msg3 = <s, '3', 't'>
in
[ In(msg3), TAChallengeC(<$C, iid>, certT, id_c, r1) ]
--[ Eq(verify(s, <'TA', id_c, r1>, cert_pk(certT)), true), CompletedTA($C, iid, cert_id(certT)) ]->
[ TACompleteC(<$C, iid>, certT, id_c, r1) ]
/* Chip Authentication */
// State machine: CA_INIT_C -> CA_INIT_T -> CA_FINISH_C -> CA_FINISH_T
#ifdef PFS
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) ]
-->
[ Out(msg4), Out(iid), CAInitC(<$C, iid>, certT, id_c, r1, ~r2, ~skCe) ]
#else
rule CA_INIT_C:
let
msg4 = <certC, ~r2, '4', 'c'>
in
[ Fr(~r2), TACompleteC(<$C, iid>, certT, id_c, r1), !Cert($C, certC) ]
-->
[ Out(msg4), Out(iid), CAInitC(<$C, iid>, certT, id_c, r1, ~r2) ]
#endif
#ifdef PFS
rule CA_INIT_T:
let
msg4 = <certC, r2, pkCe, '4', 'c'>
pkC = cert_pk(certC)
cip = encaps(~k, pkC)
cipe = encaps(~ke, pkCe)
sid = <certT, certC, r2, cip, pkCe, cipe>
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) ]->
[ Out(msg5), CAInitT(<$T, iid>, id_c, certC, r2, <~k, cip>, <~ke, cipe>, pkCe) ]
#else
rule CA_INIT_T:
let
msg4 = <certC, r2, '4', 'c'>
pkC = cert_pk(certC)
cip = encaps(~k, pkC)
sid = <certT, certC, r2, cip>
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) ]->
[ Out(msg5), CAInitT(<$T, iid>, id_c, certC, r2, <~k, cip>) ]
#endif
#ifdef PFS
rule CA_FINISH_C:
let
msg5 = <cip, s, cipe, '5', 't'>
sid = <certT, certC, r2, cip, pk(skCe), cipe>
k = decaps(cip, ~skC)
ke = decaps(cipe, skCe)
kCNF = kdf(<'CNF', sid>, <k, ke>)
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) ]
--[ 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
rule CA_FINISH_C:
let
msg5 = <cip, s, '5', 't'>
sid = <certT, certC, r2, cip>
k = decaps(cip, ~skC)
kCNF = kdf(<'CNF', sid>, k)
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) ]
--[ 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
#ifdef PFS
rule CA_FINISH_T:
let
msg6 = <kCNF_C, '6', 'c'>
sid = <certT, certC, r2, cip, pkCe, cipe>
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) ]
--[ Eq(kCNF, kCNF_C), Completed(kKEY, sid, $T, 'terminal', cert_id(certC)), Finished(sid) ]->
[ CAFinishT(cert_id(certC), $T, kKEY), !SessionReveal(sid, kKEY) ]
#else
rule CA_FINISH_T:
let
msg6 = <kCNF_c, '6', 'c'>
sid = <certT, certC, r2, cip>
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) ]
--[ 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)
end
lemmas.spthy 0 → 100644
+ 126
− 0
View file @ 856dd764
// 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)
"
// Agreement
lemma weak_agreement_C:
"All k sid C T #i #t .
Completed(k, sid, C, 'chip', T) @ #i
& Finished(sid) @ #t
==> (Ex k2 sid2 #j .
Completed(k2, sid2, T, 'terminal', C) @ #j)
| (Ex #k . Corrupted(C) @ #k)
| (Ex #k . Corrupted(T) @ #k)
"
lemma weak_agreement_T:
"All k sid C T #i #t .
Completed(k, sid, T, 'terminal', C) @ #i
& Finished(sid) @ #t
==> (Ex k2 sid2 #j .
Completed(k2, sid2, C, 'chip', T) @ #j)
| (Ex #k . Corrupted(C) @ #k)
| (Ex #k . Corrupted(T) @ #k)
"
lemma agreement_C:
"All k sid C T #i #t .
Completed(k, sid, C, 'chip', T) @ #i
& Finished(sid) @ #t
==> (Ex #j .
Completed(k, sid, T, 'terminal', C) @ #j)
| (Ex #k . Corrupted(C) @ #k)
| (Ex #k . Corrupted(T) @ #k)
"
lemma agreement_T:
"All k sid C T #i #t .
Completed(k, sid, T, 'terminal', C) @ #i
& Finished(sid) @ #t
==> (Ex #j .
Completed(k, sid, C, 'chip', T) @ #j)
| (Ex #k . Corrupted(C) @ #k)
| (Ex #k . Corrupted(T) @ #k)
"
lemma aliveness:
"All k sid A role B #i #t .
Completed(k, sid, A, role, B) @ #i
& Finished(sid) @ #t
==> (Ex k2 sid2 role2 C #j .
Completed(k2, sid2, B, role2, C) @ #j)
| (Ex #k . Corrupted(B) @ #k)
"
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) & (sid = sid2)
"
// Sole purpose of static key of T is authentication
// The final keys k/k2 are only derived from pkC/skC, pkTe/skTe and r2
lemma consistency:
"All C T k k2 sid #i #j .
Completed(k, sid, C, 'chip', T) @ #i
& Completed(k2, sid, T, 'terminal', C) @ #j
==> (k=k2)
| (Ex #m . Corrupted(C) @ #m)
"
// Key secrecy
lemma key_secrecy:
"All C T k sid #i #j .
Completed(k, sid, C, 'chip', T) @ #i
& Completed(k, sid, T, 'terminal', C) @ #j
==> not(Ex #m . K(k) @ #m)
| (Ex #m . Revealed(sid) @ #m)
| (Ex #m . Corrupted(C) @ #m)
"
// Cannot track chip before CA
lemma chip_hiding:
"All C T iid #i .
CompletedTA(C, iid, T) @ #i
==> not(Ex #m . K(iid) @ #m)
| (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))
"
*/
// Perfect forward secrecy
lemma pfs:
"All C T k sid #i #j .
Completed(k, sid, C, 'chip', T) @ #i
& Completed(k, sid, T, 'terminal', C) @ #j
& not(Ex #m . Corrupted(C) @ #m & #m < #j)
& not(Ex #m . Corrupted(T) @ #m & #m < #j)
==> (not(Ex #m . K(k) @ #m)
| (Ex #m . Revealed(sid) @ #m))
"
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment