Theory m3_nssk_par
section ‹Needham-Schroeder Shared Key, "parallel" variant (L3)›
theory m3_nssk_par imports m2_nssk "../Refinement/Message"
begin
text ‹
We model an abstract version of the Needham-Schroeder Shared Key protocol:
\[
\begin{array}{lll}
\mathrm{M1.} & A \rightarrow S: & A, B, Na \\
\mathrm{M2.} & S \rightarrow A: & \{Na, B, Kab, \{Kab, A\}_{Kbs} \}_{Kas} \\
\mathrm{M3.} & A \rightarrow B: & \{Kab, A\}_{Kbs} \\
\mathrm{M4.} & B \rightarrow A: & \{Nb\}_{Kab} \\
\mathrm{M5.} & A \rightarrow B: & \{Nb - 1 \}_{Kab} \\
\end{array}
\]
We model a "parallel" version of the NSSK protocol:
\[
\begin{array}{lll}
\mathrm{M1.} & A \rightarrow S: & A, B, Na \\
\mathrm{M2.} & S \rightarrow A: & \{Na, B, Kab\}_{Kas} \\
\mathrm{M3.} & S \rightarrow B: & \{Kab, A\}_{Kbs} \\
\mathrm{M4.} & B \rightarrow A: & \{Nb\}_{Kab} \\
\mathrm{M5.} & A \rightarrow B: & \{Nb - 1 \}_{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: agent's local state.›
type_synonym
m3_obs = m2_obs
definition
m3_obs :: "m3_state ⇒ m3_obs" where
"m3_obs s ≡ ⦇ runs = runs s, leak = leak 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 Rb A B ≡ {(s, s1).
Rb ∉ dom (runs s) ∧
s1 = s⦇
runs := (runs s)(Rb ↦ (Resp, [A, B], []))
⦈
}"
definition
m3_step3 :: "[rid_t, agent, agent, nonce, key] ⇒ m3_trans"
where
"m3_step3 Rs A B Na Kab ≡ {(s, s1).
Rs ∉ dom (runs s) ∧
Kab = sesK (Rs$sk) ∧
⦃Agent A, Agent B, Nonce Na⦄ ∈ IK s ∧
s1 = s⦇
runs := (runs s)(Rs ↦ (Serv, [A, B], [aNon Na])),
IK := {Crypt (shrK A) ⦃Nonce Na, Agent B, Key Kab⦄,
Crypt (shrK B) ⦃Key Kab, Agent A⦄} ∪ IK s
⦈
}"
definition
m3_step4 :: "[rid_t, agent, agent, nonce, key] ⇒ m3_trans"
where
"m3_step4 Ra A B Na Kab ≡ {(s, s1).
runs s Ra = Some (Init, [A, B], []) ∧
Na = Ra$na ∧
Crypt (shrK A) ⦃Nonce Na, Agent B, Key Kab⦄ ∈ IK s ∧
s1 = s⦇
runs := (runs s)(Ra ↦ (Init, [A, B], [aKey Kab]))
⦈
}"
definition
m3_step5 :: "[rid_t, agent, agent, nonce, key] ⇒ m3_trans"
where
"m3_step5 Rb A B Nb Kab ≡ {(s, s1).
runs s Rb = Some (Resp, [A, B], []) ∧
Nb = Rb$nb ∧
Crypt (shrK B) ⦃Key Kab, Agent A⦄ ∈ IK s ∧
s1 = s⦇
runs := (runs s)(Rb ↦ (Resp, [A, B], [aKey Kab])),
IK := insert (Crypt Kab (Nonce Nb)) (IK s)
⦈
}"
definition
m3_step6 :: "[rid_t, agent, agent, nonce, nonce, key] ⇒ m3_trans"
where
"m3_step6 Ra A B Na Nb Kab ≡ {(s, s').
runs s Ra = Some (Init, [A, B], [aKey Kab]) ∧
Na = Ra$na ∧
Crypt Kab (Nonce Nb) ∈ IK s ∧
s' = s⦇
runs := (runs s)(Ra ↦ (Init, [A, B], [aKey Kab, aNon Nb])),
IK := insert (Crypt Kab ⦃Nonce Nb, Nonce Nb⦄) (IK s)
⦈
}"
definition
m3_step7 :: "[rid_t, agent, agent, nonce, key] ⇒ m3_trans"
where
"m3_step7 Rb A B Nb Kab ≡ {(s, s').
runs s Rb = Some (Resp, [A, B], [aKey Kab]) ∧
Nb = Rb$nb ∧
Crypt Kab ⦃Nonce Nb, Nonce Nb⦄ ∈ IK s ∧
s' = s⦇
runs := (runs s)(Rb ↦ (Resp, [A, B], [aKey Kab, END]))
⦈
}"
text ‹Session key compromise.›
definition
m3_leak :: "[rid_t, rid_t, rid_t, agent, agent] ⇒ m3_trans"
where
"m3_leak Rs Ra Rb A B ≡ {(s, s1).
runs s Rs = Some (Serv, [A, B], [aNon (Ra$na)]) ∧
runs s Ra = Some (Init, [A, B], [aKey (sesK (Rs$sk)), aNon (Rb$nb)]) ∧
runs s Rb = Some (Resp, [A, B], [aKey (sesK (Rs$sk)), END]) ∧
s1 = s⦇ leak := insert (sesK (Rs$sk), Ra$na, Rb$nb) (leak s),
IK := insert (Key (sesK (Rs$sk))) (IK s) ⦈
}"
text ‹Intruder fake event.›
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_state set"
where
"m3_init ≡ { ⦇
runs = Map.empty,
leak = shrK`bad × {undefined} × {undefined},
IK = Key`shrK`bad
⦈ }"
definition
m3_trans :: "(m3_state × m3_state) set" where
"m3_trans ≡ (⋃Ra Rb Rs A B Na Nb Kab.
m3_step1 Ra A B Na ∪
m3_step2 Rb A B ∪
m3_step3 Rs A B Na Kab ∪
m3_step4 Ra A B Na Kab ∪
m3_step5 Rb A B Nb Kab ∪
m3_step6 Ra A B Na Nb Kab ∪
m3_step7 Rb A B Nb Kab ∪
m3_leak Rs Ra Rb A B ∪
m3_DY_fake ∪
Id
)"
definition
m3 :: "(m3_state, m3_obs) spec" where
"m3 ≡ ⦇
init = m3_init,
trans = m3_trans,
obs = m3_obs
⦈"
lemmas m3_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_step7_def m3_leak_def m3_DY_fake_def
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›
text ‹inv1: Secrecy of long-term keys›
definition
m3_inv1_lkeysec :: "m3_state set"
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 m3_inv1_lkeysec_def)
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_incr) (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 ‹inv7a: 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 derived from the corresponding L2 invariant
using the simulation relation.
›
definition
m3_inv7a_sesK_compr :: "m3_pred"
where
"m3_inv7a_sesK_compr ≡ {s. ∀K KK.
KK ⊆ range sesK ⟶
(Key K ∈ analz (Key`KK ∪ (IK s))) = (K ∈ KK ∨ Key K ∈ analz (IK s))
}"
lemmas m3_inv7a_sesK_comprI = m3_inv7a_sesK_compr_def [THEN setc_def_to_intro, rule_format]
lemmas m3_inv7a_sesK_comprE = m3_inv7a_sesK_compr_def [THEN setc_def_to_elim, rule_format]
lemmas m3_inv7a_sesK_comprD = m3_inv7a_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_inv7a_sesK_compr_simps =
m3_inv7a_sesK_comprD
m3_inv7a_sesK_comprD [where KK="{Kab}" for Kab, simplified]
m3_inv7a_sesK_comprD [where KK="insert Kab KK" for Kab KK, 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 Na⦄ ∈ H
⟹ Insec A B (Msg [aNon Na]) ∈ abs_msg H"
| am_M2:
"Crypt (shrK C) ⦃Nonce N, Agent B, Key K⦄ ∈ H
⟹ Secure Sv C (Msg [aNon N, aAgt B, aKey K]) ∈ abs_msg H"
| am_M3:
"Crypt (shrK C) ⦃Key K, Agent A⦄ ∈ H
⟹ Secure Sv C (Msg [aKey K, aAgt A]) ∈ abs_msg H"
| am_M4:
"Crypt K (Nonce N) ∈ H
⟹ dAuth K (Msg [aNon N]) ∈ abs_msg H"
| am_M5:
"Crypt K ⦃Nonce N, Nonce N'⦄ ∈ H
⟹ dAuth K (Msg [aNon N, aNon N']) ∈ 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}"
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_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_keysD = R23_keys_def [THEN rel_def_to_dest, 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_nonD = R23_non_def [THEN rel_def_to_dest, simplified, rule_format, rotated 2]
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 ‹Further lemmas: general lemma for simplifier and different instantiations.›
lemmas R23_keys_simps =
R23_keysD
R23_keysD [where KK="{}", simplified]
R23_keysD [where KK="{K'}" for K', simplified]
R23_keysD [where KK="insert K' KK" for K' KK, simplified, OF _ conjI]
lemmas R23_non_dests =
R23_nonD
R23_nonD [where KK="{}", simplified]
R23_nonD [where KK="{K}" for K, simplified]
R23_nonD [where KK="insert K KK" for K KK, simplified, OF _ _ conjI]
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_keys_simps dest: R23_non_dests)+
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 m2_defs 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 m2_defs m3_defs intro!: R23_intros)
(auto)
lemma PO_m3_step3_refines_m2_step3:
"{R23 ∩ (m2_inv3a_sesK_compr) × (m3_inv7a_sesK_compr ∩ m3_inv1_lkeysec)}
(m2_step3 Rs A B Na Kab), (m3_step3 Rs A B Na Kab)
{> 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_inv7a_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])),
chan := insert (Secure Sv A (Msg [aNon Na, aAgt B, aKey Kab]))
(insert (Secure Sv B (Msg [aKey Kab, aAgt A])) (chan s)) ⦈"
let ?t'=
"t⦇ runs := (runs t)(Rs ↦ (Serv, [A, B], [aNon Na])),
IK := insert (Crypt (shrK A) ⦃ Nonce Na, Agent B, Key Kab ⦄)
(insert (Crypt (shrK B) ⦃ Key Kab, Agent A ⦄) (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_inv7a_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_inv7a_sesK_compr_simps
dest: R23_non_dests)
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 m2_defs m3_defs)
qed
lemma PO_m3_step4_refines_m2_step4:
"{R23}
(m2_step4 Ra A B Na Kab), (m3_step4 Ra A B Na Kab)
{> R23}"
by (auto simp add: PO_rhoare_defs R23_def m2_defs m3_defs intro!: R23_intros)
(auto)
lemma PO_m3_step5_refines_m2_step5:
"{R23}
(m2_step5 Rb A B Nb Kab), (m3_step5 Rb A B Nb Kab)
{> R23}"
by (auto simp add: PO_rhoare_defs R23_def m2_defs m3_defs intro!: R23_intros)
(auto)
lemma PO_m3_step6_refines_m2_step6:
"{R23}
(m2_step6 Ra A B Na Nb Kab), (m3_step6 Ra A B Na Nb Kab)
{> R23}"
by (auto simp add: PO_rhoare_defs R23_def m2_defs m3_defs intro!: R23_intros)
(auto)
lemma PO_m3_step7_refines_m2_step7:
"{R23}
(m2_step7 Rb A B Nb Kab), (m3_step7 Rb A B Nb Kab)
{> R23}"
by (auto simp add: PO_rhoare_defs R23_def m2_defs m3_defs intro!: R23_intros)
(auto)
text ‹Intruder events.›
lemma PO_m3_leak_refines_m2_leak:
"{R23}
(m2_leak Rs Ra Rb A B), (m3_leak Rs Ra Rb A B)
{>R23}"
by (auto simp add: PO_rhoare_defs R23_def m2_defs m3_defs intro!: R23_intros)
(auto simp add: R23_keys_simps dest: R23_non_dests)
lemma PO_m3_DY_fake_refines_m2_fake:
"{R23 ∩ UNIV × m3_inv1_lkeysec}
m2_fake, m3_DY_fake
{> R23}"
apply (auto simp add: PO_rhoare_defs R23_def m2_defs 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_keys_simps dest: R23_non_dests)
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_step7_refines_m2_step7 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 m2_defs m3_defs intro!: R23_intros)
lemma PO_m3_refines_trans_m2 [iff]:
"{R23 ∩ (m2_inv3a_sesK_compr) × (m3_inv7a_sesK_compr ∩ m3_inv1_lkeysec)}
(trans m2), (trans m3)
{> R23}"
apply (auto simp add: m3_def m3_trans_def m2_def m2_trans_def)
apply (blast intro!: PO_m3_trans_refines_m2_trans)+
done
lemma PO_m3_observation_consistent [iff]:
"obs_consistent R23 med32 m2 m3"
by (auto simp add: obs_consistent_def R23_def med32_def m2_defs 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_inv7a_sesK_compr"
by (auto simp add: R23_def R23_keys_simps intro!: m3_inv7a_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 ‹inv4 (derived): Key secrecy for initiator›
definition
m3_inv4_ikk_init :: "m3_state set"
where
"m3_inv4_ikk_init ≡ {s. ∀Ra K A B al.
runs s Ra = Some (Init, [A, B], aKey K # al) ⟶ A ∈ good ⟶ B ∈ good ⟶
Key K ∈ analz (IK s) ⟶
(∃Nb'. (K, Ra $ na, Nb') ∈ leak s)
}"
lemmas m3_inv4_ikk_initI = m3_inv4_ikk_init_def [THEN setc_def_to_intro, rule_format]
lemmas m3_inv4_ikk_initE [elim] = m3_inv4_ikk_init_def [THEN setc_def_to_elim, rule_format]
lemmas m3_inv4_ikk_initD = m3_inv4_ikk_init_def [THEN setc_def_to_dest, rule_format, rotated 1]
lemma PO_m3_inv4_ikk_init: "reach m3 ⊆ m3_inv4_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_inv4_ikk_init"
by (auto simp add: R23_def R23_pres_def R23_keys_simps intro!: m3_inv4_ikk_initI)
qed auto
subsubsection ‹inv5 (derived): Key secrecy for responder›
definition
m3_inv5_ikk_resp :: "m3_state set"
where
"m3_inv5_ikk_resp ≡ {s. ∀Rb K A B al.
runs s Rb = Some (Resp, [A, B], aKey K # al) ⟶ A ∈ good ⟶ B ∈ good ⟶
Key K ∈ analz (IK s) ⟶
K ∈ Domain (leak s)
}"
lemmas m3_inv5_ikk_respI = m3_inv5_ikk_resp_def [THEN setc_def_to_intro, rule_format]
lemmas m3_inv5_ikk_respE [elim] = m3_inv5_ikk_resp_def [THEN setc_def_to_elim, rule_format]
lemmas m3_inv5_ikk_respD = m3_inv5_ikk_resp_def [THEN setc_def_to_dest, rule_format, rotated 1]
lemma PO_m3_inv4_ikk_resp: "reach m3 ⊆ m3_inv5_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_inv5_ikk_resp"
by (auto simp add: R23_def R23_pres_def R23_keys_simps intro!: m3_inv5_ikk_respI)
(elim m2_inv7_ikk_respE, auto)
qed auto
end