Theory pfslvl3
section ‹Key Transport Protocol with PFS (L3 locale)›
theory pfslvl3
imports pfslvl2 Implem_lemmas
begin
subsection ‹State and Events›
text ‹Level 3 state›
text ‹(The types have to be defined outside the locale.)›
record l3_state = l1_state +
bad :: "agent set"
type_synonym l3_obs = "l3_state"
type_synonym
l3_pred = "l3_state set"
type_synonym
l3_trans = "(l3_state × l3_state) set"
text ‹attacker event›
definition
l3_dy :: "msg ⇒ l3_trans"
where
"l3_dy ≡ ik_dy"
text ‹compromise events›
definition
l3_lkr_others :: "agent ⇒ l3_trans"
where
"l3_lkr_others A ≡ {(s,s').
A ≠ test_owner ∧
A ≠ test_partner ∧
s' = s⦇bad := {A} ∪ bad s,
ik := keys_of A ∪ ik s⦈
}"
definition
l3_lkr_actor :: "agent ⇒ l3_trans"
where
"l3_lkr_actor A ≡ {(s,s').
A = test_owner ∧
A ≠ test_partner ∧
s' = s⦇bad := {A} ∪ bad s,
ik := keys_of A ∪ ik s⦈
}"
definition
l3_lkr_after :: "agent ⇒ l3_trans"
where
"l3_lkr_after A ≡ {(s,s').
test_ended s ∧
s' = s⦇bad := {A} ∪ bad s,
ik := keys_of A ∪ ik s⦈
}"
definition
l3_skr :: "rid_t ⇒ msg ⇒ l3_trans"
where
"l3_skr R K ≡ {(s,s').
R ≠ test ∧ R ∉ partners ∧
in_progress (progress s R) xsk ∧
guessed_frame R xsk = Some K ∧
s' = s⦇ik := {K} ∪ ik s⦈
}"
text ‹New locale for the level 3 protocol›
text ‹This locale does not add new assumptions, it is only used to separate the level 3
protocol from the implementation locale.›
locale pfslvl3 = valid_implem
begin
text ‹protocol events›
definition
l3_step1 :: "rid_t ⇒ agent ⇒ agent ⇒ l3_trans"
where
"l3_step1 Ra A B ≡ {(s, s').
Ra ∉ dom (progress s) ∧
guessed_runs Ra = ⦇role=Init, owner=A, partner=B⦈ ∧
s' = s⦇
progress := (progress s)(Ra ↦ {xpkE, xskE}),
ik := {implAuth A B ⟨Number 0, epubKF (Ra$kE)⟩} ∪ (ik s)
⦈
}"
definition
l3_step2 :: "rid_t ⇒ agent ⇒ agent ⇒ msg ⇒ l3_trans"
where
"l3_step2 Rb A B KE ≡ {(s, s').
guessed_runs Rb = ⦇role=Resp, owner=B, partner=A⦈ ∧
Rb ∉ dom (progress s) ∧
guessed_frame Rb xpkE = Some KE ∧
implAuth A B ⟨Number 0, KE⟩ ∈ ik s ∧
s' = s⦇
progress := (progress s)(Rb ↦ {xpkE, xsk}),
ik := {implAuth B A (Aenc (NonceF (Rb$sk)) KE)} ∪ (ik s),
signals := if can_signal s A B then
addSignal (signals s) (Running A B ⟨KE, NonceF (Rb$sk)⟩)
else
signals s,
secret := {x. x = NonceF (Rb$sk) ∧ Rb = test} ∪ secret s
⦈
}"
definition
l3_step3 :: "rid_t ⇒ agent ⇒ agent ⇒ msg ⇒ l3_trans"
where
"l3_step3 Ra A B K ≡ {(s, s').
guessed_runs Ra = ⦇role=Init, owner=A, partner=B⦈ ∧
progress s Ra = Some {xpkE, xskE} ∧
guessed_frame Ra xsk = Some K ∧
implAuth B A (Aenc K (epubKF (Ra$kE))) ∈ ik s ∧
s' = s⦇ progress := (progress s)(Ra ↦ {xpkE, xskE, xsk}),
signals := if can_signal s A B then
addSignal (signals s) (Commit A B ⟨epubKF (Ra$kE), K⟩)
else
signals s,
secret := {x. x = K ∧ Ra = test} ∪ secret s
⦈
}"
text ‹specification›
text ‹initial compromise›
definition
ik_init :: "msg set"
where
"ik_init ≡ {priK C |C. C ∈ bad_init} ∪ {pubK A | A. True} ∪
{shrK A B |A B. A ∈ bad_init ∨ B ∈ bad_init} ∪ Tags"
text ‹lemmas about @{term "ik_init"}›
lemma parts_ik_init [simp]: "parts ik_init = ik_init"
by (auto elim!: parts.induct, auto simp add: ik_init_def)
lemma analz_ik_init [simp]: "analz ik_init = ik_init"
by (auto dest: analz_into_parts)
lemma abs_ik_init [iff]: "abs ik_init = {}"
apply (auto elim!: absE)
apply (auto simp add: ik_init_def)
done
lemma payloadSet_ik_init [iff]: "ik_init ∩ payload = {}"
by (auto simp add: ik_init_def)
lemma validSet_ik_init [iff]: "ik_init ∩ valid = {}"
by (auto simp add: ik_init_def)
definition
l3_init :: "l3_state set"
where
"l3_init ≡ { ⦇
ik = ik_init,
secret = {},
progress = Map.empty,
signals = λx. 0,
bad = bad_init
⦈}"
lemmas l3_init_defs = l3_init_def ik_init_def
definition
l3_trans :: "l3_trans"
where
"l3_trans ≡ (⋃m M KE Rb Ra A B K.
l3_step1 Ra A B ∪
l3_step2 Rb A B KE ∪
l3_step3 Ra A B m ∪
l3_dy M ∪
l3_lkr_others A ∪
l3_lkr_after A ∪
l3_skr Ra K ∪
Id
)"
definition
l3 :: "(l3_state, l3_obs) spec" where
"l3 ≡ ⦇
init = l3_init,
trans = l3_trans,
obs = id
⦈"
lemmas l3_loc_defs =
l3_step1_def l3_step2_def l3_step3_def
l3_def l3_init_defs l3_trans_def
l3_dy_def
l3_lkr_others_def l3_lkr_after_def l3_skr_def
lemmas l3_defs = l3_loc_defs ik_dy_def
lemmas l3_nostep_defs = l3_def l3_init_def l3_trans_def
lemma l3_obs_id [simp]: "obs l3 = id"
by (simp add: l3_def)
subsection ‹Invariants›
subsubsection ‹inv1: No long-term keys as message parts›
definition
l3_inv1 :: "l3_state set"
where
"l3_inv1 ≡ {s.
parts (ik s) ∩ range LtK ⊆ ik s
}"
lemmas l3_inv1I = l3_inv1_def [THEN setc_def_to_intro, rule_format]
lemmas l3_inv1E [elim] = l3_inv1_def [THEN setc_def_to_elim, rule_format]
lemmas l3_inv1D = l3_inv1_def [THEN setc_def_to_dest, rule_format]
lemma l3_inv1D' [dest]: "⟦ LtK K ∈ parts (ik s); s ∈ l3_inv1⟧ ⟹ LtK K ∈ ik s"
by (auto simp add: l3_inv1_def)
lemma l3_inv1_init [iff]:
"init l3 ⊆ l3_inv1"
by (auto simp add: l3_def l3_init_def intro!:l3_inv1I)
lemma l3_inv1_trans [iff]:
"{l3_inv1} trans l3 {> l3_inv1}"
apply (auto simp add: PO_hoare_defs l3_nostep_defs intro!: l3_inv1I)
apply (auto simp add: l3_defs dy_fake_msg_def dy_fake_chan_def
parts_insert [where H="ik _"] parts_insert [where H="insert _ (ik _)"]
dest!: Fake_parts_insert)
apply (auto dest:analz_into_parts)
done
lemma PO_l3_inv1 [iff]:
"reach l3 ⊆ l3_inv1"
by (rule inv_rule_basic) (auto)
subsubsection ‹inv2: @{term "bad s"} indeed contains "bad" keys›
definition
l3_inv2 :: "l3_state set"
where
"l3_inv2 ≡ {s.
Keys_bad (ik s) (bad s)
}"
lemmas l3_inv2I = l3_inv2_def [THEN setc_def_to_intro, rule_format]
lemmas l3_inv2E [elim] = l3_inv2_def [THEN setc_def_to_elim, rule_format]
lemmas l3_inv2D = l3_inv2_def [THEN setc_def_to_dest, rule_format]
lemma l3_inv2_init [simp,intro!]:
"init l3 ⊆ l3_inv2"
by (auto simp add: l3_def l3_init_defs intro!:l3_inv2I Keys_badI)
lemma l3_inv2_trans [simp,intro!]:
"{l3_inv2 ∩ l3_inv1} trans l3 {> l3_inv2}"
apply (auto simp add: PO_hoare_defs l3_nostep_defs intro!: l3_inv2I)
apply (auto simp add: l3_defs dy_fake_msg_def dy_fake_chan_def)
text ‹4 subgoals: dy, lkr*, skr›
apply (auto intro: Keys_bad_insert_Fake Keys_bad_insert_keys_of)
apply (auto intro!: Keys_bad_insert_payload)
done
lemma PO_l3_inv2 [iff]: "reach l3 ⊆ l3_inv2"
by (rule_tac J="l3_inv1" in inv_rule_incr) (auto)
subsubsection ‹inv3›
text ‹If a message can be analyzed from the intruder knowledge then it can
be derived (using synth/analz) from the sets of implementation, non-implementation, and
long-term key messages and the tags. That is, intermediate messages are not needed.
›
definition
l3_inv3 :: "l3_state set"
where
"l3_inv3 ≡ {s.
analz (ik s) ⊆
synth (analz ((ik s ∩ payload) ∪ ((ik s) ∩ valid) ∪ (ik s ∩ range LtK) ∪ Tags))
}"
lemmas l3_inv3I = l3_inv3_def [THEN setc_def_to_intro, rule_format]
lemmas l3_inv3E = l3_inv3_def [THEN setc_def_to_elim, rule_format]
lemmas l3_inv3D = l3_inv3_def [THEN setc_def_to_dest, rule_format]
lemma l3_inv3_init [iff]:
"init l3 ⊆ l3_inv3"
apply (auto simp add: l3_def l3_init_def intro!: l3_inv3I)
apply (auto simp add: ik_init_def intro!: synth_increasing [THEN [2] rev_subsetD])
done
declare domIff [iff del]
text ‹Most of the cases in this proof are simple and very similar.
The proof could probably be shortened.›
lemma l3_inv3_trans [simp,intro!]:
"{l3_inv3} trans l3 {> l3_inv3}"
proof (simp add: l3_nostep_defs, safe)
fix Ra A B
show "{l3_inv3} l3_step1 Ra A B {> l3_inv3}"
apply (auto simp add: PO_hoare_def l3_defs intro!: l3_inv3I dest!: l3_inv3D)
apply (auto intro!: validI dest!: analz_insert_partition [THEN [2] rev_subsetD])
done
next
fix Rb A B KE
show "{l3_inv3} l3_step2 Rb A B KE {> l3_inv3}"
apply (auto simp add: PO_hoare_def l3_defs intro!: l3_inv3I dest!: l3_inv3D)
apply (auto intro!: validI dest!: analz_insert_partition [THEN [2] rev_subsetD])
done
next
fix Ra A B K
show "{l3_inv3} l3_step3 Ra A B K {> l3_inv3}"
apply (auto simp add: PO_hoare_def l3_defs intro!: l3_inv3I dest!: l3_inv3D)
done
next
fix m
show "{l3_inv3} l3_dy m {> l3_inv3}"
apply (auto simp add: PO_hoare_def l3_defs dy_fake_chan_def dy_fake_msg_def
intro!: l3_inv3I dest!: l3_inv3D)
apply (drule synth_analz_insert)
apply (blast intro: synth_analz_monotone dest: synth_monotone)
done
next
fix A
show "{l3_inv3} l3_lkr_others A {> l3_inv3}"
apply (auto simp add: PO_hoare_def l3_defs intro!: l3_inv3I dest!: l3_inv3D)
apply (drule analz_Un_partition [of _ "keys_of A"], auto)
done
next
fix A
show "{l3_inv3} l3_lkr_after A {> l3_inv3}"
apply (auto simp add: PO_hoare_def l3_defs intro!: l3_inv3I dest!: l3_inv3D)
apply (drule analz_Un_partition [of _ "keys_of A"], auto)
done
next
fix R K
show "{l3_inv3} l3_skr R K {> l3_inv3}"
apply (auto simp add: PO_hoare_def l3_defs intro!: l3_inv3I dest!: l3_inv3D)
apply (auto dest!: analz_insert_partition [THEN [2] rev_subsetD])
done
qed
lemma PO_l3_inv3 [iff]: "reach l3 ⊆ l3_inv3"
by (rule inv_rule_basic) (auto)
subsubsection ‹inv4: the intruder knows the tags›
definition
l3_inv4 :: "l3_state set"
where
"l3_inv4 ≡ {s.
Tags ⊆ ik s
}"
lemmas l3_inv4I = l3_inv4_def [THEN setc_def_to_intro, rule_format]
lemmas l3_inv4E [elim] = l3_inv4_def [THEN setc_def_to_elim, rule_format]
lemmas l3_inv4D = l3_inv4_def [THEN setc_def_to_dest, rule_format]
lemma l3_inv4_init [simp,intro!]:
"init l3 ⊆ l3_inv4"
by (auto simp add: l3_def l3_init_def ik_init_def intro!:l3_inv4I)
lemma l3_inv4_trans [simp,intro!]:
"{l3_inv4} trans l3 {> l3_inv4}"
apply (auto simp add: PO_hoare_defs l3_nostep_defs intro!: l3_inv4I)
apply (auto simp add: l3_defs dy_fake_chan_def dy_fake_msg_def)
done
lemma PO_l3_inv4 [simp,intro!]: "reach l3 ⊆ l3_inv4"
by (rule inv_rule_basic) (auto)
text ‹The remaining invariants are derived from the others.
They are not protocol dependent provided the previous invariants hold.›
subsubsection ‹inv5›
text ‹The messages that the L3 DY intruder can derive from the intruder knowledge
(using @{term "synth"}/@{term "analz"}), are either implementations or intermediate messages or
can also be derived by the L2 intruder from the set
@{term "extr (bad s) ((ik s) ∩ payload) (abs (ik s))"}, that is, given the
non-implementation messages and the abstractions of (implementation) messages
in the intruder knowledge.
›
definition
l3_inv5 :: "l3_state set"
where
"l3_inv5 ≡ {s.
synth (analz (ik s)) ⊆
dy_fake_msg (bad s) (ik s ∩ payload) (abs (ik s)) ∪ -payload
}"
lemmas l3_inv5I = l3_inv5_def [THEN setc_def_to_intro, rule_format]
lemmas l3_inv5E = l3_inv5_def [THEN setc_def_to_elim, rule_format]
lemmas l3_inv5D = l3_inv5_def [THEN setc_def_to_dest, rule_format]
lemma l3_inv5_derived: "l3_inv2 ∩ l3_inv3 ⊆ l3_inv5"
by (auto simp add: abs_validSet dy_fake_msg_def intro!: l3_inv5I
dest!: l3_inv3D [THEN synth_mono, THEN [2] rev_subsetD]
dest!: synth_analz_NI_I_K_synth_analz_NI_E [THEN [2] rev_subsetD])
lemma PO_l3_inv5 [simp,intro!]: "reach l3 ⊆ l3_inv5"
using l3_inv5_derived PO_l3_inv2 PO_l3_inv3
by blast
subsubsection ‹inv6›
text ‹If the level 3 intruder can deduce a message implementing an insecure channel message, then:
\begin{itemize}
\item either the message is already in the intruder knowledge;
\item or the message is constructed, and the payload can also be deduced by the intruder.
\end{itemize}
›
definition
l3_inv6 :: "l3_state set"
where
"l3_inv6 ≡ {s. ∀ A B M.
(implInsec A B M ∈ synth (analz (ik s)) ∧ M ∈ payload) ⟶
(implInsec A B M ∈ ik s ∨ M ∈ synth (analz (ik s)))
}"
lemmas l3_inv6I = l3_inv6_def [THEN setc_def_to_intro, rule_format]
lemmas l3_inv6E = l3_inv6_def [THEN setc_def_to_elim, rule_format]
lemmas l3_inv6D = l3_inv6_def [THEN setc_def_to_dest, rule_format]
lemma l3_inv6_derived [simp,intro!]:
"l3_inv3 ∩ l3_inv4 ⊆ l3_inv6"
apply (auto intro!: l3_inv6I dest!: l3_inv3D)
text ‹1 subgoal›
apply (drule synth_mono, simp, drule subsetD, assumption)
apply (auto dest!: implInsec_synth_analz [rotated 1, where H="_ ∪ _"])
apply (auto dest!: synth_analz_monotone [of _ "_ ∪ _" "ik _"])
done
lemma PO_l3_inv6 [simp,intro!]: "reach l3 ⊆ l3_inv6"
using l3_inv6_derived PO_l3_inv3 PO_l3_inv4
by (blast)
subsubsection ‹inv7›
text ‹If the level 3 intruder can deduce a message implementing a confidential channel message,
then:
\begin{itemize}
\item either the message is already in the intruder knowledge;
\item or the message is constructed, and the payload can also be deduced by the intruder.
\end{itemize}
›
definition
l3_inv7 :: "l3_state set"
where
"l3_inv7 ≡ {s. ∀ A B M.
(implConfid A B M ∈ synth (analz (ik s)) ∧ M ∈ payload) ⟶
(implConfid A B M ∈ ik s ∨ M ∈ synth (analz (ik s)))
}"
lemmas l3_inv7I = l3_inv7_def [THEN setc_def_to_intro, rule_format]
lemmas l3_inv7E = l3_inv7_def [THEN setc_def_to_elim, rule_format]
lemmas l3_inv7D = l3_inv7_def [THEN setc_def_to_dest, rule_format]
lemma l3_inv7_derived [simp,intro!]:
"l3_inv3 ∩ l3_inv4 ⊆ l3_inv7"
apply (auto intro!: l3_inv7I dest!: l3_inv3D)
text ‹1 subgoal›
apply (drule synth_mono, simp, drule subsetD, assumption)
apply (auto dest!: implConfid_synth_analz [rotated 1, where H="_ ∪ _"])
apply (auto dest!: synth_analz_monotone [of _ "_ ∪ _" "ik _"])
done
lemma PO_l3_inv7 [simp,intro!]: "reach l3 ⊆ l3_inv7"
using l3_inv7_derived PO_l3_inv3 PO_l3_inv4
by (blast)
subsubsection ‹inv8›
text ‹If the level 3 intruder can deduce a message implementing an authentic channel message then:
\begin{itemize}
\item either the message is already in the intruder knowledge;
\item or the message is constructed, and in this case the payload can also be deduced
by the intruder, and one of the agents is bad.
\end{itemize}
›
definition
l3_inv8 :: "l3_state set"
where
"l3_inv8 ≡ {s. ∀ A B M.
(implAuth A B M ∈ synth (analz (ik s)) ∧ M ∈ payload) ⟶
(implAuth A B M ∈ ik s ∨ (M ∈ synth (analz (ik s)) ∧ (A ∈ bad s ∨ B ∈ bad s)))
}"
lemmas l3_inv8I = l3_inv8_def [THEN setc_def_to_intro, rule_format]
lemmas l3_inv8E = l3_inv8_def [THEN setc_def_to_elim, rule_format]
lemmas l3_inv8D = l3_inv8_def [THEN setc_def_to_dest, rule_format]
lemma l3_inv8_derived [iff]:
"l3_inv2 ∩ l3_inv3 ∩ l3_inv4 ⊆ l3_inv8"
apply (auto intro!: l3_inv8I dest!: l3_inv3D l3_inv2D)
text ‹2 subgoals: M is deducible and the agents are bad›
apply (drule synth_mono, simp, drule subsetD, assumption)
apply (auto dest!: implAuth_synth_analz [rotated 1, where H="_ ∪ _"] elim!: synth_analz_monotone)
apply (drule synth_mono, simp, drule subsetD, assumption)
apply (auto dest!: implAuth_synth_analz [rotated 1, where H="_ ∪ _"])
done
lemma PO_l3_inv8 [iff]: "reach l3 ⊆ l3_inv8"
using l3_inv8_derived
PO_l3_inv3 PO_l3_inv2 PO_l3_inv4
by blast
subsubsection ‹inv9›
text ‹If the level 3 intruder can deduce a message implementing a secure channel message then:
\begin{itemize}
\item either the message is already in the intruder knowledge;
\item or the message is constructed, and in this case the payload can also be deduced
by the intruder, and one of the agents is bad.
\end{itemize}
›
definition
l3_inv9 :: "l3_state set"
where
"l3_inv9 ≡ {s. ∀ A B M.
(implSecure A B M ∈ synth (analz (ik s)) ∧ M ∈ payload) ⟶
(implSecure A B M ∈ ik s ∨ (M ∈ synth (analz (ik s)) ∧ (A ∈ bad s ∨ B ∈ bad s)))
}"
lemmas l3_inv9I = l3_inv9_def [THEN setc_def_to_intro, rule_format]
lemmas l3_inv9E = l3_inv9_def [THEN setc_def_to_elim, rule_format]
lemmas l3_inv9D = l3_inv9_def [THEN setc_def_to_dest, rule_format]
lemma l3_inv9_derived [iff]:
"l3_inv2 ∩ l3_inv3 ∩ l3_inv4 ⊆ l3_inv9"
apply (auto intro!: l3_inv9I dest!:l3_inv3D l3_inv2D)
text ‹2 subgoals: M is deducible and the agents are bad›
apply (drule synth_mono, simp, drule subsetD, assumption)
apply (auto dest!: implSecure_synth_analz [rotated 1, where H="_ ∪ _"] elim!: synth_analz_monotone)
apply (drule synth_mono, simp, drule subsetD, assumption)
apply (auto dest!: implSecure_synth_analz [rotated 1, where H="_ ∪ _"])
done
lemma PO_l3_inv9 [iff]: "reach l3 ⊆ l3_inv9"
using l3_inv9_derived
PO_l3_inv3 PO_l3_inv2 PO_l3_inv4
by blast
subsection ‹Refinement›
text ‹mediator function›
definition
med23s :: "l3_obs ⇒ l2_obs"
where
"med23s t ≡ ⦇
ik = ik t ∩ payload,
secret = secret t,
progress = progress t,
signals = signals t,
chan = abs (ik t),
bad = bad t
⦈"
text ‹relation between states›
definition
R23s :: "(l2_state * l3_state) set"
where
"R23s ≡ {(s, s').
s = med23s s'
}"
lemmas R23s_defs = R23s_def med23s_def
lemma R23sI:
"⟦ ik s = ik t ∩ payload; secret s = secret t; progress s = progress t; signals s = signals t;
chan s = abs (ik t); l2_state.bad s = bad t ⟧
⟹ (s, t) ∈ R23s"
by (auto simp add: R23s_def med23s_def)
lemma R23sD:
"(s, t) ∈ R23s ⟹
ik s = ik t ∩ payload ∧ secret s = secret t ∧ progress s = progress t ∧ signals s = signals t ∧
chan s = abs (ik t) ∧ l2_state.bad s = bad t"
by (auto simp add: R23s_def med23s_def)
lemma R23sE [elim]:
"⟦ (s, t) ∈ R23s;
⟦ ik s = ik t ∩ payload; secret s = secret t; progress s = progress t; signals s = signals t;
chan s = abs (ik t); l2_state.bad s = bad t ⟧ ⟹ P ⟧
⟹ P"
by (auto simp add: R23s_def med23s_def)
lemma can_signal_R23 [simp]:
"(s2, s3) ∈ R23s ⟹
can_signal s2 A B ⟷ can_signal s3 A B"
by (auto simp add: can_signal_def)
subsubsection ‹Protocol events›
lemma l3_step1_refines_step1:
"{R23s} l2_step1 Ra A B, l3_step1 Ra A B {>R23s}"
apply (auto simp add: PO_rhoare_defs R23s_defs)
apply (auto simp add: l3_defs l2_step1_def)
done
lemma l3_step2_refines_step2:
"{R23s} l2_step2 Rb A B KE, l3_step2 Rb A B KE{>R23s}"
apply (auto simp add: PO_rhoare_defs R23s_defs l2_step2_def)
apply (auto simp add: l3_step2_def)
done
lemma l3_step3_refines_step3:
"{R23s} l2_step3 Ra A B K, l3_step3 Ra A B K {>R23s}"
apply (auto simp add: PO_rhoare_defs R23s_defs l2_step3_def)
apply (auto simp add: l3_step3_def)
done
subsubsection ‹Intruder events›
lemma l3_dy_payload_refines_dy_fake_msg:
"M ∈ payload ⟹
{R23s ∩ UNIV × l3_inv5} l2_dy_fake_msg M, l3_dy M {>R23s}"
apply (auto simp add: PO_rhoare_defs R23s_defs)
apply (auto simp add: l3_defs l2_dy_fake_msg_def dest: l3_inv5D)
done
lemma l3_dy_valid_refines_dy_fake_chan:
"⟦ M ∈ valid; M' ∈ abs {M} ⟧ ⟹
{R23s ∩ UNIV × (l3_inv5 ∩ l3_inv6 ∩ l3_inv7 ∩ l3_inv8 ∩ l3_inv9)}
l2_dy_fake_chan M', l3_dy M
{>R23s}"
apply (auto simp add: PO_rhoare_defs R23s_defs, simp add: l2_dy_fake_chan_def)
apply (auto simp add: l3_defs)
text ‹1 subgoal›
apply (erule valid_cases, simp_all add: dy_fake_chan_def)
text ‹Insec›
apply (blast dest: l3_inv6D l3_inv5D)
text ‹Confid›
apply (blast dest: l3_inv7D l3_inv5D)
text ‹Auth›
apply (blast dest: l3_inv8D l3_inv5D)
text ‹Secure›
apply (blast dest: l3_inv9D l3_inv5D)
done
lemma l3_dy_valid_refines_dy_fake_chan_Un:
"M ∈ valid ⟹
{R23s ∩ UNIV × (l3_inv5 ∩ l3_inv6 ∩ l3_inv7 ∩ l3_inv8 ∩ l3_inv9)}
⋃M'. l2_dy_fake_chan M', l3_dy M
{>R23s}"
by (auto dest: valid_abs intro: l3_dy_valid_refines_dy_fake_chan)
lemma l3_dy_isLtKey_refines_skip:
"{R23s} Id, l3_dy (LtK ltk) {>R23s}"
apply (auto simp add: PO_rhoare_defs R23s_defs l3_defs)
apply (auto elim!: absE)
done
lemma l3_dy_others_refines_skip:
"⟦ M ∉ range LtK; M ∉ valid; M ∉ payload ⟧ ⟹
{R23s} Id, l3_dy M {>R23s}"
apply (auto simp add: PO_rhoare_defs R23s_defs)
apply (auto simp add: l3_defs)
apply (auto elim!: absE intro: validI)
done
lemma l3_dy_refines_dy_fake_msg_dy_fake_chan_skip:
"{R23s ∩ UNIV × (l3_inv5 ∩ l3_inv6 ∩ l3_inv7 ∩ l3_inv8 ∩ l3_inv9)}
l2_dy_fake_msg M ∪ (⋃M'. l2_dy_fake_chan M') ∪ Id, l3_dy M
{>R23s}"
by (cases "M ∈ payload ∪ valid ∪ range LtK")
(auto dest: l3_dy_payload_refines_dy_fake_msg l3_dy_valid_refines_dy_fake_chan_Un
intro: l3_dy_isLtKey_refines_skip dest!: l3_dy_others_refines_skip)
subsubsection ‹Compromise events›
lemma l3_lkr_others_refines_lkr_others:
"{R23s} l2_lkr_others A, l3_lkr_others A {>R23s}"
apply (auto simp add: PO_rhoare_defs R23s_defs)
apply (auto simp add: l3_defs l2_lkr_others_def)
done
lemma l3_lkr_after_refines_lkr_after:
"{R23s} l2_lkr_after A, l3_lkr_after A {>R23s}"
apply (auto simp add: PO_rhoare_defs R23s_defs)
apply (auto simp add: l3_defs l2_lkr_after_def)
done
lemma l3_skr_refines_skr:
"{R23s} l2_skr R K, l3_skr R K {>R23s}"
apply (auto simp add: PO_rhoare_defs R23s_defs)
apply (auto simp add: l3_defs l2_skr_def)
done
lemmas l3_trans_refines_l2_trans =
l3_step1_refines_step1 l3_step2_refines_step2 l3_step3_refines_step3
l3_dy_refines_dy_fake_msg_dy_fake_chan_skip
l3_lkr_others_refines_lkr_others l3_lkr_after_refines_lkr_after l3_skr_refines_skr
lemma l3_refines_init_l2 [iff]:
"init l3 ⊆ R23s `` (init l2)"
by (auto simp add: R23s_defs l2_defs l3_def l3_init_def)
lemma l3_refines_trans_l2 [iff]:
"{R23s ∩ (UNIV × (l3_inv1 ∩ l3_inv2 ∩ l3_inv3 ∩ l3_inv4))} trans l2, trans l3 {> R23s}"
proof -
let ?pre' = "R23s ∩ (UNIV × (l3_inv5 ∩ l3_inv6 ∩ l3_inv7 ∩ l3_inv8 ∩ l3_inv9))"
show ?thesis (is "{?pre} ?t1, ?t2 {>?post}")
proof (rule relhoare_conseq_left)
show "?pre ⊆ ?pre'"
using l3_inv5_derived l3_inv6_derived l3_inv7_derived l3_inv8_derived l3_inv9_derived by blast
next
show "{?pre'} ?t1, ?t2 {> ?post}"
by (auto simp add: l2_def l3_def l2_trans_def l3_trans_def
intro!: l3_trans_refines_l2_trans)
qed
qed
lemma PO_obs_consistent_R23s [iff]:
"obs_consistent R23s med23s l2 l3"
by (auto simp add: obs_consistent_def R23s_def med23s_def l2_defs)
lemma l3_refines_l2 [iff]:
"refines
(R23s ∩
(reach l2 × (l3_inv1 ∩ l3_inv2 ∩ l3_inv3 ∩ l3_inv4)))
med23s l2 l3"
by (rule Refinement_using_invariants, auto)
lemma l3_implements_l2 [iff]:
"implements med23s l2 l3"
by (rule refinement_soundness) (auto)
subsection ‹Derived invariants›
subsubsection ‹inv10: secrets contain no implementation material›
definition
l3_inv10 :: "l3_state set"
where
"l3_inv10 ≡ {s.
secret s ⊆ payload
}"
lemmas l3_inv10I = l3_inv10_def [THEN setc_def_to_intro, rule_format]
lemmas l3_inv10E = l3_inv10_def [THEN setc_def_to_elim, rule_format]
lemmas l3_inv10D = l3_inv10_def [THEN setc_def_to_dest, rule_format]
lemma l3_inv10_init [iff]:
"init l3 ⊆ l3_inv10"
by (auto simp add: l3_def l3_init_def ik_init_def intro!:l3_inv10I)
lemma l3_inv10_trans [iff]:
"{l3_inv10} trans l3 {> l3_inv10}"
apply (auto simp add: PO_hoare_defs l3_nostep_defs)
apply (auto simp add: l3_defs l3_inv10_def)
done
lemma PO_l3_inv10 [iff]: "reach l3 ⊆ l3_inv10"
by (rule inv_rule_basic) (auto)
lemma l3_obs_inv10 [iff]: "oreach l3 ⊆ l3_inv10"
by (auto simp add: oreach_def)
subsubsection ‹Partial secrecy›
text ‹We want to prove @{term "l3_secrecy"}, ie
@{term "synth (analz (ik s)) ∩ secret s = {}"},
but by refinement we only get @{term "l3_partial_secrecy"}:
@{term "dy_fake_msg (bad s) (payloadSet (ik s)) (abs (ik s)) ∩ secret s = {}"}.
This is fine if secrets contain no implementation material.
Then, by @{term "inv5"}, a message in @{term "synth (analz (ik s))"} is in
@{term "dy_fake_msg (bad s) (payloadSet (ik s)) (abs (ik s)) ∪ -payload"},
and @{term "l3_partial_secrecy"} proves it is not a secret.
›
definition
l3_partial_secrecy :: "('a l3_state_scheme) set"
where
"l3_partial_secrecy ≡ {s.
dy_fake_msg (bad s) (ik s ∩ payload) (abs (ik s)) ∩ secret s = {}
}"
lemma l3_obs_partial_secrecy [iff]: "oreach l3 ⊆ l3_partial_secrecy"
apply (rule external_invariant_translation [OF l2_obs_secrecy _ l3_implements_l2])
apply (auto simp add: med23s_def l2_secrecy_def l3_partial_secrecy_def)
done
subsubsection ‹Secrecy›
definition
l3_secrecy :: "('a l3_state_scheme) set"
where
"l3_secrecy ≡ l1_secrecy"
lemma l3_obs_inv5: "oreach l3 ⊆ l3_inv5"
by (auto simp add: oreach_def)
lemma l3_obs_secrecy [iff]: "oreach l3 ⊆ l3_secrecy"
apply (rule, frule l3_obs_inv5 [THEN [2] rev_subsetD], frule l3_obs_inv10 [THEN [2] rev_subsetD])
apply (auto simp add: med23s_def l2_secrecy_def l3_secrecy_def s0_secrecy_def l3_inv10_def)
using l3_partial_secrecy_def apply (blast dest!: l3_inv5D subsetD [OF l3_obs_partial_secrecy])
done
lemma l3_secrecy [iff]: "reach l3 ⊆ l3_secrecy"
by (rule external_to_internal_invariant [OF l3_obs_secrecy], auto)
subsubsection ‹Injective agreement›
abbreviation "l3_iagreement ≡ l1_iagreement"
lemma l3_obs_iagreement [iff]: "oreach l3 ⊆ l3_iagreement"
apply (rule external_invariant_translation [OF l2_obs_iagreement _ l3_implements_l2])
apply (auto simp add: med23s_def l1_iagreement_def)
done
lemma l3_iagreement [iff]: "reach l3 ⊆ l3_iagreement"
by (rule external_to_internal_invariant [OF l3_obs_iagreement], auto)
end
end