Theory m3_kerberos5
section ‹Core Kerberos 5 (L3)›
theory m3_kerberos5 imports m2_kerberos "../Refinement/Message"
begin
text ‹
We model the core Kerberos 5 protocol:
\[
\begin{array}{lll}
\mathrm{M1.} & A \rightarrow S: & A, B, Na \\
\mathrm{M2.} & S \rightarrow A: & \{Kab, B, Ts, Na\}_{Kas}, \{Kab, A, Ts\}_{Kbs} \\
\mathrm{M3.} & A \rightarrow B: & \{A, Ta\}_{Kab}, \{Kab, A, Ts\}_{Kbs} \\
\mathrm{M4.} & B \rightarrow A: & \{Ta\}_{Kab} \\
\end{array}
\]
›
text ‹Proof tool configuration. Avoid annoying automatic unfolding of
‹dom›.›
declare domIff [simp, iff del]
subsection ‹Setup›
text ‹Now we can define the initial key knowledge.›
overloading ltkeySetup' ≡ ltkeySetup begin
definition ltkeySetup_def: "ltkeySetup' ≡ {(sharK C, A) | C A. A = C ∨ A = Sv}"
end
lemma corrKey_shrK_bad [simp]: "corrKey = shrK`bad"
by (auto simp add: keySetup_def ltkeySetup_def corrKey_def)
subsection ‹State›
text ‹The secure channels are star-shaped to/from the server. Therefore,
we have only one agent in the relation.›
record m3_state = "m1_state" +
IK :: "msg set"
text ‹Observable state:
@{term "runs"}, @{term "leak"}, @{term "clk"}, and @{term "cache"}.›
type_synonym
m3_obs = "m2_obs"
definition
m3_obs :: "m3_state ⇒ m3_obs" where
"m3_obs s ≡ ⦇ runs = runs s, leak = leak s, clk = clk s, cache = cache s ⦈"
type_synonym
m3_pred = "m3_state set"
type_synonym
m3_trans = "(m3_state × m3_state) set"
subsection ‹Events›
text ‹Protocol events.›
definition
m3_step1 :: "[rid_t, agent, agent, nonce] ⇒ m3_trans"
where
"m3_step1 Ra A B Na ≡ {(s, s1).
Ra ∉ dom (runs s) ∧
Na = Ra$na ∧
s1 = s⦇
runs := (runs s)(Ra ↦ (Init, [A, B], [])),
IK := insert ⦃Agent A, Agent B, Nonce Na⦄ (IK s)
⦈
}"
definition
m3_step2 :: "[rid_t, agent, agent] ⇒ m3_trans"
where
"m3_step2 ≡ m1_step2"
definition
m3_step3 :: "[rid_t, agent, agent, key, nonce, time] ⇒ m3_trans"
where
"m3_step3 Rs A B Kab Na Ts ≡ {(s, s1).
Rs ∉ dom (runs s) ∧
Kab = sesK (Rs$sk) ∧
⦃Agent A, Agent B, Nonce Na⦄ ∈ IK s ∧
Ts = clk s ∧
s1 = s⦇
runs := (runs s)(Rs ↦ (Serv, [A, B], [aNon Na, aNum Ts])),
IK := insert ⦃Crypt (shrK A) ⦃Key Kab, Agent B, Number Ts, Nonce Na⦄,
Crypt (shrK B) ⦃Key Kab, Agent A, Number Ts⦄⦄
(IK s)
⦈
}"
definition
m3_step4 :: "[rid_t, agent, agent, nonce, key, time, time, msg] ⇒ m3_trans"
where
"m3_step4 Ra A B Na Kab Ts Ta X ≡ {(s, s1).
runs s Ra = Some (Init, [A, B], []) ∧
Na = Ra$na ∧
⦃Crypt (shrK A)
⦃Key Kab, Agent B, Number Ts, Nonce Na⦄, X⦄ ∈ IK s ∧
Ta = clk s ∧
clk s < Ts + Ls ∧
s1 = s⦇
runs := (runs s)(Ra ↦ (Init, [A, B], [aKey Kab, aNum Ts, aNum Ta])),
IK := insert ⦃Crypt Kab ⦃Agent A, Number Ta⦄, X⦄ (IK s)
⦈
}"
definition
m3_step5 :: "[rid_t, agent, agent, key, time, time] ⇒ m3_trans"
where
"m3_step5 Rb A B Kab Ts Ta ≡ {(s, s1).
runs s Rb = Some (Resp, [A, B], []) ∧
⦃Crypt Kab ⦃Agent A, Number Ta⦄,
Crypt (shrK B) ⦃Key Kab, Agent A, Number Ts⦄⦄ ∈ IK s ∧
clk s < Ts + Ls ∧
clk s < Ta + La ∧
(B, Kab, Ta) ∉ cache s ∧
s1 = s⦇
runs := (runs s)(Rb ↦ (Resp, [A, B], [aKey Kab, aNum Ts, aNum Ta])),
cache := insert (B, Kab, Ta) (cache s),
IK := insert (Crypt Kab (Number Ta)) (IK s)
⦈
}"
definition
m3_step6 :: "[rid_t, agent, agent, nonce, key, time, time] ⇒ m3_trans"
where
"m3_step6 Ra A B Na Kab Ts Ta ≡ {(s, s').
runs s Ra = Some (Init, [A, B], [aKey Kab, aNum Ts, aNum Ta]) ∧
Na = Ra$na ∧
clk s < Ts + Ls ∧
Crypt Kab (Number Ta) ∈ IK s ∧
s' = s⦇
runs := (runs s)(Ra ↦ (Init, [A, B], [aKey Kab, aNum Ts, aNum Ta, END]))
⦈
}"
text ‹Clock tick event›
definition
m3_tick :: "time ⇒ m3_trans"
where
"m3_tick ≡ m1_tick"
text ‹Purge event: purge cache of expired timestamps›
definition
m3_purge :: "agent ⇒ m3_trans"
where
"m3_purge ≡ m1_purge"
text ‹Session key compromise.›
definition
m3_leak :: "[rid_t, agent, agent, nonce, time] ⇒ m3_trans"
where
"m3_leak Rs A B Na Ts ≡ {(s, s1).
runs s Rs = Some (Serv, [A, B], [aNon Na, aNum Ts]) ∧
(clk s ≥ Ts + Ls) ∧
s1 = s⦇ leak := insert (sesK (Rs$sk), A, B, Na, Ts) (leak s),
IK := insert (Key (sesK (Rs$sk))) (IK s) ⦈
}"
text ‹Intruder fake event. The following "Dolev-Yao" event generates all
intruder-derivable messages.›
definition
m3_DY_fake :: "m3_trans"
where
"m3_DY_fake ≡ {(s, s1).
s1 = s(| IK := synth (analz (IK s)) |)
}"
subsection ‹Transition system›
definition
m3_init :: "m3_pred"
where
"m3_init ≡ { ⦇
runs = Map.empty,
leak = shrK`bad × {undefined},
clk = 0,
cache = {},
IK = Key`shrK`bad
⦈ }"
definition
m3_trans :: "m3_trans" where
"m3_trans ≡ (⋃A B Ra Rb Rs Na Kab Ts Ta T X.
m3_step1 Ra A B Na ∪
m3_step2 Rb A B ∪
m3_step3 Rs A B Kab Na Ts ∪
m3_step4 Ra A B Na Kab Ts Ta X ∪
m3_step5 Rb A B Kab Ts Ta ∪
m3_step6 Ra A B Na Kab Ts Ta ∪
m3_tick T ∪
m3_purge A ∪
m3_leak Rs A B Na Ts ∪
m3_DY_fake ∪
Id
)"
definition
m3 :: "(m3_state, m3_obs) spec" where
"m3 ≡ ⦇
init = m3_init,
trans = m3_trans,
obs = m3_obs
⦈"
lemmas m3_loc_defs =
m3_def m3_init_def m3_trans_def m3_obs_def
m3_step1_def m3_step2_def m3_step3_def m3_step4_def m3_step5_def
m3_step6_def m3_tick_def m3_purge_def m3_leak_def m3_DY_fake_def
lemmas m3_defs = m3_loc_defs m2_defs
subsection ‹Invariants›
text ‹Specialized injection that we can apply more aggressively.›
lemmas analz_Inj_IK = analz.Inj [where H="IK s" for s]
lemmas parts_Inj_IK = parts.Inj [where H="IK s" for s]
declare parts_Inj_IK [dest!]
declare analz_into_parts [dest]
subsubsection ‹inv1: Secrecy of pre-distributed shared keys›
definition
m3_inv1_lkeysec :: "m3_pred"
where
"m3_inv1_lkeysec ≡ {s. ∀C.
(Key (shrK C) ∈ parts (IK s) ⟶ C ∈ bad) ∧
(C ∈ bad ⟶ Key (shrK C) ∈ IK s)
}"
lemmas m3_inv1_lkeysecI = m3_inv1_lkeysec_def [THEN setc_def_to_intro, rule_format]
lemmas m3_inv1_lkeysecE [elim] = m3_inv1_lkeysec_def [THEN setc_def_to_elim, rule_format]
lemmas m3_inv1_lkeysecD = m3_inv1_lkeysec_def [THEN setc_def_to_dest, rule_format]
text ‹Invariance proof.›
lemma PO_m3_inv1_lkeysec_init [iff]:
"init m3 ⊆ m3_inv1_lkeysec"
by (auto simp add: m3_defs intro!: m3_inv1_lkeysecI)
lemma PO_m3_inv1_lkeysec_trans [iff]:
"{m3_inv1_lkeysec} trans m3 {> m3_inv1_lkeysec}"
by (fastforce simp add: PO_hoare_defs m3_defs intro!: m3_inv1_lkeysecI)
lemma PO_m3_inv1_lkeysec [iff]: "reach m3 ⊆ m3_inv1_lkeysec"
by (rule inv_rule_basic) (fast+)
text ‹Useful simplifier lemmas›
lemma m3_inv1_lkeysec_for_parts [simp]:
"⟦ s ∈ m3_inv1_lkeysec ⟧ ⟹ Key (shrK C) ∈ parts (IK s) ⟷ C ∈ bad"
by auto
lemma m3_inv1_lkeysec_for_analz [simp]:
"⟦ s ∈ m3_inv1_lkeysec ⟧ ⟹ Key (shrK C) ∈ analz (IK s) ⟷ C ∈ bad"
by auto
subsubsection ‹inv2: Session keys not used to encrypt other session keys›
text ‹Session keys are not used to encrypt other keys. Proof requires
generalization to sets of session keys.
NOTE: This invariant will be inherted from the corresponding L2 invariant
using the simulation relation.
›
definition
m3_inv2_sesK_compr :: "m3_pred"
where
"m3_inv2_sesK_compr ≡ {s. ∀K KK.
KK ⊆ range sesK ⟶
(Key K ∈ analz (Key`KK ∪ (IK s))) = (K ∈ KK ∨ Key K ∈ analz (IK s))
}"
lemmas m3_inv2_sesK_comprI = m3_inv2_sesK_compr_def [THEN setc_def_to_intro, rule_format]
lemmas m3_inv2_sesK_comprE = m3_inv2_sesK_compr_def [THEN setc_def_to_elim, rule_format]
lemmas m3_inv2_sesK_comprD = m3_inv2_sesK_compr_def [THEN setc_def_to_dest, rule_format]
text ‹Additional lemma›
lemmas insert_commute_Key = insert_commute [where x="Key K" for K]
lemmas m3_inv2_sesK_compr_simps =
m3_inv2_sesK_comprD
m3_inv2_sesK_comprD [where KK="insert Kab KK" for Kab KK, simplified]
m3_inv2_sesK_comprD [where KK="{Kab}" for Kab, simplified]
insert_commute_Key
subsection ‹Refinement›
subsubsection ‹Message abstraction and simulation relation›
text ‹Abstraction function on sets of messages.›
inductive_set
abs_msg :: "msg set ⇒ chmsg set"
for H :: "msg set"
where
am_M1:
"⦃Agent A, Agent B, Nonce N⦄ ∈ H
⟹ Insec A B (Msg [aNon N]) ∈ abs_msg H"
| am_M2a:
"Crypt (shrK C) ⦃Key K, Agent B, Number T, Nonce N⦄ ∈ H
⟹ Secure Sv C (Msg [aKey K, aAgt B, aNum T, aNon N]) ∈ abs_msg H"
| am_M2b:
"Crypt (shrK C) ⦃Key K, Agent A, Number T⦄ ∈ H
⟹ Secure Sv C (Msg [aKey K, aAgt A, aNum T]) ∈ abs_msg H"
| am_M3:
"Crypt K ⦃Agent A, Number T⦄ ∈ H
⟹ dAuth K (Msg [aAgt A, aNum T]) ∈ abs_msg H"
| am_M4:
"Crypt K (Number T) ∈ H
⟹ dAuth K (Msg [aNum T]) ∈ abs_msg H"
text ‹R23: The simulation relation. This is a data refinement of
the insecure and secure channels of refinement 2.›
definition
R23_msgs :: "(m2_state × m3_state) set" where
"R23_msgs ≡ {(s, t). abs_msg (parts (IK t)) ⊆ chan s }"
definition
R23_keys :: "(m2_state × m3_state) set" where
"R23_keys ≡ {(s, t). ∀KK K. KK ⊆ range sesK ⟶
Key K ∈ analz (Key`KK ∪ (IK t)) ⟷ aKey K ∈ extr (aKey`KK ∪ ik0) (chan s)
}"
definition
R23_non :: "(m2_state × m3_state) set" where
"R23_non ≡ {(s, t). ∀KK N. KK ⊆ range sesK ⟶
Nonce N ∈ analz (Key`KK ∪ (IK t)) ⟷ aNon N ∈ extr (aKey`KK ∪ ik0) (chan s)
}"
definition
R23_pres :: "(m2_state × m3_state) set" where
"R23_pres ≡ {(s, t). runs s = runs t ∧ leak s = leak t ∧ clk s = clk t ∧ cache s = cache t}"
definition
R23 :: "(m2_state × m3_state) set" where
"R23 ≡ R23_msgs ∩ R23_keys ∩ R23_non ∩ R23_pres"
lemmas R23_defs =
R23_def R23_msgs_def R23_keys_def R23_non_def R23_pres_def
text ‹The mediator function is the identity here.›
definition
med32 :: "m3_obs ⇒ m2_obs" where
"med32 ≡ id"
lemmas R23_msgsI = R23_msgs_def [THEN rel_def_to_intro, simplified, rule_format]
lemmas R23_msgsE [elim] = R23_msgs_def [THEN rel_def_to_elim, simplified, rule_format]
lemmas R23_msgsE' [elim] = R23_msgs_def [THEN rel_def_to_dest, simplified, rule_format, THEN subsetD]
lemmas R23_keysI = R23_keys_def [THEN rel_def_to_intro, simplified, rule_format]
lemmas R23_keysE [elim] = R23_keys_def [THEN rel_def_to_elim, simplified, rule_format]
lemmas R23_nonI = R23_non_def [THEN rel_def_to_intro, simplified, rule_format]
lemmas R23_nonE [elim] = R23_non_def [THEN rel_def_to_elim, simplified, rule_format]
lemmas R23_presI = R23_pres_def [THEN rel_def_to_intro, simplified, rule_format]
lemmas R23_presE [elim] = R23_pres_def [THEN rel_def_to_elim, simplified, rule_format]
lemmas R23_intros = R23_msgsI R23_keysI R23_nonI R23_presI
text ‹Simplifier lemmas for various instantiations (keys and nonces).›
lemmas R23_keys_simp = R23_keys_def [THEN rel_def_to_dest, simplified, rule_format]
lemmas R23_keys_simps =
R23_keys_simp
R23_keys_simp [where KK="{}", simplified]
R23_keys_simp [where KK="{K'}" for K', simplified]
R23_keys_simp [where KK="insert K' KK" for K' KK, simplified, OF _ conjI]
lemmas R23_non_simp = R23_non_def [THEN rel_def_to_dest, simplified, rule_format]
lemmas R23_non_simps =
R23_non_simp
R23_non_simp [where KK="{}", simplified]
R23_non_simp [where KK="{K}" for K, simplified]
R23_non_simp [where KK="insert K KK" for K KK, simplified, OF _ conjI]
lemmas R23_simps = R23_keys_simps R23_non_simps
subsubsection ‹General lemmas›
text ‹General facts about @{term "abs_msg"}›
declare abs_msg.intros [intro!]
declare abs_msg.cases [elim!]
lemma abs_msg_empty: "abs_msg {} = {}"
by (auto)
lemma abs_msg_Un [simp]:
"abs_msg (G ∪ H) = abs_msg G ∪ abs_msg H"
by (auto)
lemma abs_msg_mono [elim]:
"⟦ m ∈ abs_msg G; G ⊆ H ⟧ ⟹ m ∈ abs_msg H"
by (auto)
lemma abs_msg_insert_mono [intro]:
"⟦ m ∈ abs_msg H ⟧ ⟹ m ∈ abs_msg (insert m' H)"
by (auto)
text ‹Facts about @{term "abs_msg"} concerning abstraction of fakeable
messages. This is crucial for proving the refinement of the intruder event.›
lemma abs_msg_DY_subset_fakeable:
"⟦ (s, t) ∈ R23_msgs; (s, t) ∈ R23_keys; (s, t) ∈ R23_non; t ∈ m3_inv1_lkeysec ⟧
⟹ abs_msg (synth (analz (IK t))) ⊆ fake ik0 (dom (runs s)) (chan s)"
apply (auto)
prefer 2 apply (blast)
prefer 3 apply (blast)
prefer 4 apply (blast)
prefer 5 apply (blast)
apply (intro fake_StatCh fake_DynCh, auto simp add: R23_simps)+
done
subsubsection ‹Refinement proof›
text ‹Pair decomposition. These were set to \texttt{elim!}, which is too
agressive here.›
declare MPair_analz [rule del, elim]
declare MPair_parts [rule del, elim]
text ‹Protocol events.›
lemma PO_m3_step1_refines_m2_step1:
"{R23}
(m2_step1 Ra A B Na), (m3_step1 Ra A B Na)
{> R23}"
by (auto simp add: PO_rhoare_defs R23_def m3_defs intro!: R23_intros) (auto)
lemma PO_m3_step2_refines_m2_step2:
"{R23}
(m2_step2 Rb A B), (m3_step2 Rb A B)
{> R23}"
by (auto simp add: PO_rhoare_defs R23_def m3_defs intro!: R23_intros)
lemma PO_m3_step3_refines_m2_step3:
"{R23 ∩ (m2_inv3a_sesK_compr) × (m3_inv2_sesK_compr ∩ m3_inv1_lkeysec)}
(m2_step3 Rs A B Kab Na Ts), (m3_step3 Rs A B Kab Na Ts)
{> R23}"
proof -
{ fix s t
assume H:
"(s, t) ∈ R23_msgs" "(s, t) ∈ R23_keys" "(s, t) ∈ R23_non"
"(s, t) ∈ R23_pres"
"s ∈ m2_inv3a_sesK_compr"
"t ∈ m3_inv2_sesK_compr" "t ∈ m3_inv1_lkeysec"
"Kab = sesK (Rs$sk)" "Rs ∉ dom (runs t)"
"⦃ Agent A, Agent B, Nonce Na ⦄ ∈ parts (IK t)"
let ?s'=
"s⦇ runs := (runs s)(Rs ↦ (Serv, [A, B], [aNon Na, aNum (clk t)])),
chan := insert (Secure Sv A (Msg [aKey Kab, aAgt B, aNum (clk t), aNon Na]))
(insert (Secure Sv B (Msg [aKey Kab, aAgt A, aNum (clk t)])) (chan s)) ⦈"
let ?t'=
"t⦇ runs := (runs t)(Rs ↦ (Serv, [A, B], [aNon Na, aNum (clk t)])),
IK := insert
⦃ Crypt (shrK A) ⦃ Key Kab, Agent B, Number (clk t), Nonce Na ⦄,
Crypt (shrK B) ⦃ Key Kab, Agent A, Number (clk t) ⦄ ⦄
(IK t) ⦈"
have "(?s', ?t') ∈ R23_msgs" using H
by (-) (rule R23_intros, auto)
moreover
have "(?s', ?t') ∈ R23_keys" using H
by (-) (rule R23_intros,
auto simp add: m2_inv3a_sesK_compr_simps m3_inv2_sesK_compr_simps,
auto simp add: R23_keys_simps)
moreover
have "(?s', ?t') ∈ R23_non" using H
by (-)
(rule R23_intros,
auto simp add: m2_inv3a_sesK_compr_simps m3_inv2_sesK_compr_simps R23_non_simps)
moreover
have "(?s', ?t') ∈ R23_pres" using H
by (-) (rule R23_intros, auto)
moreover
note calculation
}
thus ?thesis
by (auto simp add: PO_rhoare_defs R23_def m3_defs)
qed
lemma PO_m3_step4_refines_m2_step4:
"{R23 ∩ UNIV × m3_inv1_lkeysec}
(m2_step4 Ra A B Na Kab Ts Ta), (m3_step4 Ra A B Na Kab Ts Ta X)
{> R23}"
proof -
{ fix s t
assume H:
"(s, t) ∈ R23_msgs" "(s, t) ∈ R23_keys" "(s, t) ∈ R23_non"
"(s, t) ∈ R23_pres" "t ∈ m3_inv1_lkeysec"
"runs t Ra = Some (Init, [A, B], [])" "Na = Ra$na"
"⦃ Crypt (shrK A) ⦃Key Kab, Agent B, Number Ts, Nonce Na⦄, X⦄ ∈ analz (IK t)"
let ?s' = "s⦇ runs := (runs s)(Ra ↦ (Init, [A, B], [aKey Kab, aNum Ts, aNum (clk t)])),
chan := insert (dAuth Kab (Msg [aAgt A, aNum (clk t)])) (chan s) ⦈"
and ?t' = "t⦇ runs := (runs t)(Ra ↦ (Init, [A, B], [aKey Kab, aNum Ts, aNum (clk t)])),
IK := insert ⦃Crypt Kab ⦃Agent A, Number (clk t)⦄, X⦄ (IK t) ⦈"
from H have
"Secure Sv A (Msg [aKey Kab, aAgt B, aNum Ts, aNon Na]) ∈ chan s"
by (auto dest!: analz_into_parts elim!: MPair_parts)
moreover
from H have "X ∈ parts (IK t)" by (auto)
with H have "(?s', ?t') ∈ R23_msgs" by (auto intro!: R23_intros) (auto)
moreover
from H have "X ∈ analz (IK t)" by (auto)
with H have "(?s', ?t') ∈ R23_keys"
by (auto intro!: R23_intros) (auto dest!: analz_cut intro: analz_monotonic)
moreover
from H have "X ∈ analz (IK t)" by (auto)
with H have "(?s', ?t') ∈ R23_non"
by (auto intro!: R23_intros) (auto dest!: analz_cut intro: analz_monotonic)
moreover
have "(?s', ?t') ∈ R23_pres" using H
by (auto intro!: R23_intros)
moreover
note calculation
}
thus ?thesis
by (auto simp add: PO_rhoare_defs R23_def m3_defs dest!: analz_Inj_IK)
qed
lemma PO_m3_step5_refines_m2_step5:
"{R23}
(m2_step5 Rb A B Kab Ts Ta), (m3_step5 Rb A B Kab Ts Ta)
{> R23}"
by (auto simp add: PO_rhoare_defs R23_def m3_defs intro!: R23_intros)
(auto)
lemma PO_m3_step6_refines_m2_step6:
"{R23}
(m2_step6 Ra A B Na Kab Ts Ta), (m3_step6 Ra A B Na Kab Ts Ta)
{> R23}"
by (auto simp add: PO_rhoare_defs R23_def m3_defs intro!: R23_intros)
lemma PO_m3_tick_refines_m2_tick:
"{R23}
(m2_tick T), (m3_tick T)
{>R23}"
by (auto simp add: PO_rhoare_defs R23_def m3_defs intro!: R23_intros)
lemma PO_m3_purge_refines_m2_purge:
"{R23}
(m2_purge A), (m3_purge A)
{>R23}"
by (auto simp add: PO_rhoare_defs R23_def m3_defs intro!: R23_intros)
text ‹Intruder events.›
lemma PO_m3_leak_refines_m2_leak:
"{R23}
(m2_leak Rs A B Na Ts), (m3_leak Rs A B Na Ts)
{>R23}"
by (auto simp add: PO_rhoare_defs R23_def m3_defs R23_simps intro!: R23_intros)
lemma PO_m3_DY_fake_refines_m2_fake:
"{R23 ∩ m2_inv3a_sesK_compr × (m3_inv2_sesK_compr ∩ m3_inv1_lkeysec)}
m2_fake, m3_DY_fake
{> R23}"
apply (auto simp add: PO_rhoare_defs R23_def m3_defs intro!: R23_intros
del: abs_msg.cases)
apply (auto intro: abs_msg_DY_subset_fakeable [THEN subsetD]
del: abs_msg.cases)
apply (auto simp add: R23_simps)
done
text ‹All together now...›
lemmas PO_m3_trans_refines_m2_trans =
PO_m3_step1_refines_m2_step1 PO_m3_step2_refines_m2_step2
PO_m3_step3_refines_m2_step3 PO_m3_step4_refines_m2_step4
PO_m3_step5_refines_m2_step5 PO_m3_step6_refines_m2_step6
PO_m3_tick_refines_m2_tick PO_m3_purge_refines_m2_purge
PO_m3_leak_refines_m2_leak PO_m3_DY_fake_refines_m2_fake
lemma PO_m3_refines_init_m2 [iff]:
"init m3 ⊆ R23``(init m2)"
by (auto simp add: R23_def m3_defs intro!: R23_intros)
lemma PO_m3_refines_trans_m2 [iff]:
"{R23 ∩ (m2_inv3a_sesK_compr) × (m3_inv2_sesK_compr ∩ m3_inv1_lkeysec)}
(trans m2), (trans m3)
{> R23}"
by (auto simp add: m3_def m3_trans_def m2_def m2_trans_def)
(blast intro!: PO_m3_trans_refines_m2_trans)+
lemma PO_m3_observation_consistent [iff]:
"obs_consistent R23 med32 m2 m3"
by (auto simp add: obs_consistent_def R23_def med32_def m3_defs)
text ‹Refinement result.›
lemma m3_refines_m2 [iff]:
"refines
(R23 ∩ (m2_inv3a_sesK_compr) × (m3_inv1_lkeysec))
med32 m2 m3"
proof -
have "R23 ∩ m2_inv3a_sesK_compr × UNIV ⊆ UNIV × m3_inv2_sesK_compr"
by (auto simp add: R23_def R23_keys_simps intro!: m3_inv2_sesK_comprI)
thus ?thesis
by (-) (rule Refinement_using_invariants, auto)
qed
lemma m3_implements_m2 [iff]:
"implements med32 m2 m3"
by (rule refinement_soundness) (auto)
subsection ‹Inherited invariants›
subsubsection ‹inv3 (derived): Key secrecy for initiator›
definition
m3_inv3_ikk_init :: "m3_state set"
where
"m3_inv3_ikk_init ≡ {s. ∀A B Ra K Ts nl.
runs s Ra = Some (Init, [A, B], aKey K # aNum Ts # nl) ⟶ A ∈ good ⟶ B ∈ good ⟶
Key K ∈ analz (IK s) ⟶
(K, A, B, Ra$na, Ts) ∈ leak s
}"
lemmas m3_inv3_ikk_initI = m3_inv3_ikk_init_def [THEN setc_def_to_intro, rule_format]
lemmas m3_inv3_ikk_initE [elim] = m3_inv3_ikk_init_def [THEN setc_def_to_elim, rule_format]
lemmas m3_inv3_ikk_initD = m3_inv3_ikk_init_def [THEN setc_def_to_dest, rule_format, rotated 1]
lemma PO_m3_inv3_ikk_init: "reach m3 ⊆ m3_inv3_ikk_init"
proof (rule INV_from_Refinement_using_invariants [OF m3_refines_m2])
show "Range (R23 ∩ m2_inv3a_sesK_compr × m3_inv1_lkeysec ∩ m2_inv6_ikk_init × UNIV)
⊆ m3_inv3_ikk_init"
by (fastforce simp add: R23_def R23_keys_simps intro!: m3_inv3_ikk_initI)
qed auto
subsubsection ‹inv4 (derived): Key secrecy for responder›
definition
m3_inv4_ikk_resp :: "m3_state set"
where
"m3_inv4_ikk_resp ≡ {s. ∀A B Rb K Ts nl.
runs s Rb = Some (Resp, [A, B], aKey K # aNum Ts # nl) ⟶ A ∈ good ⟶ B ∈ good ⟶
Key K ∈ analz (IK s) ⟶
(∃Na. (K, A, B, Na, Ts) ∈ leak s)
}"
lemmas m3_inv4_ikk_respI = m3_inv4_ikk_resp_def [THEN setc_def_to_intro, rule_format]
lemmas m3_inv4_ikk_respE [elim] = m3_inv4_ikk_resp_def [THEN setc_def_to_elim, rule_format]
lemmas m3_inv4_ikk_respD = m3_inv4_ikk_resp_def [THEN setc_def_to_dest, rule_format, rotated 1]
lemma PO_m3_inv4_ikk_resp: "reach m3 ⊆ m3_inv4_ikk_resp"
proof (rule INV_from_Refinement_using_invariants [OF m3_refines_m2])
show "Range (R23 ∩ m2_inv3a_sesK_compr × m3_inv1_lkeysec ∩ m2_inv7_ikk_resp × UNIV)
⊆ m3_inv4_ikk_resp"
by (auto simp add: R23_def R23_keys_simps intro!: m3_inv4_ikk_respI)
(elim m2_inv7_ikk_respE, auto)
qed auto
end