Theory KerberosIV
section‹The Kerberos Protocol, Version IV›
theory KerberosIV imports Public begin
text‹The "u" prefix indicates theorems referring to an updated version of the protocol. The "r" suffix indicates theorems where the confidentiality assumptions are relaxed by the corresponding arguments.›
abbreviation
Kas :: agent where "Kas == Server"
abbreviation
Tgs :: agent where "Tgs == Friend 0"
axiomatization where
Tgs_not_bad [iff]: "Tgs ∉ bad"
definition
authKeys :: "event list ⇒ key set" where
"authKeys evs = {authK. ∃A Peer Ta. Says Kas A
(Crypt (shrK A) ⦃Key authK, Agent Peer, Number Ta,
(Crypt (shrK Peer) ⦃Agent A, Agent Peer, Key authK, Number Ta⦄)
⦄) ∈ set evs}"
definition
Issues :: "[agent, agent, msg, event list] ⇒ bool"
("_ Issues _ with _ on _" [50, 0, 0, 50] 50) where
"(A Issues B with X on evs) =
(∃Y. Says A B Y ∈ set evs ∧ X ∈ parts {Y} ∧
X ∉ parts (spies (takeWhile (λz. z ≠ Says A B Y) (rev evs))))"
definition
before :: "[event, event list] ⇒ event list" ("before _ on _" [0, 50] 50)
where "(before ev on evs) = takeWhile (λz. z ≠ ev) (rev evs)"
definition
Unique :: "[event, event list] ⇒ bool" ("Unique _ on _" [0, 50] 50)
where "(Unique ev on evs) = (ev ∉ set (tl (dropWhile (λz. z ≠ ev) evs)))"
consts
authKlife :: nat
servKlife :: nat
authlife :: nat
replylife :: nat
specification (authKlife)
authKlife_LB [iff]: "2 ≤ authKlife"
by blast
specification (servKlife)
servKlife_LB [iff]: "2 + authKlife ≤ servKlife"
by blast
specification (authlife)
authlife_LB [iff]: "Suc 0 ≤ authlife"
by blast
specification (replylife)
replylife_LB [iff]: "Suc 0 ≤ replylife"
by blast
abbreviation
CT :: "event list ⇒ nat" where
"CT == length"
abbreviation
expiredAK :: "[nat, event list] ⇒ bool" where
"expiredAK Ta evs == authKlife + Ta < CT evs"
abbreviation
expiredSK :: "[nat, event list] ⇒ bool" where
"expiredSK Ts evs == servKlife + Ts < CT evs"
abbreviation
expiredA :: "[nat, event list] ⇒ bool" where
"expiredA T evs == authlife + T < CT evs"
abbreviation
valid :: "[nat, nat] ⇒ bool" ("valid _ wrt _" [0, 50] 50) where
"valid T1 wrt T2 == T1 ≤ replylife + T2"
definition AKcryptSK :: "[key, key, event list] ⇒ bool" where
"AKcryptSK authK servK evs ==
∃A B Ts.
Says Tgs A (Crypt authK
⦃Key servK, Agent B, Number Ts,
Crypt (shrK B) ⦃Agent A, Agent B, Key servK, Number Ts⦄ ⦄)
∈ set evs"
inductive_set kerbIV :: "event list set"
where
Nil: "[] ∈ kerbIV"
| Fake: "⟦ evsf ∈ kerbIV; X ∈ synth (analz (spies evsf)) ⟧
⟹ Says Spy B X # evsf ∈ kerbIV"
| K1: "⟦ evs1 ∈ kerbIV ⟧
⟹ Says A Kas ⦃Agent A, Agent Tgs, Number (CT evs1)⦄ # evs1
∈ kerbIV"
| K2: "⟦ evs2 ∈ kerbIV; Key authK ∉ used evs2; authK ∈ symKeys;
Says A' Kas ⦃Agent A, Agent Tgs, Number T1⦄ ∈ set evs2 ⟧
⟹ Says Kas A
(Crypt (shrK A) ⦃Key authK, Agent Tgs, Number (CT evs2),
(Crypt (shrK Tgs) ⦃Agent A, Agent Tgs, Key authK,
Number (CT evs2)⦄)⦄) # evs2 ∈ kerbIV"
| K3: "⟦ evs3 ∈ kerbIV;
Says A Kas ⦃Agent A, Agent Tgs, Number T1⦄ ∈ set evs3;
Says Kas' A (Crypt (shrK A) ⦃Key authK, Agent Tgs, Number Ta,
authTicket⦄) ∈ set evs3;
valid Ta wrt T1
⟧
⟹ Says A Tgs ⦃authTicket,
(Crypt authK ⦃Agent A, Number (CT evs3)⦄),
Agent B⦄ # evs3 ∈ kerbIV"
| K4: "⟦ evs4 ∈ kerbIV; Key servK ∉ used evs4; servK ∈ symKeys;
B ≠ Tgs; authK ∈ symKeys;
Says A' Tgs ⦃
(Crypt (shrK Tgs) ⦃Agent A, Agent Tgs, Key authK,
Number Ta⦄),
(Crypt authK ⦃Agent A, Number T2⦄), Agent B⦄
∈ set evs4;
¬ expiredAK Ta evs4;
¬ expiredA T2 evs4;
servKlife + (CT evs4) ≤ authKlife + Ta
⟧
⟹ Says Tgs A
(Crypt authK ⦃Key servK, Agent B, Number (CT evs4),
Crypt (shrK B) ⦃Agent A, Agent B, Key servK,
Number (CT evs4)⦄ ⦄)
# evs4 ∈ kerbIV"
| K5: "⟦ evs5 ∈ kerbIV; authK ∈ symKeys; servK ∈ symKeys;
Says A Tgs
⦃authTicket, Crypt authK ⦃Agent A, Number T2⦄,
Agent B⦄
∈ set evs5;
Says Tgs' A
(Crypt authK ⦃Key servK, Agent B, Number Ts, servTicket⦄)
∈ set evs5;
valid Ts wrt T2 ⟧
⟹ Says A B ⦃servTicket,
Crypt servK ⦃Agent A, Number (CT evs5)⦄ ⦄
# evs5 ∈ kerbIV"
| K6: "⟦ evs6 ∈ kerbIV;
Says A' B ⦃
(Crypt (shrK B) ⦃Agent A, Agent B, Key servK, Number Ts⦄),
(Crypt servK ⦃Agent A, Number T3⦄)⦄
∈ set evs6;
¬ expiredSK Ts evs6;
¬ expiredA T3 evs6
⟧
⟹ Says B A (Crypt servK (Number T3))
# evs6 ∈ kerbIV"
| Oops1: "⟦ evsO1 ∈ kerbIV; A ≠ Spy;
Says Kas A
(Crypt (shrK A) ⦃Key authK, Agent Tgs, Number Ta,
authTicket⦄) ∈ set evsO1;
expiredAK Ta evsO1 ⟧
⟹ Says A Spy ⦃Agent A, Agent Tgs, Number Ta, Key authK⦄
# evsO1 ∈ kerbIV"
| Oops2: "⟦ evsO2 ∈ kerbIV; A ≠ Spy;
Says Tgs A
(Crypt authK ⦃Key servK, Agent B, Number Ts, servTicket⦄)
∈ set evsO2;
expiredSK Ts evsO2 ⟧
⟹ Says A Spy ⦃Agent A, Agent B, Number Ts, Key servK⦄
# evsO2 ∈ kerbIV"
declare Says_imp_knows_Spy [THEN parts.Inj, dest]
declare parts.Body [dest]
declare analz_into_parts [dest]
declare Fake_parts_insert_in_Un [dest]
subsection‹Lemmas about lists, for reasoning about Issues›
lemma spies_Says_rev: "spies (evs @ [Says A B X]) = insert X (spies evs)"
apply (induct_tac "evs")
apply (rename_tac [2] a b)
apply (induct_tac [2] a, auto)
done
lemma spies_Gets_rev: "spies (evs @ [Gets A X]) = spies evs"
apply (induct_tac "evs")
apply (rename_tac [2] a b)
apply (induct_tac [2] a, auto)
done
lemma spies_Notes_rev: "spies (evs @ [Notes A X]) =
(if A∈bad then insert X (spies evs) else spies evs)"
apply (induct_tac "evs")
apply (rename_tac [2] a b)
apply (induct_tac [2] a, auto)
done
lemma spies_evs_rev: "spies evs = spies (rev evs)"
apply (induct_tac "evs")
apply (rename_tac [2] a b)
apply (induct_tac [2] a)
apply (simp_all (no_asm_simp) add: spies_Says_rev spies_Gets_rev spies_Notes_rev)
done
lemmas parts_spies_evs_revD2 = spies_evs_rev [THEN equalityD2, THEN parts_mono]
lemma spies_takeWhile: "spies (takeWhile P evs) ⊆ spies evs"
apply (induct_tac "evs")
apply (rename_tac [2] a b)
apply (induct_tac [2] "a", auto)
txt‹Resembles ‹used_subset_append› in theory Event.›
done
lemmas parts_spies_takeWhile_mono = spies_takeWhile [THEN parts_mono]
subsection‹Lemmas about \<^term>‹authKeys››
lemma authKeys_empty: "authKeys [] = {}"
unfolding authKeys_def
apply (simp (no_asm))
done
lemma authKeys_not_insert:
"(∀A Ta akey Peer.
ev ≠ Says Kas A (Crypt (shrK A) ⦃akey, Agent Peer, Ta,
(Crypt (shrK Peer) ⦃Agent A, Agent Peer, akey, Ta⦄)⦄))
⟹ authKeys (ev # evs) = authKeys evs"
unfolding authKeys_def by auto
lemma authKeys_insert:
"authKeys
(Says Kas A (Crypt (shrK A) ⦃Key K, Agent Peer, Number Ta,
(Crypt (shrK Peer) ⦃Agent A, Agent Peer, Key K, Number Ta⦄)⦄) # evs)
= insert K (authKeys evs)"
unfolding authKeys_def by auto
lemma authKeys_simp:
"K ∈ authKeys
(Says Kas A (Crypt (shrK A) ⦃Key K', Agent Peer, Number Ta,
(Crypt (shrK Peer) ⦃Agent A, Agent Peer, Key K', Number Ta⦄)⦄) # evs)
⟹ K = K' | K ∈ authKeys evs"
unfolding authKeys_def by auto
lemma authKeysI:
"Says Kas A (Crypt (shrK A) ⦃Key K, Agent Tgs, Number Ta,
(Crypt (shrK Tgs) ⦃Agent A, Agent Tgs, Key K, Number Ta⦄)⦄) ∈ set evs
⟹ K ∈ authKeys evs"
unfolding authKeys_def by auto
lemma authKeys_used: "K ∈ authKeys evs ⟹ Key K ∈ used evs"
by (simp add: authKeys_def, blast)
subsection‹Forwarding Lemmas›
text‹--For reasoning about the encrypted portion of message K3--›
lemma K3_msg_in_parts_spies:
"Says Kas' A (Crypt KeyA ⦃authK, Peer, Ta, authTicket⦄)
∈ set evs ⟹ authTicket ∈ parts (spies evs)"
by blast
lemma Oops_range_spies1:
"⟦ Says Kas A (Crypt KeyA ⦃Key authK, Peer, Ta, authTicket⦄)
∈ set evs ;
evs ∈ kerbIV ⟧ ⟹ authK ∉ range shrK ∧ authK ∈ symKeys"
apply (erule rev_mp)
apply (erule kerbIV.induct, auto)
done
text‹--For reasoning about the encrypted portion of message K5--›
lemma K5_msg_in_parts_spies:
"Says Tgs' A (Crypt authK ⦃servK, Agent B, Ts, servTicket⦄)
∈ set evs ⟹ servTicket ∈ parts (spies evs)"
by blast
lemma Oops_range_spies2:
"⟦ Says Tgs A (Crypt authK ⦃Key servK, Agent B, Ts, servTicket⦄)
∈ set evs ;
evs ∈ kerbIV ⟧ ⟹ servK ∉ range shrK ∧ servK ∈ symKeys"
apply (erule rev_mp)
apply (erule kerbIV.induct, auto)
done
lemma Says_ticket_parts:
"Says S A (Crypt K ⦃SesKey, B, TimeStamp, Ticket⦄) ∈ set evs
⟹ Ticket ∈ parts (spies evs)"
by blast
lemma Spy_see_shrK [simp]:
"evs ∈ kerbIV ⟹ (Key (shrK A) ∈ parts (spies evs)) = (A ∈ bad)"
apply (erule kerbIV.induct)
apply (frule_tac [7] K5_msg_in_parts_spies)
apply (frule_tac [5] K3_msg_in_parts_spies, simp_all)
apply (blast+)
done
lemma Spy_analz_shrK [simp]:
"evs ∈ kerbIV ⟹ (Key (shrK A) ∈ analz (spies evs)) = (A ∈ bad)"
by auto
lemma Spy_see_shrK_D [dest!]:
"⟦ Key (shrK A) ∈ parts (spies evs); evs ∈ kerbIV ⟧ ⟹ A∈bad"
by (blast dest: Spy_see_shrK)
lemmas Spy_analz_shrK_D = analz_subset_parts [THEN subsetD, THEN Spy_see_shrK_D, dest!]
text‹Nobody can have used non-existent keys!›
lemma new_keys_not_used [simp]:
"⟦Key K ∉ used evs; K ∈ symKeys; evs ∈ kerbIV⟧
⟹ K ∉ keysFor (parts (spies evs))"
apply (erule rev_mp)
apply (erule kerbIV.induct)
apply (frule_tac [7] K5_msg_in_parts_spies)
apply (frule_tac [5] K3_msg_in_parts_spies, simp_all)
txt‹Fake›
apply (force dest!: keysFor_parts_insert)
txt‹Others›
apply (force dest!: analz_shrK_Decrypt)+
done
lemma new_keys_not_analzd:
"⟦evs ∈ kerbIV; K ∈ symKeys; Key K ∉ used evs⟧
⟹ K ∉ keysFor (analz (spies evs))"
by (blast dest: new_keys_not_used intro: keysFor_mono [THEN subsetD])
subsection‹Lemmas for reasoning about predicate "before"›
lemma used_Says_rev: "used (evs @ [Says A B X]) = parts {X} ∪ (used evs)"
apply (induct_tac "evs")
apply simp
apply (rename_tac a b)
apply (induct_tac "a")
apply auto
done
lemma used_Notes_rev: "used (evs @ [Notes A X]) = parts {X} ∪ (used evs)"
apply (induct_tac "evs")
apply simp
apply (rename_tac a b)
apply (induct_tac "a")
apply auto
done
lemma used_Gets_rev: "used (evs @ [Gets B X]) = used evs"
apply (induct_tac "evs")
apply simp
apply (rename_tac a b)
apply (induct_tac "a")
apply auto
done
lemma used_evs_rev: "used evs = used (rev evs)"
apply (induct_tac "evs")
apply simp
apply (rename_tac a b)
apply (induct_tac "a")
apply (simp add: used_Says_rev)
apply (simp add: used_Gets_rev)
apply (simp add: used_Notes_rev)
done
lemma used_takeWhile_used [rule_format]:
"x ∈ used (takeWhile P X) ⟶ x ∈ used X"
apply (induct_tac "X")
apply simp
apply (rename_tac a b)
apply (induct_tac "a")
apply (simp_all add: used_Nil)
apply (blast dest!: initState_into_used)+
done
lemma set_evs_rev: "set evs = set (rev evs)"
by auto
lemma takeWhile_void [rule_format]:
"x ∉ set evs ⟶ takeWhile (λz. z ≠ x) evs = evs"
by auto
subsection‹Regularity Lemmas›
text‹These concern the form of items passed in messages›
text‹Describes the form of all components sent by Kas›
lemma Says_Kas_message_form:
"⟦ Says Kas A (Crypt K ⦃Key authK, Agent Peer, Number Ta, authTicket⦄)
∈ set evs;
evs ∈ kerbIV ⟧ ⟹
K = shrK A ∧ Peer = Tgs ∧
authK ∉ range shrK ∧ authK ∈ authKeys evs ∧ authK ∈ symKeys ∧
authTicket = (Crypt (shrK Tgs) ⦃Agent A, Agent Tgs, Key authK, Number Ta⦄) ∧
Key authK ∉ used(before
Says Kas A (Crypt K ⦃Key authK, Agent Peer, Number Ta, authTicket⦄)
on evs) ∧
Ta = CT (before
Says Kas A (Crypt K ⦃Key authK, Agent Peer, Number Ta, authTicket⦄)
on evs)"
unfolding before_def
apply (erule rev_mp)
apply (erule kerbIV.induct)
apply (simp_all (no_asm) add: authKeys_def authKeys_insert, blast, blast)
txt‹K2›
apply (simp (no_asm) add: takeWhile_tail)
apply (rule conjI)
apply (metis Key_not_used authKeys_used length_rev set_rev takeWhile_void used_evs_rev)
apply blast+
done
lemma SesKey_is_session_key:
"⟦ Crypt (shrK Tgs_B) ⦃Agent A, Agent Tgs_B, Key SesKey, Number T⦄
∈ parts (spies evs); Tgs_B ∉ bad;
evs ∈ kerbIV ⟧
⟹ SesKey ∉ range shrK"
apply (erule rev_mp)
apply (erule kerbIV.induct)
apply (frule_tac [7] K5_msg_in_parts_spies)
apply (frule_tac [5] K3_msg_in_parts_spies, simp_all, blast)
done
lemma authTicket_authentic:
"⟦ Crypt (shrK Tgs) ⦃Agent A, Agent Tgs, Key authK, Number Ta⦄
∈ parts (spies evs);
evs ∈ kerbIV ⟧
⟹ Says Kas A (Crypt (shrK A) ⦃Key authK, Agent Tgs, Number Ta,
Crypt (shrK Tgs) ⦃Agent A, Agent Tgs, Key authK, Number Ta⦄⦄)
∈ set evs"
apply (erule rev_mp)
apply (erule kerbIV.induct)
apply (frule_tac [7] K5_msg_in_parts_spies)
apply (frule_tac [5] K3_msg_in_parts_spies, simp_all)
txt‹Fake, K4›
apply (blast+)
done
lemma authTicket_crypt_authK:
"⟦ Crypt (shrK Tgs) ⦃Agent A, Agent Tgs, Key authK, Number Ta⦄
∈ parts (spies evs);
evs ∈ kerbIV ⟧
⟹ authK ∈ authKeys evs"
apply (frule authTicket_authentic, assumption)
apply (simp (no_asm) add: authKeys_def)
apply blast
done
text‹Describes the form of servK, servTicket and authK sent by Tgs›
lemma Says_Tgs_message_form:
"⟦ Says Tgs A (Crypt authK ⦃Key servK, Agent B, Number Ts, servTicket⦄)
∈ set evs;
evs ∈ kerbIV ⟧
⟹ B ≠ Tgs ∧
authK ∉ range shrK ∧ authK ∈ authKeys evs ∧ authK ∈ symKeys ∧
servK ∉ range shrK ∧ servK ∉ authKeys evs ∧ servK ∈ symKeys ∧
servTicket = (Crypt (shrK B) ⦃Agent A, Agent B, Key servK, Number Ts⦄) ∧
Key servK ∉ used (before
Says Tgs A (Crypt authK ⦃Key servK, Agent B, Number Ts, servTicket⦄)
on evs) ∧
Ts = CT(before
Says Tgs A (Crypt authK ⦃Key servK, Agent B, Number Ts, servTicket⦄)
on evs) "
unfolding before_def
apply (erule rev_mp)
apply (erule kerbIV.induct)
apply (simp_all add: authKeys_insert authKeys_not_insert authKeys_empty authKeys_simp, blast)
txt‹We need this simplification only for Message 4›
apply (simp (no_asm) add: takeWhile_tail)
apply auto
txt‹Five subcases of Message 4›
apply (blast dest!: SesKey_is_session_key)
apply (blast dest: authTicket_crypt_authK)
apply (blast dest!: authKeys_used Says_Kas_message_form)
txt‹subcase: used before›
apply (metis used_evs_rev used_takeWhile_used)
txt‹subcase: CT before›
apply (metis length_rev set_evs_rev takeWhile_void)
done
lemma authTicket_form:
"⟦ Crypt (shrK A) ⦃Key authK, Agent Tgs, Ta, authTicket⦄
∈ parts (spies evs);
A ∉ bad;
evs ∈ kerbIV ⟧
⟹ authK ∉ range shrK ∧ authK ∈ symKeys ∧
authTicket = Crypt (shrK Tgs) ⦃Agent A, Agent Tgs, Key authK, Ta⦄"
apply (erule rev_mp)
apply (erule kerbIV.induct)
apply (frule_tac [7] K5_msg_in_parts_spies)
apply (frule_tac [5] K3_msg_in_parts_spies, simp_all)
apply (blast+)
done
text‹This form holds also over an authTicket, but is not needed below.›
lemma servTicket_form:
"⟦ Crypt authK ⦃Key servK, Agent B, Ts, servTicket⦄
∈ parts (spies evs);
Key authK ∉ analz (spies evs);
evs ∈ kerbIV ⟧
⟹ servK ∉ range shrK ∧ servK ∈ symKeys ∧
(∃A. servTicket = Crypt (shrK B) ⦃Agent A, Agent B, Key servK, Ts⦄)"
apply (erule rev_mp)
apply (erule rev_mp)
apply (erule kerbIV.induct, analz_mono_contra)
apply (frule_tac [7] K5_msg_in_parts_spies)
apply (frule_tac [5] K3_msg_in_parts_spies, simp_all, blast)
done
text‹Essentially the same as ‹authTicket_form››
lemma Says_kas_message_form:
"⟦ Says Kas' A (Crypt (shrK A)
⦃Key authK, Agent Tgs, Ta, authTicket⦄) ∈ set evs;
evs ∈ kerbIV ⟧
⟹ authK ∉ range shrK ∧ authK ∈ symKeys ∧
authTicket =
Crypt (shrK Tgs) ⦃Agent A, Agent Tgs, Key authK, Ta⦄
| authTicket ∈ analz (spies evs)"
by (blast dest: analz_shrK_Decrypt authTicket_form
Says_imp_spies [THEN analz.Inj])
lemma Says_tgs_message_form:
"⟦ Says Tgs' A (Crypt authK ⦃Key servK, Agent B, Ts, servTicket⦄)
∈ set evs; authK ∈ symKeys;
evs ∈ kerbIV ⟧
⟹ servK ∉ range shrK ∧
(∃A. servTicket =
Crypt (shrK B) ⦃Agent A, Agent B, Key servK, Ts⦄)
| servTicket ∈ analz (spies evs)"
by (metis Says_imp_analz_Spy Says_imp_parts_knows_Spy analz.Decrypt analz.Snd invKey_K servTicket_form)
subsection‹Authenticity theorems: confirm origin of sensitive messages›
lemma authK_authentic:
"⟦ Crypt (shrK A) ⦃Key authK, Peer, Ta, authTicket⦄
∈ parts (spies evs);
A ∉ bad; evs ∈ kerbIV ⟧
⟹ Says Kas A (Crypt (shrK A) ⦃Key authK, Peer, Ta, authTicket⦄)
∈ set evs"
apply (erule rev_mp)
apply (erule kerbIV.induct)
apply (frule_tac [7] K5_msg_in_parts_spies)
apply (frule_tac [5] K3_msg_in_parts_spies, simp_all)
txt‹Fake›
apply blast
txt‹K4›
apply (blast dest!: authTicket_authentic [THEN Says_Kas_message_form])
done
text‹If a certain encrypted message appears then it originated with Tgs›
lemma servK_authentic:
"⟦ Crypt authK ⦃Key servK, Agent B, Number Ts, servTicket⦄
∈ parts (spies evs);
Key authK ∉ analz (spies evs);
authK ∉ range shrK;
evs ∈ kerbIV ⟧
⟹ ∃A. Says Tgs A (Crypt authK ⦃Key servK, Agent B, Number Ts, servTicket⦄)
∈ set evs"
apply (erule rev_mp)
apply (erule rev_mp)
apply (erule kerbIV.induct, analz_mono_contra)
apply (frule_tac [7] K5_msg_in_parts_spies)
apply (frule_tac [5] K3_msg_in_parts_spies, simp_all)
txt‹Fake›
apply blast
txt‹K2›
apply blast
txt‹K4›
apply auto
done
lemma servK_authentic_bis:
"⟦ Crypt authK ⦃Key servK, Agent B, Number Ts, servTicket⦄
∈ parts (spies evs);
Key authK ∉ analz (spies evs);
B ≠ Tgs;
evs ∈ kerbIV ⟧
⟹ ∃A. Says Tgs A (Crypt authK ⦃Key servK, Agent B, Number Ts, servTicket⦄)
∈ set evs"
apply (erule rev_mp)
apply (erule rev_mp)
apply (erule kerbIV.induct, analz_mono_contra)
apply (frule_tac [7] K5_msg_in_parts_spies)
apply (frule_tac [5] K3_msg_in_parts_spies, simp_all)
txt‹Fake›
apply blast
txt‹K4›
apply blast
done
text‹Authenticity of servK for B›
lemma servTicket_authentic_Tgs:
"⟦ Crypt (shrK B) ⦃Agent A, Agent B, Key servK, Number Ts⦄
∈ parts (spies evs); B ≠ Tgs; B ∉ bad;
evs ∈ kerbIV ⟧
⟹ ∃authK.
Says Tgs A (Crypt authK ⦃Key servK, Agent B, Number Ts,
Crypt (shrK B) ⦃Agent A, Agent B, Key servK, Number Ts⦄⦄)
∈ set evs"
apply (erule rev_mp)
apply (erule rev_mp)
apply (erule kerbIV.induct)
apply (frule_tac [7] K5_msg_in_parts_spies)
apply (frule_tac [5] K3_msg_in_parts_spies, simp_all)
apply blast+
done
text‹Anticipated here from next subsection›
lemma K4_imp_K2:
"⟦ Says Tgs A (Crypt authK ⦃Key servK, Agent B, Number Ts, servTicket⦄)
∈ set evs; evs ∈ kerbIV⟧
⟹ ∃Ta. Says Kas A
(Crypt (shrK A)
⦃Key authK, Agent Tgs, Number Ta,
Crypt (shrK Tgs) ⦃Agent A, Agent Tgs, Key authK, Number Ta⦄⦄)
∈ set evs"
apply (erule rev_mp)
apply (erule kerbIV.induct)
apply (frule_tac [7] K5_msg_in_parts_spies)
apply (frule_tac [5] K3_msg_in_parts_spies, simp_all, auto)
apply (blast dest!: Says_imp_spies [THEN parts.Inj, THEN parts.Fst, THEN authTicket_authentic])
done
text‹Anticipated here from next subsection›
lemma u_K4_imp_K2:
"⟦ Says Tgs A (Crypt authK ⦃Key servK, Agent B, Number Ts, servTicket⦄)
∈ set evs; evs ∈ kerbIV⟧
⟹ ∃Ta. (Says Kas A (Crypt (shrK A) ⦃Key authK, Agent Tgs, Number Ta,
Crypt (shrK Tgs) ⦃Agent A, Agent Tgs, Key authK, Number Ta⦄⦄)
∈ set evs
∧ servKlife + Ts ≤ authKlife + Ta)"
apply (erule rev_mp)
apply (erule kerbIV.induct)
apply (frule_tac [7] K5_msg_in_parts_spies)
apply (frule_tac [5] K3_msg_in_parts_spies, simp_all, auto)
apply (blast dest!: Says_imp_spies [THEN parts.Inj, THEN parts.Fst, THEN authTicket_authentic])
done
lemma servTicket_authentic_Kas:
"⟦ Crypt (shrK B) ⦃Agent A, Agent B, Key servK, Number Ts⦄
∈ parts (spies evs); B ≠ Tgs; B ∉ bad;
evs ∈ kerbIV ⟧
⟹ ∃authK Ta.
Says Kas A
(Crypt (shrK A) ⦃Key authK, Agent Tgs, Number Ta,
Crypt (shrK Tgs) ⦃Agent A, Agent Tgs, Key authK, Number Ta⦄⦄)
∈ set evs"
by (blast dest!: servTicket_authentic_Tgs K4_imp_K2)
lemma u_servTicket_authentic_Kas:
"⟦ Crypt (shrK B) ⦃Agent A, Agent B, Key servK, Number Ts⦄
∈ parts (spies evs); B ≠ Tgs; B ∉ bad;
evs ∈ kerbIV ⟧
⟹ ∃authK Ta. Says Kas A (Crypt(shrK A) ⦃Key authK, Agent Tgs, Number Ta,
Crypt (shrK Tgs) ⦃Agent A, Agent Tgs, Key authK, Number Ta⦄⦄)
∈ set evs
∧ servKlife + Ts ≤ authKlife + Ta"
by (blast dest!: servTicket_authentic_Tgs u_K4_imp_K2)
lemma servTicket_authentic:
"⟦ Crypt (shrK B) ⦃Agent A, Agent B, Key servK, Number Ts⦄
∈ parts (spies evs); B ≠ Tgs; B ∉ bad;
evs ∈ kerbIV ⟧
⟹ ∃Ta authK.
Says Kas A (Crypt (shrK A) ⦃Key authK, Agent Tgs, Number Ta,
Crypt (shrK Tgs) ⦃Agent A, Agent Tgs, Key authK, Number Ta⦄⦄)
∈ set evs
∧ Says Tgs A (Crypt authK ⦃Key servK, Agent B, Number Ts,
Crypt (shrK B) ⦃Agent A, Agent B, Key servK, Number Ts⦄⦄)
∈ set evs"
by (blast dest: servTicket_authentic_Tgs K4_imp_K2)
lemma u_servTicket_authentic:
"⟦ Crypt (shrK B) ⦃Agent A, Agent B, Key servK, Number Ts⦄
∈ parts (spies evs); B ≠ Tgs; B ∉ bad;
evs ∈ kerbIV ⟧
⟹ ∃Ta authK.
(Says Kas A (Crypt (shrK A) ⦃Key authK, Agent Tgs, Number Ta,
Crypt (shrK Tgs) ⦃Agent A, Agent Tgs, Key authK, Number Ta⦄⦄)
∈ set evs
∧ Says Tgs A (Crypt authK ⦃Key servK, Agent B, Number Ts,
Crypt (shrK B) ⦃Agent A, Agent B, Key servK, Number Ts⦄⦄)
∈ set evs
∧ servKlife + Ts ≤ authKlife + Ta)"
by (blast dest: servTicket_authentic_Tgs u_K4_imp_K2)
lemma u_NotexpiredSK_NotexpiredAK:
"⟦ ¬ expiredSK Ts evs; servKlife + Ts ≤ authKlife + Ta ⟧
⟹ ¬ expiredAK Ta evs"
by (metis le_less_trans)
subsection‹Reliability: friendly agents send something if something else happened›
lemma K3_imp_K2:
"⟦ Says A Tgs
⦃authTicket, Crypt authK ⦃Agent A, Number T2⦄, Agent B⦄
∈ set evs;
A ∉ bad; evs ∈ kerbIV ⟧
⟹ ∃Ta. Says Kas A (Crypt (shrK A)
⦃Key authK, Agent Tgs, Number Ta, authTicket⦄)
∈ set evs"
apply (erule rev_mp)
apply (erule kerbIV.induct)
apply (frule_tac [7] K5_msg_in_parts_spies)
apply (frule_tac [5] K3_msg_in_parts_spies, simp_all, blast, blast)
apply (blast dest: Says_imp_spies [THEN parts.Inj, THEN authK_authentic])
done
text‹Anticipated here from next subsection. An authK is encrypted by one and only one Shared key. A servK is encrypted by one and only one authK.›
lemma Key_unique_SesKey:
"⟦ Crypt K ⦃Key SesKey, Agent B, T, Ticket⦄
∈ parts (spies evs);
Crypt K' ⦃Key SesKey, Agent B', T', Ticket'⦄
∈ parts (spies evs); Key SesKey ∉ analz (spies evs);
evs ∈ kerbIV ⟧
⟹ K=K' ∧ B=B' ∧ T=T' ∧ Ticket=Ticket'"
apply (erule rev_mp)
apply (erule rev_mp)
apply (erule rev_mp)
apply (erule kerbIV.induct, analz_mono_contra)
apply (frule_tac [7] K5_msg_in_parts_spies)
apply (frule_tac [5] K3_msg_in_parts_spies, simp_all)
txt‹Fake, K2, K4›
apply (blast+)
done
lemma Tgs_authenticates_A:
"⟦ Crypt authK ⦃Agent A, Number T2⦄ ∈ parts (spies evs);
Crypt (shrK Tgs) ⦃Agent A, Agent Tgs, Key authK, Number Ta⦄
∈ parts (spies evs);
Key authK ∉ analz (spies evs); A ∉ bad; evs ∈ kerbIV ⟧
⟹ ∃ B. Says A Tgs ⦃
Crypt (shrK Tgs) ⦃Agent A, Agent Tgs, Key authK, Number Ta⦄,
Crypt authK ⦃Agent A, Number T2⦄, Agent B ⦄ ∈ set evs"
apply (drule authTicket_authentic, assumption, rotate_tac 4)
apply (erule rev_mp, erule rev_mp, erule rev_mp)
apply (erule kerbIV.induct, analz_mono_contra)
apply (frule_tac [5] Says_ticket_parts)
apply (frule_tac [7] Says_ticket_parts)
apply (simp_all (no_asm_simp) add: all_conj_distrib)
txt‹Fake›
apply blast
txt‹K2›
apply (force dest!: Crypt_imp_keysFor)
txt‹K3›
apply (blast dest: Key_unique_SesKey)
txt‹K5›
apply (metis K3_imp_K2 Key_unique_SesKey Spy_see_shrK parts.Body parts.Fst
Says_imp_knows_Spy [THEN parts.Inj])
done
lemma Says_K5:
"⟦ Crypt servK ⦃Agent A, Number T3⦄ ∈ parts (spies evs);
Says Tgs A (Crypt authK ⦃Key servK, Agent B, Number Ts,
servTicket⦄) ∈ set evs;
Key servK ∉ analz (spies evs);
A ∉ bad; B ∉ bad; evs ∈ kerbIV ⟧
⟹ Says A B ⦃servTicket, Crypt servK ⦃Agent A, Number T3⦄⦄ ∈ set evs"
apply (erule rev_mp)
apply (erule rev_mp)
apply (erule rev_mp)
apply (erule kerbIV.induct, analz_mono_contra)
apply (frule_tac [5] Says_ticket_parts)
apply (frule_tac [7] Says_ticket_parts)
apply (simp_all (no_asm_simp) add: all_conj_distrib)
apply blast
txt‹K3›
apply (blast dest: authK_authentic Says_Kas_message_form Says_Tgs_message_form)
txt‹K4›
apply (force dest!: Crypt_imp_keysFor)
txt‹K5›
apply (blast dest: Key_unique_SesKey)
done
text‹Anticipated here from next subsection›
lemma unique_CryptKey:
"⟦ Crypt (shrK B) ⦃Agent A, Agent B, Key SesKey, T⦄
∈ parts (spies evs);
Crypt (shrK B') ⦃Agent A', Agent B', Key SesKey, T'⦄
∈ parts (spies evs); Key SesKey ∉ analz (spies evs);
evs ∈ kerbIV ⟧
⟹ A=A' ∧ B=B' ∧ T=T'"
apply (erule rev_mp)
apply (erule rev_mp)
apply (erule rev_mp)
apply (erule kerbIV.induct, analz_mono_contra)
apply (frule_tac [7] K5_msg_in_parts_spies)
apply (frule_tac [5] K3_msg_in_parts_spies, simp_all)
txt‹Fake, K2, K4›
apply (blast+)
done
lemma Says_K6:
"⟦ Crypt servK (Number T3) ∈ parts (spies evs);
Says Tgs A (Crypt authK ⦃Key servK, Agent B, Number Ts,
servTicket⦄) ∈ set evs;
Key servK ∉ analz (spies evs);
A ∉ bad; B ∉ bad; evs ∈ kerbIV ⟧
⟹ Says B A (Crypt servK (Number T3)) ∈ set evs"
apply (erule rev_mp)
apply (erule rev_mp)
apply (erule rev_mp)
apply (erule kerbIV.induct, analz_mono_contra)
apply (frule_tac [5] Says_ticket_parts)
apply (frule_tac [7] Says_ticket_parts)
apply (simp_all (no_asm_simp))
apply blast
apply (metis Crypt_imp_invKey_keysFor invKey_K new_keys_not_used)
apply (clarify)
apply (frule Says_Tgs_message_form, assumption)
apply (metis K3_msg_in_parts_spies parts.Fst Says_imp_knows_Spy [THEN parts.Inj]
unique_CryptKey)
done
text‹Needs a unicity theorem, hence moved here›
lemma servK_authentic_ter:
"⟦ Says Kas A
(Crypt (shrK A) ⦃Key authK, Agent Tgs, Number Ta, authTicket⦄) ∈ set evs;
Crypt authK ⦃Key servK, Agent B, Number Ts, servTicket⦄
∈ parts (spies evs);
Key authK ∉ analz (spies evs);
evs ∈ kerbIV ⟧
⟹ Says Tgs A (Crypt authK ⦃Key servK, Agent B, Number Ts, servTicket⦄)
∈ set evs"
apply (frule Says_Kas_message_form, assumption)
apply (erule rev_mp)
apply (erule rev_mp)
apply (erule rev_mp)
apply (erule kerbIV.induct, analz_mono_contra)
apply (frule_tac [7] K5_msg_in_parts_spies)
apply (frule_tac [5] K3_msg_in_parts_spies, simp_all, blast)
txt‹K2›
apply (blast dest!: servK_authentic Says_Tgs_message_form authKeys_used)
txt‹K4 remain›
apply (blast dest!: unique_CryptKey)
done
subsection‹Unicity Theorems›
text‹The session key, if secure, uniquely identifies the Ticket
whether authTicket or servTicket. As a matter of fact, one can read
also Tgs in the place of B.›
lemma unique_authKeys:
"⟦ Says Kas A
(Crypt Ka ⦃Key authK, Agent Tgs, Ta, X⦄) ∈ set evs;
Says Kas A'
(Crypt Ka' ⦃Key authK, Agent Tgs, Ta', X'⦄) ∈ set evs;
evs ∈ kerbIV ⟧ ⟹ A=A' ∧ Ka=Ka' ∧ Ta=Ta' ∧ X=X'"
apply (erule rev_mp)
apply (erule rev_mp)
apply (erule kerbIV.induct)
apply (frule_tac [7] K5_msg_in_parts_spies)
apply (frule_tac [5] K3_msg_in_parts_spies, simp_all)
txt‹K2›
apply blast
done
text‹servK uniquely identifies the message from Tgs›
lemma unique_servKeys:
"⟦ Says Tgs A
(Crypt K ⦃Key servK, Agent B, Ts, X⦄) ∈ set evs;
Says Tgs A'
(Crypt K' ⦃Key servK, Agent B', Ts', X'⦄) ∈ set evs;
evs ∈ kerbIV ⟧ ⟹ A=A' ∧ B=B' ∧ K=K' ∧ Ts=Ts' ∧ X=X'"
apply (erule rev_mp)
apply (erule rev_mp)
apply (erule kerbIV.induct)
apply (frule_tac [7] K5_msg_in_parts_spies)
apply (frule_tac [5] K3_msg_in_parts_spies, simp_all)
txt‹K4›
apply blast
done
text‹Revised unicity theorems›
lemma Kas_Unique:
"⟦ Says Kas A
(Crypt Ka ⦃Key authK, Agent Tgs, Ta, authTicket⦄) ∈ set evs;
evs ∈ kerbIV ⟧ ⟹
Unique (Says Kas A (Crypt Ka ⦃Key authK, Agent Tgs, Ta, authTicket⦄))
on evs"
apply (erule rev_mp, erule kerbIV.induct, simp_all add: Unique_def)
apply blast
done
lemma Tgs_Unique:
"⟦ Says Tgs A
(Crypt authK ⦃Key servK, Agent B, Ts, servTicket⦄) ∈ set evs;
evs ∈ kerbIV ⟧ ⟹
Unique (Says Tgs A (Crypt authK ⦃Key servK, Agent B, Ts, servTicket⦄))
on evs"
apply (erule rev_mp, erule kerbIV.induct, simp_all add: Unique_def)
apply blast
done
subsection‹Lemmas About the Predicate \<^term>‹AKcryptSK››
lemma not_AKcryptSK_Nil [iff]: "¬ AKcryptSK authK servK []"
by (simp add: AKcryptSK_def)
lemma AKcryptSKI:
"⟦ Says Tgs A (Crypt authK ⦃Key servK, Agent B, Number Ts, X ⦄) ∈ set evs;
evs ∈ kerbIV ⟧ ⟹ AKcryptSK authK servK evs"
unfolding AKcryptSK_def
apply (blast dest: Says_Tgs_message_form)
done
lemma AKcryptSK_Says [simp]:
"AKcryptSK authK servK (Says S A X # evs) =
(Tgs = S ∧
(∃B Ts. X = Crypt authK
⦃Key servK, Agent B, Number Ts,
Crypt (shrK B) ⦃Agent A, Agent B, Key servK, Number Ts⦄ ⦄)
| AKcryptSK authK servK evs)"
by (auto simp add: AKcryptSK_def)
lemma Auth_fresh_not_AKcryptSK:
"⟦ Key authK ∉ used evs; evs ∈ kerbIV ⟧
⟹ ¬ AKcryptSK authK servK evs"
unfolding AKcryptSK_def
apply (erule rev_mp)
apply (erule kerbIV.induct)
apply (frule_tac [7] K5_msg_in_parts_spies)
apply (frule_tac [5] K3_msg_in_parts_spies, simp_all, blast)
done
lemma Serv_fresh_not_AKcryptSK:
"Key servK ∉ used evs ⟹ ¬ AKcryptSK authK servK evs"
unfolding AKcryptSK_def by blast
lemma authK_not_AKcryptSK:
"⟦ Crypt (shrK Tgs) ⦃Agent A, Agent Tgs, Key authK, tk⦄
∈ parts (spies evs); evs ∈ kerbIV ⟧
⟹ ¬ AKcryptSK K authK evs"
apply (erule rev_mp)
apply (erule kerbIV.induct)
apply (frule_tac [7] K5_msg_in_parts_spies)
apply (frule_tac [5] K3_msg_in_parts_spies, simp_all)
txt‹Fake›
apply blast
txt‹K2: by freshness›
apply (simp add: AKcryptSK_def)
txt‹K4›
apply (blast+)
done
text‹A secure serverkey cannot have been used to encrypt others›
lemma servK_not_AKcryptSK:
"⟦ Crypt (shrK B) ⦃Agent A, Agent B, Key SK, Number Ts⦄ ∈ parts (spies evs);
Key SK ∉ analz (spies evs); SK ∈ symKeys;
B ≠ Tgs; evs ∈ kerbIV ⟧
⟹ ¬ AKcryptSK SK K evs"
apply (erule rev_mp)
apply (erule rev_mp)
apply (erule kerbIV.induct, analz_mono_contra)
apply (frule_tac [7] K5_msg_in_parts_spies)
apply (frule_tac [5] K3_msg_in_parts_spies, simp_all, blast)
txt‹K4›
apply (metis Auth_fresh_not_AKcryptSK Crypt_imp_keysFor new_keys_not_used parts.Fst parts.Snd Says_imp_knows_Spy [THEN parts.Inj] unique_CryptKey)
done
text‹Long term keys are not issued as servKeys›
lemma shrK_not_AKcryptSK:
"evs ∈ kerbIV ⟹ ¬ AKcryptSK K (shrK A) evs"
unfolding AKcryptSK_def
apply (erule kerbIV.induct)
apply (frule_tac [7] K5_msg_in_parts_spies)
apply (frule_tac [5] K3_msg_in_parts_spies, auto)
done
text‹The Tgs message associates servK with authK and therefore not with any
other key authK.›
lemma Says_Tgs_AKcryptSK:
"⟦ Says Tgs A (Crypt authK ⦃Key servK, Agent B, Number Ts, X ⦄)
∈ set evs;
authK' ≠ authK; evs ∈ kerbIV ⟧
⟹ ¬ AKcryptSK authK' servK evs"
unfolding AKcryptSK_def
apply (blast dest: unique_servKeys)
done
text‹Equivalently›
lemma not_different_AKcryptSK:
"⟦ AKcryptSK authK servK evs;
authK' ≠ authK; evs ∈ kerbIV ⟧
⟹ ¬ AKcryptSK authK' servK evs ∧ servK ∈ symKeys"
apply (simp add: AKcryptSK_def)
apply (blast dest: unique_servKeys Says_Tgs_message_form)
done
lemma AKcryptSK_not_AKcryptSK:
"⟦ AKcryptSK authK servK evs; evs ∈ kerbIV ⟧
⟹ ¬ AKcryptSK servK K evs"
apply (erule rev_mp)
apply (erule kerbIV.induct)
apply (frule_tac [7] K5_msg_in_parts_spies)
apply (frule_tac [5] K3_msg_in_parts_spies, simp_all)
apply (metis Auth_fresh_not_AKcryptSK Says_imp_spies authK_not_AKcryptSK
authKeys_used authTicket_crypt_authK parts.Fst parts.Inj)
done
text‹The only session keys that can be found with the help of session keys are
those sent by Tgs in step K4.›
text‹We take some pains to express the property
as a logical equivalence so that the simplifier can apply it.›
lemma Key_analz_image_Key_lemma:
"P ⟶ (Key K ∈ analz (Key`KK ∪ H)) ⟶ (K∈KK | Key K ∈ analz H)
⟹
P ⟶ (Key K ∈ analz (Key`KK ∪ H)) = (K∈KK | Key K ∈ analz H)"
by (blast intro: analz_mono [THEN subsetD])
lemma AKcryptSK_analz_insert:
"⟦ AKcryptSK K K' evs; K ∈ symKeys; evs ∈ kerbIV ⟧
⟹ Key K' ∈ analz (insert (Key K) (spies evs))"
apply (simp add: AKcryptSK_def, clarify)
apply (drule Says_imp_spies [THEN analz.Inj, THEN analz_insertI], auto)
done
lemma authKeys_are_not_AKcryptSK:
"⟦ K ∈ authKeys evs ∪ range shrK; evs ∈ kerbIV ⟧
⟹ ∀SK. ¬ AKcryptSK SK K evs ∧ K ∈ symKeys"
apply (simp add: authKeys_def AKcryptSK_def)
apply (blast dest: Says_Kas_message_form Says_Tgs_message_form)
done
lemma not_authKeys_not_AKcryptSK:
"⟦ K ∉ authKeys evs;
K ∉ range shrK; evs ∈ kerbIV ⟧
⟹ ∀SK. ¬ AKcryptSK K SK evs"
apply (simp add: AKcryptSK_def)
apply (blast dest: Says_Tgs_message_form)
done
subsection‹Secrecy Theorems›
text‹For the Oops2 case of the next theorem›
lemma Oops2_not_AKcryptSK:
"⟦ evs ∈ kerbIV;
Says Tgs A (Crypt authK
⦃Key servK, Agent B, Number Ts, servTicket⦄)
∈ set evs ⟧
⟹ ¬ AKcryptSK servK SK evs"
by (blast dest: AKcryptSKI AKcryptSK_not_AKcryptSK)
text‹Big simplification law for keys SK that are not crypted by keys in KK
It helps prove three, otherwise hard, facts about keys. These facts are
exploited as simplification laws for analz, and also "limit the damage"
in case of loss of a key to the spy. See ESORICS98.
[simplified by LCP]›
lemma Key_analz_image_Key [rule_format (no_asm)]:
"evs ∈ kerbIV ⟹
(∀SK KK. SK ∈ symKeys ∧ KK ⊆ -(range shrK) ⟶
(∀K ∈ KK. ¬ AKcryptSK K SK evs) ⟶
(Key SK ∈ analz (Key`KK ∪ (spies evs))) =
(SK ∈ KK | Key SK ∈ analz (spies evs)))"
apply (erule kerbIV.induct)
apply (frule_tac [10] Oops_range_spies2)
apply (frule_tac [9] Oops_range_spies1)
apply (frule_tac [7] Says_tgs_message_form)
apply (frule_tac [5] Says_kas_message_form)
apply (safe del: impI intro!: Key_analz_image_Key_lemma [THEN impI])
txt‹Case-splits for Oops1 and message 5: the negated case simplifies using
the induction hypothesis›
apply (case_tac [11] "AKcryptSK authK SK evsO1")
apply (case_tac [8] "AKcryptSK servK SK evs5")
apply (simp_all del: image_insert
add: analz_image_freshK_simps AKcryptSK_Says shrK_not_AKcryptSK
Oops2_not_AKcryptSK Auth_fresh_not_AKcryptSK
Serv_fresh_not_AKcryptSK Says_Tgs_AKcryptSK Spy_analz_shrK)
txt‹Fake›
apply spy_analz
txt‹K2›
apply blast
txt‹K3›
apply blast
txt‹K4›
apply (blast dest!: authK_not_AKcryptSK)
txt‹K5›
apply (case_tac "Key servK ∈ analz (spies evs5) ")
txt‹If servK is compromised then the result follows directly...›
apply (simp (no_asm_simp) add: analz_insert_eq Un_upper2 [THEN analz_mono, THEN subsetD])
txt‹...therefore servK is uncompromised.›
txt‹The AKcryptSK servK SK evs5 case leads to a contradiction.›
apply (blast elim!: servK_not_AKcryptSK [THEN [2] rev_notE] del: allE ballE)
txt‹Another K5 case›
apply blast
txt‹Oops1›
apply simp
apply (blast dest!: AKcryptSK_analz_insert)
done
text‹First simplification law for analz: no session keys encrypt
authentication keys or shared keys.›
lemma analz_insert_freshK1:
"⟦ evs ∈ kerbIV; K ∈ authKeys evs ∪ range shrK;
SesKey ∉ range shrK ⟧
⟹ (Key K ∈ analz (insert (Key SesKey) (spies evs))) =
(K = SesKey | Key K ∈ analz (spies evs))"
apply (frule authKeys_are_not_AKcryptSK, assumption)
apply (simp del: image_insert
add: analz_image_freshK_simps add: Key_analz_image_Key)
done
text‹Second simplification law for analz: no service keys encrypt any other keys.›
lemma analz_insert_freshK2:
"⟦ evs ∈ kerbIV; servK ∉ (authKeys evs); servK ∉ range shrK;
K ∈ symKeys ⟧
⟹ (Key K ∈ analz (insert (Key servK) (spies evs))) =
(K = servK | Key K ∈ analz (spies evs))"
apply (frule not_authKeys_not_AKcryptSK, assumption, assumption)
apply (simp del: image_insert
add: analz_image_freshK_simps add: Key_analz_image_Key)
done
text‹Third simplification law for analz: only one authentication key encrypts a certain service key.›
lemma analz_insert_freshK3:
"⟦ AKcryptSK authK servK evs;
authK' ≠ authK; authK' ∉ range shrK; evs ∈ kerbIV ⟧
⟹ (Key servK ∈ analz (insert (Key authK') (spies evs))) =
(servK = authK' | Key servK ∈ analz (spies evs))"
apply (drule_tac authK' = authK' in not_different_AKcryptSK, blast, assumption)
apply (simp del: image_insert
add: analz_image_freshK_simps add: Key_analz_image_Key)
done
lemma analz_insert_freshK3_bis:
"⟦ Says Tgs A
(Crypt authK ⦃Key servK, Agent B, Number Ts, servTicket⦄)
∈ set evs;
authK ≠ authK'; authK' ∉ range shrK; evs ∈ kerbIV ⟧
⟹ (Key servK ∈ analz (insert (Key authK') (spies evs))) =
(servK = authK' | Key servK ∈ analz (spies evs))"
apply (frule AKcryptSKI, assumption)
apply (simp add: analz_insert_freshK3)
done
text‹a weakness of the protocol›
lemma authK_compromises_servK:
"⟦ Says Tgs A
(Crypt authK ⦃Key servK, Agent B, Number Ts, servTicket⦄)
∈ set evs; authK ∈ symKeys;
Key authK ∈ analz (spies evs); evs ∈ kerbIV ⟧
⟹ Key servK ∈ analz (spies evs)"
by (metis Says_imp_analz_Spy analz.Fst analz_Decrypt')
lemma servK_notin_authKeysD:
"⟦ Crypt authK ⦃Key servK, Agent B, Ts,
Crypt (shrK B) ⦃Agent A, Agent B, Key servK, Ts⦄⦄
∈ parts (spies evs);
Key servK ∉ analz (spies evs);
B ≠ Tgs; evs ∈ kerbIV ⟧
⟹ servK ∉ authKeys evs"
apply (erule rev_mp)
apply (erule rev_mp)
apply (simp add: authKeys_def)
apply (erule kerbIV.induct, analz_mono_contra)
apply (frule_tac [7] K5_msg_in_parts_spies)
apply (frule_tac [5] K3_msg_in_parts_spies, simp_all)
apply (blast+)
done
text‹If Spy sees the Authentication Key sent in msg K2, then
the Key has expired.›
lemma Confidentiality_Kas_lemma [rule_format]:
"⟦ authK ∈ symKeys; A ∉ bad; evs ∈ kerbIV ⟧
⟹ Says Kas A
(Crypt (shrK A)
⦃Key authK, Agent Tgs, Number Ta,
Crypt (shrK Tgs) ⦃Agent A, Agent Tgs, Key authK, Number Ta⦄⦄)
∈ set evs ⟶
Key authK ∈ analz (spies evs) ⟶
expiredAK Ta evs"
apply (erule kerbIV.induct)
apply (frule_tac [10] Oops_range_spies2)
apply (frule_tac [9] Oops_range_spies1)
apply (frule_tac [7] Says_tgs_message_form)
apply (frule_tac [5] Says_kas_message_form)
apply (safe del: impI conjI impCE)
apply (simp_all (no_asm_simp) add: Says_Kas_message_form less_SucI analz_insert_eq not_parts_not_analz analz_insert_freshK1 pushes)
txt‹Fake›
apply spy_analz
txt‹K2›
apply blast
txt‹K4›
apply blast
txt‹Level 8: K5›
apply (blast dest: servK_notin_authKeysD Says_Kas_message_form intro: less_SucI)
txt‹Oops1›
apply (blast dest!: unique_authKeys intro: less_SucI)
txt‹Oops2›
apply (blast dest: Says_Tgs_message_form Says_Kas_message_form)
done
lemma Confidentiality_Kas:
"⟦ Says Kas A
(Crypt Ka ⦃Key authK, Agent Tgs, Number Ta, authTicket⦄)
∈ set evs;
¬ expiredAK Ta evs;
A ∉ bad; evs ∈ kerbIV ⟧
⟹ Key authK ∉ analz (spies evs)"
by (blast dest: Says_Kas_message_form Confidentiality_Kas_lemma)
text‹If Spy sees the Service Key sent in msg K4, then
the Key has expired.›
lemma Confidentiality_lemma [rule_format]:
"⟦ Says Tgs A
(Crypt authK
⦃Key servK, Agent B, Number Ts,
Crypt (shrK B) ⦃Agent A, Agent B, Key servK, Number Ts⦄⦄)
∈ set evs;
Key authK ∉ analz (spies evs);
servK ∈ symKeys;
A ∉ bad; B ∉ bad; evs ∈ kerbIV ⟧
⟹ Key servK ∈ analz (spies evs) ⟶
expiredSK Ts evs"
apply (erule rev_mp)
apply (erule rev_mp)
apply (erule kerbIV.induct)
apply (rule_tac [9] impI)+
apply analz_mono_contra
apply (frule_tac [10] Oops_range_spies2)
apply (frule_tac [9] Oops_range_spies1)
apply (frule_tac [7] Says_tgs_message_form)
apply (frule_tac [5] Says_kas_message_form)
apply (safe del: impI conjI impCE)
apply (simp_all add: less_SucI new_keys_not_analzd Says_Kas_message_form Says_Tgs_message_form analz_insert_eq not_parts_not_analz analz_insert_freshK1 analz_insert_freshK2 analz_insert_freshK3_bis pushes)
txt‹Fake›
apply spy_analz
txt‹K2›
apply (blast intro: parts_insertI less_SucI)
txt‹K4›
apply (blast dest: authTicket_authentic Confidentiality_Kas)
txt‹K5›
apply (metis Says_imp_spies Says_ticket_parts Tgs_not_bad analz_insert_freshK2
less_SucI parts.Inj servK_notin_authKeysD unique_CryptKey)
txt‹Oops1›
apply (blast dest: Says_Kas_message_form Says_Tgs_message_form intro: less_SucI)
txt‹Oops2›
apply (blast dest: Says_imp_spies [THEN parts.Inj] Key_unique_SesKey intro: less_SucI)
done
text‹In the real world Tgs can't check wheter authK is secure!›
lemma Confidentiality_Tgs:
"⟦ Says Tgs A
(Crypt authK ⦃Key servK, Agent B, Number Ts, servTicket⦄)
∈ set evs;
Key authK ∉ analz (spies evs);
¬ expiredSK Ts evs;
A ∉ bad; B ∉ bad; evs ∈ kerbIV ⟧
⟹ Key servK ∉ analz (spies evs)"
by (blast dest: Says_Tgs_message_form Confidentiality_lemma)
text‹In the real world Tgs CAN check what Kas sends!›
lemma Confidentiality_Tgs_bis:
"⟦ Says Kas A
(Crypt Ka ⦃Key authK, Agent Tgs, Number Ta, authTicket⦄)
∈ set evs;
Says Tgs A
(Crypt authK ⦃Key servK, Agent B, Number Ts, servTicket⦄)
∈ set evs;
¬ expiredAK Ta evs; ¬ expiredSK Ts evs;
A ∉ bad; B ∉ bad; evs ∈ kerbIV ⟧
⟹ Key servK ∉ analz (spies evs)"
by (blast dest!: Confidentiality_Kas Confidentiality_Tgs)
text‹Most general form›
lemmas Confidentiality_Tgs_ter = authTicket_authentic [THEN Confidentiality_Tgs_bis]
lemmas Confidentiality_Auth_A = authK_authentic [THEN Confidentiality_Kas]
text‹Needs a confidentiality guarantee, hence moved here.
Authenticity of servK for A›
lemma servK_authentic_bis_r:
"⟦ Crypt (shrK A) ⦃Key authK, Agent Tgs, Number Ta, authTicket⦄
∈ parts (spies evs);
Crypt authK ⦃Key servK, Agent B, Number Ts, servTicket⦄
∈ parts (spies evs);
¬ expiredAK Ta evs; A ∉ bad; evs ∈ kerbIV ⟧
⟹Says Tgs A (Crypt authK ⦃Key servK, Agent B, Number Ts, servTicket⦄)
∈ set evs"
by (blast dest: authK_authentic Confidentiality_Auth_A servK_authentic_ter)
lemma Confidentiality_Serv_A:
"⟦ Crypt (shrK A) ⦃Key authK, Agent Tgs, Number Ta, authTicket⦄
∈ parts (spies evs);
Crypt authK ⦃Key servK, Agent B, Number Ts, servTicket⦄
∈ parts (spies evs);
¬ expiredAK Ta evs; ¬ expiredSK Ts evs;
A ∉ bad; B ∉ bad; evs ∈ kerbIV ⟧
⟹ Key servK ∉ analz (spies evs)"
apply (drule authK_authentic, assumption, assumption)
apply (blast dest: Confidentiality_Kas Says_Kas_message_form servK_authentic_ter Confidentiality_Tgs_bis)
done
lemma Confidentiality_B:
"⟦ Crypt (shrK B) ⦃Agent A, Agent B, Key servK, Number Ts⦄
∈ parts (spies evs);
Crypt authK ⦃Key servK, Agent B, Number Ts, servTicket⦄
∈ parts (spies evs);
Crypt (shrK A) ⦃Key authK, Agent Tgs, Number Ta, authTicket⦄
∈ parts (spies evs);
¬ expiredSK Ts evs; ¬ expiredAK Ta evs;
A ∉ bad; B ∉ bad; B ≠ Tgs; evs ∈ kerbIV ⟧
⟹ Key servK ∉ analz (spies evs)"
apply (frule authK_authentic)
apply (frule_tac [3] Confidentiality_Kas)
apply (frule_tac [6] servTicket_authentic, auto)
apply (blast dest!: Confidentiality_Tgs_bis dest: Says_Kas_message_form servK_authentic unique_servKeys unique_authKeys)
done
lemma u_Confidentiality_B:
"⟦ Crypt (shrK B) ⦃Agent A, Agent B, Key servK, Number Ts⦄
∈ parts (spies evs);
¬ expiredSK Ts evs;
A ∉ bad; B ∉ bad; B ≠ Tgs; evs ∈ kerbIV ⟧
⟹ Key servK ∉ analz (spies evs)"
by (blast dest: u_servTicket_authentic u_NotexpiredSK_NotexpiredAK Confidentiality_Tgs_bis)
subsection‹Parties authentication: each party verifies "the identity of
another party who generated some data" (quoted from Neuman and Ts'o).›
text‹These guarantees don't assess whether two parties agree on
the same session key: sending a message containing a key
doesn't a priori state knowledge of the key.›
text‹‹Tgs_authenticates_A› can be found above›
lemma A_authenticates_Tgs:
"⟦ Says Kas A
(Crypt (shrK A) ⦃Key authK, Agent Tgs, Number Ta, authTicket⦄) ∈ set evs;
Crypt authK ⦃Key servK, Agent B, Number Ts, servTicket⦄
∈ parts (spies evs);
Key authK ∉ analz (spies evs);
evs ∈ kerbIV ⟧
⟹ Says Tgs A (Crypt authK ⦃Key servK, Agent B, Number Ts, servTicket⦄)
∈ set evs"
apply (frule Says_Kas_message_form, assumption)
apply (erule rev_mp)
apply (erule rev_mp)
apply (erule rev_mp)
apply (erule kerbIV.induct, analz_mono_contra)
apply (frule_tac [7] K5_msg_in_parts_spies)
apply (frule_tac [5] K3_msg_in_parts_spies, simp_all, blast)
txt‹K2›
apply (blast dest!: servK_authentic Says_Tgs_message_form authKeys_used)
txt‹K4›
apply (blast dest!: unique_CryptKey)
done
lemma B_authenticates_A:
"⟦ Crypt servK ⦃Agent A, Number T3⦄ ∈ parts (spies evs);
Crypt (shrK B) ⦃Agent A, Agent B, Key servK, Number Ts⦄
∈ parts (spies evs);
Key servK ∉ analz (spies evs);
A ∉ bad; B ∉ bad; B ≠ Tgs; evs ∈ kerbIV ⟧
⟹ Says A B ⦃Crypt (shrK B) ⦃Agent A, Agent B, Key servK, Number Ts⦄,
Crypt servK ⦃Agent A, Number T3⦄⦄ ∈ set evs"
by (blast dest: servTicket_authentic_Tgs intro: Says_K5)
text‹The second assumption tells B what kind of key servK is.›
lemma B_authenticates_A_r:
"⟦ Crypt servK ⦃Agent A, Number T3⦄ ∈ parts (spies evs);
Crypt (shrK B) ⦃Agent A, Agent B, Key servK, Number Ts⦄
∈ parts (spies evs);
Crypt authK ⦃Key servK, Agent B, Number Ts, servTicket⦄
∈ parts (spies evs);
Crypt (shrK A) ⦃Key authK, Agent Tgs, Number Ta, authTicket⦄
∈ parts (spies evs);
¬ expiredSK Ts evs; ¬ expiredAK Ta evs;
B ≠ Tgs; A ∉ bad; B ∉ bad; evs ∈ kerbIV ⟧
⟹ Says A B ⦃Crypt (shrK B) ⦃Agent A, Agent B, Key servK, Number Ts⦄,
Crypt servK ⦃Agent A, Number T3⦄ ⦄ ∈ set evs"
by (blast intro: Says_K5 dest: Confidentiality_B servTicket_authentic_Tgs)
text‹‹u_B_authenticates_A› would be the same as ‹B_authenticates_A› because the servK confidentiality assumption is yet unrelaxed›
lemma u_B_authenticates_A_r:
"⟦ Crypt servK ⦃Agent A, Number T3⦄ ∈ parts (spies evs);
Crypt (shrK B) ⦃Agent A, Agent B, Key servK, Number Ts⦄
∈ parts (spies evs);
¬ expiredSK Ts evs;
B ≠ Tgs; A ∉ bad; B ∉ bad; evs ∈ kerbIV ⟧
⟹ Says A B ⦃Crypt (shrK B) ⦃Agent A, Agent B, Key servK, Number Ts⦄,
Crypt servK ⦃Agent A, Number T3⦄ ⦄ ∈ set evs"
by (blast intro: Says_K5 dest: u_Confidentiality_B servTicket_authentic_Tgs)
lemma A_authenticates_B:
"⟦ Crypt servK (Number T3) ∈ parts (spies evs);
Crypt authK ⦃Key servK, Agent B, Number Ts, servTicket⦄
∈ parts (spies evs);
Crypt (shrK A) ⦃Key authK, Agent Tgs, Number Ta, authTicket⦄
∈ parts (spies evs);
Key authK ∉ analz (spies evs); Key servK ∉ analz (spies evs);
A ∉ bad; B ∉ bad; evs ∈ kerbIV ⟧
⟹ Says B A (Crypt servK (Number T3)) ∈ set evs"
by (blast dest: authK_authentic servK_authentic Says_Kas_message_form Key_unique_SesKey K4_imp_K2 intro: Says_K6)
lemma A_authenticates_B_r:
"⟦ Crypt servK (Number T3) ∈ parts (spies evs);
Crypt authK ⦃Key servK, Agent B, Number Ts, servTicket⦄
∈ parts (spies evs);
Crypt (shrK A) ⦃Key authK, Agent Tgs, Number Ta, authTicket⦄
∈ parts (spies evs);
¬ expiredAK Ta evs; ¬ expiredSK Ts evs;
A ∉ bad; B ∉ bad; evs ∈ kerbIV ⟧
⟹ Says B A (Crypt servK (Number T3)) ∈ set evs"
apply (frule authK_authentic)
apply (frule_tac [3] Says_Kas_message_form)
apply (frule_tac [4] Confidentiality_Kas)
apply (frule_tac [7] servK_authentic)
prefer 8 apply blast
apply (erule_tac [9] exE)
apply (frule_tac [9] K4_imp_K2)
apply assumption+
apply (blast dest: Key_unique_SesKey intro!: Says_K6 dest: Confidentiality_Tgs
)
done
subsection‹Key distribution guarantees
An agent knows a session key if he used it to issue a cipher.
These guarantees also convey a stronger form of
authentication - non-injective agreement on the session key›
lemma Kas_Issues_A:
"⟦ Says Kas A (Crypt (shrK A) ⦃Key authK, Peer, Ta, authTicket⦄) ∈ set evs;
evs ∈ kerbIV ⟧
⟹ Kas Issues A with (Crypt (shrK A) ⦃Key authK, Peer, Ta, authTicket⦄)
on evs"
unfolding Issues_def
apply (rule exI)
apply (rule conjI, assumption)
apply (simp (no_asm))
apply (erule rev_mp)
apply (erule kerbIV.induct)
apply (frule_tac [5] Says_ticket_parts)
apply (frule_tac [7] Says_ticket_parts)
apply (simp_all (no_asm_simp) add: all_conj_distrib)
txt‹K2›
apply (simp add: takeWhile_tail)
apply (blast dest: authK_authentic parts_spies_takeWhile_mono [THEN subsetD] parts_spies_evs_revD2 [THEN subsetD])
done
lemma A_authenticates_and_keydist_to_Kas:
"⟦ Crypt (shrK A) ⦃Key authK, Peer, Ta, authTicket⦄ ∈ parts (spies evs);
A ∉ bad; evs ∈ kerbIV ⟧
⟹ Kas Issues A with (Crypt (shrK A) ⦃Key authK, Peer, Ta, authTicket⦄)
on evs"
by (blast dest: authK_authentic Kas_Issues_A)
lemma honest_never_says_newer_timestamp_in_auth:
"⟦ (CT evs) ≤ T; A ∉ bad; Number T ∈ parts {X}; evs ∈ kerbIV ⟧
⟹ ∀ B Y. Says A B ⦃Y, X⦄ ∉ set evs"
apply (erule rev_mp)
apply (erule kerbIV.induct)
apply force+
done
lemma honest_never_says_current_timestamp_in_auth:
"⟦ (CT evs) = T; Number T ∈ parts {X}; evs ∈ kerbIV ⟧
⟹ ∀ A B Y. A ∉ bad ⟶ Says A B ⦃Y, X⦄ ∉ set evs"
by (metis eq_imp_le honest_never_says_newer_timestamp_in_auth)
lemma A_trusts_secure_authenticator:
"⟦ Crypt K ⦃Agent A, Number T⦄ ∈ parts (spies evs);
Key K ∉ analz (spies evs); evs ∈ kerbIV ⟧
⟹ ∃ B X. Says A Tgs ⦃X, Crypt K ⦃Agent A, Number T⦄, Agent B⦄ ∈ set evs ∨
Says A B ⦃X, Crypt K ⦃Agent A, Number T⦄⦄ ∈ set evs"
apply (erule rev_mp)
apply (erule rev_mp)
apply (erule kerbIV.induct, analz_mono_contra)
apply (frule_tac [5] Says_ticket_parts)
apply (frule_tac [7] Says_ticket_parts)
apply (simp_all add: all_conj_distrib)
apply blast+
done
lemma A_Issues_Tgs:
"⟦ Says A Tgs ⦃authTicket, Crypt authK ⦃Agent A, Number T2⦄, Agent B⦄
∈ set evs;
Key authK ∉ analz (spies evs);
A ∉ bad; evs ∈ kerbIV ⟧
⟹ A Issues Tgs with (Crypt authK ⦃Agent A, Number T2⦄) on evs"
unfolding Issues_def
apply (rule exI)
apply (rule conjI, assumption)
apply (simp (no_asm))
apply (erule rev_mp)
apply (erule rev_mp)
apply (erule kerbIV.induct, analz_mono_contra)
apply (frule_tac [5] Says_ticket_parts)
apply (frule_tac [7] Says_ticket_parts)
apply (simp_all (no_asm_simp) add: all_conj_distrib)
txt‹fake›
apply blast
txt‹K3›
apply (simp add: takeWhile_tail)
apply auto
apply (force dest!: authK_authentic Says_Kas_message_form)
apply (drule parts_spies_takeWhile_mono [THEN subsetD, THEN parts_spies_evs_revD2 [THEN subsetD]])
apply (drule A_trusts_secure_authenticator, assumption, assumption)
apply (simp add: honest_never_says_current_timestamp_in_auth)
done
lemma Tgs_authenticates_and_keydist_to_A:
"⟦ Crypt authK ⦃Agent A, Number T2⦄ ∈ parts (spies evs);
Crypt (shrK Tgs) ⦃Agent A, Agent Tgs, Key authK, Number Ta⦄
∈ parts (spies evs);
Key authK ∉ analz (spies evs);
A ∉ bad; evs ∈ kerbIV ⟧
⟹ A Issues Tgs with (Crypt authK ⦃Agent A, Number T2⦄) on evs"
by (blast dest: A_Issues_Tgs Tgs_authenticates_A)
lemma Tgs_Issues_A:
"⟦ Says Tgs A (Crypt authK ⦃Key servK, Agent B, Number Ts, servTicket ⦄)
∈ set evs;
Key authK ∉ analz (spies evs); evs ∈ kerbIV ⟧
⟹ Tgs Issues A with
(Crypt authK ⦃Key servK, Agent B, Number Ts, servTicket ⦄) on evs"
unfolding Issues_def
apply (rule exI)
apply (rule conjI, assumption)
apply (simp (no_asm))
apply (erule rev_mp)
apply (erule rev_mp)
apply (erule kerbIV.induct, analz_mono_contra)
apply (frule_tac [5] Says_ticket_parts)
apply (frule_tac [7] Says_ticket_parts)
apply (simp_all (no_asm_simp) add: all_conj_distrib)
txt‹K4›
apply (simp add: takeWhile_tail)
apply (metis knows_Spy_partsEs(2) parts.Fst usedI used_evs_rev used_takeWhile_used)
done
lemma A_authenticates_and_keydist_to_Tgs:
"⟦Crypt authK ⦃Key servK, Agent B, Number Ts, servTicket⦄ ∈ parts (spies evs);
Key authK ∉ analz (spies evs); B ≠ Tgs; evs ∈ kerbIV ⟧
⟹ ∃A. Tgs Issues A with
(Crypt authK ⦃Key servK, Agent B, Number Ts, servTicket ⦄) on evs"
by (blast dest: Tgs_Issues_A servK_authentic_bis)
lemma B_Issues_A:
"⟦ Says B A (Crypt servK (Number T3)) ∈ set evs;
Key servK ∉ analz (spies evs);
A ∉ bad; B ∉ bad; B ≠ Tgs; evs ∈ kerbIV ⟧
⟹ B Issues A with (Crypt servK (Number T3)) on evs"
unfolding Issues_def
apply (rule exI)
apply (rule conjI, assumption)
apply (simp (no_asm))
apply (erule rev_mp)
apply (erule rev_mp)
apply (erule kerbIV.induct, analz_mono_contra)
apply (frule_tac [5] Says_ticket_parts)
apply (frule_tac [7] Says_ticket_parts)
apply (simp_all (no_asm_simp) add: all_conj_distrib)
apply blast
txt‹K6 requires numerous lemmas›
apply (simp add: takeWhile_tail)
apply (blast dest: servTicket_authentic parts_spies_takeWhile_mono [THEN subsetD] parts_spies_evs_revD2 [THEN subsetD] intro: Says_K6)
done
lemma B_Issues_A_r:
"⟦ Says B A (Crypt servK (Number T3)) ∈ set evs;
Crypt (shrK B) ⦃Agent A, Agent B, Key servK, Number Ts⦄
∈ parts (spies evs);
Crypt authK ⦃Key servK, Agent B, Number Ts, servTicket⦄
∈ parts (spies evs);
Crypt (shrK A) ⦃Key authK, Agent Tgs, Number Ta, authTicket⦄
∈ parts (spies evs);
¬ expiredSK Ts evs; ¬ expiredAK Ta evs;
A ∉ bad; B ∉ bad; B ≠ Tgs; evs ∈ kerbIV ⟧
⟹ B Issues A with (Crypt servK (Number T3)) on evs"
by (blast dest!: Confidentiality_B B_Issues_A)
lemma u_B_Issues_A_r:
"⟦ Says B A (Crypt servK (Number T3)) ∈ set evs;
Crypt (shrK B) ⦃Agent A, Agent B, Key servK, Number Ts⦄
∈ parts (spies evs);
¬ expiredSK Ts evs;
A ∉ bad; B ∉ bad; B ≠ Tgs; evs ∈ kerbIV ⟧
⟹ B Issues A with (Crypt servK (Number T3)) on evs"
by (blast dest!: u_Confidentiality_B B_Issues_A)
lemma A_authenticates_and_keydist_to_B:
"⟦ Crypt servK (Number T3) ∈ parts (spies evs);
Crypt authK ⦃Key servK, Agent B, Number Ts, servTicket⦄
∈ parts (spies evs);
Crypt (shrK A) ⦃Key authK, Agent Tgs, Number Ta, authTicket⦄
∈ parts (spies evs);
Key authK ∉ analz (spies evs); Key servK ∉ analz (spies evs);
A ∉ bad; B ∉ bad; B ≠ Tgs; evs ∈ kerbIV ⟧
⟹ B Issues A with (Crypt servK (Number T3)) on evs"
by (blast dest!: A_authenticates_B B_Issues_A)
lemma A_authenticates_and_keydist_to_B_r:
"⟦ Crypt servK (Number T3) ∈ parts (spies evs);
Crypt authK ⦃Key servK, Agent B, Number Ts, servTicket⦄
∈ parts (spies evs);
Crypt (shrK A) ⦃Key authK, Agent Tgs, Number Ta, authTicket⦄
∈ parts (spies evs);
¬ expiredAK Ta evs; ¬ expiredSK Ts evs;
A ∉ bad; B ∉ bad; B ≠ Tgs; evs ∈ kerbIV ⟧
⟹ B Issues A with (Crypt servK (Number T3)) on evs"
by (blast dest!: A_authenticates_B_r Confidentiality_Serv_A B_Issues_A)
lemma A_Issues_B:
"⟦ Says A B ⦃servTicket, Crypt servK ⦃Agent A, Number T3⦄⦄
∈ set evs;
Key servK ∉ analz (spies evs);
B ≠ Tgs; A ∉ bad; B ∉ bad; evs ∈ kerbIV ⟧
⟹ A Issues B with (Crypt servK ⦃Agent A, Number T3⦄) on evs"
unfolding Issues_def
apply (rule exI)
apply (rule conjI, assumption)
apply (simp (no_asm))
apply (erule rev_mp)
apply (erule rev_mp)
apply (erule kerbIV.induct, analz_mono_contra)
apply (frule_tac [5] Says_ticket_parts)
apply (frule_tac [7] Says_ticket_parts)
apply (simp_all (no_asm_simp))
apply clarify
txt‹K5›
apply auto
apply (simp add: takeWhile_tail)
txt‹Level 15: case analysis necessary because the assumption doesn't state
the form of servTicket. The guarantee becomes stronger.›
apply (blast dest: Says_imp_spies [THEN analz.Inj, THEN analz_Decrypt']
K3_imp_K2 servK_authentic_ter
parts_spies_takeWhile_mono [THEN subsetD]
parts_spies_evs_revD2 [THEN subsetD]
intro: Says_K5)
apply (simp add: takeWhile_tail)
done
lemma A_Issues_B_r:
"⟦ Says A B ⦃servTicket, Crypt servK ⦃Agent A, Number T3⦄⦄
∈ set evs;
Crypt (shrK A) ⦃Key authK, Agent Tgs, Number Ta, authTicket⦄
∈ parts (spies evs);
Crypt authK ⦃Key servK, Agent B, Number Ts, servTicket⦄
∈ parts (spies evs);
¬ expiredAK Ta evs; ¬ expiredSK Ts evs;
B ≠ Tgs; A ∉ bad; B ∉ bad; evs ∈ kerbIV ⟧
⟹ A Issues B with (Crypt servK ⦃Agent A, Number T3⦄) on evs"
by (blast dest!: Confidentiality_Serv_A A_Issues_B)
lemma B_authenticates_and_keydist_to_A:
"⟦ Crypt servK ⦃Agent A, Number T3⦄ ∈ parts (spies evs);
Crypt (shrK B) ⦃Agent A, Agent B, Key servK, Number Ts⦄
∈ parts (spies evs);
Key servK ∉ analz (spies evs);
B ≠ Tgs; A ∉ bad; B ∉ bad; evs ∈ kerbIV ⟧
⟹ A Issues B with (Crypt servK ⦃Agent A, Number T3⦄) on evs"
by (blast dest: B_authenticates_A A_Issues_B)
lemma B_authenticates_and_keydist_to_A_r:
"⟦ Crypt servK ⦃Agent A, Number T3⦄ ∈ parts (spies evs);
Crypt (shrK B) ⦃Agent A, Agent B, Key servK, Number Ts⦄
∈ parts (spies evs);
Crypt authK ⦃Key servK, Agent B, Number Ts, servTicket⦄
∈ parts (spies evs);
Crypt (shrK A) ⦃Key authK, Agent Tgs, Number Ta, authTicket⦄
∈ parts (spies evs);
¬ expiredSK Ts evs; ¬ expiredAK Ta evs;
B ≠ Tgs; A ∉ bad; B ∉ bad; evs ∈ kerbIV ⟧
⟹ A Issues B with (Crypt servK ⦃Agent A, Number T3⦄) on evs"
by (blast dest: B_authenticates_A Confidentiality_B A_Issues_B)
text‹‹u_B_authenticates_and_keydist_to_A› would be the same as ‹B_authenticates_and_keydist_to_A› because the
servK confidentiality assumption is yet unrelaxed›
lemma u_B_authenticates_and_keydist_to_A_r:
"⟦ Crypt servK ⦃Agent A, Number T3⦄ ∈ parts (spies evs);
Crypt (shrK B) ⦃Agent A, Agent B, Key servK, Number Ts⦄
∈ parts (spies evs);
¬ expiredSK Ts evs;
B ≠ Tgs; A ∉ bad; B ∉ bad; evs ∈ kerbIV ⟧
⟹ A Issues B with (Crypt servK ⦃Agent A, Number T3⦄) on evs"
by (blast dest: u_B_authenticates_A_r u_Confidentiality_B A_Issues_B)
end