Theory pfslvl2
section ‹Key Transport Protocol with PFS (L2)›
theory pfslvl2
imports pfslvl1 Channels
begin
declare domIff [simp, iff del]
subsection ‹State and Events›
text ‹initial compromise›
consts
bad_init :: "agent set"
specification (bad_init)
bad_init_spec: "test_owner ∉ bad_init ∧ test_partner ∉ bad_init"
by auto
text ‹level 2 state›
record l2_state =
l1_state +
chan :: "chan set"
bad :: "agent set"
type_synonym l2_obs = "l2_state"
type_synonym
l2_pred = "l2_state set"
type_synonym
l2_trans = "(l2_state × l2_state) set"
text ‹attacker events›
definition
l2_dy_fake_msg :: "msg ⇒ l2_trans"
where
"l2_dy_fake_msg m ≡ {(s,s').
m ∈ dy_fake_msg (bad s) (ik s) (chan s) ∧
s' = s⦇ik := {m} ∪ ik s⦈
}"
definition
l2_dy_fake_chan :: "chan ⇒ l2_trans"
where
"l2_dy_fake_chan M ≡ {(s,s').
M ∈ dy_fake_chan (bad s) (ik s) (chan s)∧
s' = s⦇chan := {M} ∪ chan s⦈
}"
text ‹partnering›
fun
role_comp :: "role_t ⇒ role_t"
where
"role_comp Init = Resp"
| "role_comp Resp = Init"
definition
matching :: "frame ⇒ frame ⇒ bool"
where
"matching sigma sigma' ≡ ∀ x. x ∈ dom sigma ∩ dom sigma' ⟶ sigma x = sigma' x"
definition
partner_runs :: "rid_t ⇒ rid_t ⇒ bool"
where
"partner_runs R R' ≡
role (guessed_runs R) = role_comp (role (guessed_runs R')) ∧
owner (guessed_runs R) = partner (guessed_runs R') ∧
owner (guessed_runs R') = partner (guessed_runs R) ∧
matching (guessed_frame R) (guessed_frame R')
"
lemma role_comp_inv [simp]:
"role_comp (role_comp x) = x"
by (cases x, auto)
lemma role_comp_inv_eq:
"y = role_comp x ⟷ x = role_comp y"
by (auto elim!: role_comp.elims [OF sym])
definition
partners :: "rid_t set"
where
"partners ≡ {R. partner_runs test R}"
lemma test_not_partner [simp]:
"test ∉ partners"
by (auto simp add: partners_def partner_runs_def, cases "role (guessed_runs test)", auto)
lemma matching_symmetric:
"matching sigma sigma' ⟹ matching sigma' sigma"
by (auto simp add: matching_def)
lemma partner_symmetric:
"partner_runs R R' ⟹ partner_runs R' R"
by (auto simp add: partner_runs_def matching_symmetric)
lemma partner_unique:
"partner_runs R R'' ⟹ partner_runs R R' ⟹ R' = R''"
proof -
assume H':"partner_runs R R'"
then have Hm': "matching (guessed_frame R) (guessed_frame R')"
by (auto simp add: partner_runs_def)
assume H'':"partner_runs R R''"
then have Hm'': "matching (guessed_frame R) (guessed_frame R'')"
by (auto simp add: partner_runs_def)
show ?thesis
proof (cases "role (guessed_runs R')")
case Init
with H' partner_symmetric [OF H''] have Hrole:"role (guessed_runs R) = Resp"
"role (guessed_runs R'') = Init"
by (auto simp add: partner_runs_def)
with Init Hm' have "guessed_frame R xpkE = Some (epubKF (R'$kE))"
by (simp add: matching_def)
moreover from Hrole Hm'' have "guessed_frame R xpkE = Some (epubKF (R''$kE))"
by (simp add: matching_def)
ultimately show ?thesis by simp
next
case Resp
with H' partner_symmetric [OF H''] have Hrole:"role (guessed_runs R) = Init"
"role (guessed_runs R'') = Resp"
by (auto simp add: partner_runs_def)
with Resp Hm' have "guessed_frame R xsk = Some (NonceF (R'$sk))"
by (simp add: matching_def)
moreover from Hrole Hm'' have "guessed_frame R xsk = Some (NonceF (R''$sk))"
by (simp add: matching_def)
ultimately show ?thesis by simp
qed
qed
lemma partner_test:
"R ∈ partners ⟹ partner_runs R R' ⟹ R' = test"
by (auto intro!:partner_unique simp add:partners_def partner_symmetric)
text ‹compromising events›
definition
l2_lkr_others :: "agent ⇒ l2_trans"
where
"l2_lkr_others A ≡ {(s,s').
A ≠ test_owner ∧
A ≠ test_partner ∧
s' = s⦇bad := {A} ∪ bad s⦈
}"
definition
l2_lkr_actor :: "agent ⇒ l2_trans"
where
"l2_lkr_actor A ≡ {(s,s').
A = test_owner ∧
A ≠ test_partner ∧
s' = s⦇bad := {A} ∪ bad s⦈
}"
definition
l2_lkr_after :: "agent ⇒ l2_trans"
where
"l2_lkr_after A ≡ {(s,s').
test_ended s ∧
s' = s⦇bad := {A} ∪ bad s⦈
}"
definition
l2_skr :: "rid_t ⇒ msg ⇒ l2_trans"
where
"l2_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 ‹protocol events›
definition
l2_step1 :: "rid_t ⇒ agent ⇒ agent ⇒ l2_trans"
where
"l2_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}),
chan := {Auth A B (⟨Number 0, epubKF (Ra$kE)⟩)} ∪ (chan s)
⦈
}"
definition
l2_step2 :: "rid_t ⇒ agent ⇒ agent ⇒ msg ⇒ l2_trans"
where
"l2_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 ∧
Auth A B ⟨Number 0, KE⟩ ∈ chan s ∧
s' = s⦇
progress := (progress s)(Rb ↦ {xpkE, xsk}),
chan := {Auth B A (Aenc (NonceF (Rb$sk)) KE)} ∪ (chan 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
l2_step3 :: "rid_t ⇒ agent ⇒ agent ⇒ msg ⇒ l2_trans"
where
"l2_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 ∧
Auth B A (Aenc K (epubKF (Ra$kE))) ∈ chan 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›
definition
l2_init :: "l2_state set"
where
"l2_init ≡ { ⦇
ik = {},
secret = {},
progress = Map.empty,
signals = λx. 0,
chan = {},
bad = bad_init
⦈}"
definition
l2_trans :: "l2_trans" where
"l2_trans ≡ (⋃m M KE Rb Ra A B K.
l2_step1 Ra A B ∪
l2_step2 Rb A B KE ∪
l2_step3 Ra A B m ∪
l2_dy_fake_chan M ∪
l2_dy_fake_msg m ∪
l2_lkr_others A ∪
l2_lkr_after A ∪
l2_skr Ra K ∪
Id
)"
definition
l2 :: "(l2_state, l2_obs) spec" where
"l2 ≡ ⦇
init = l2_init,
trans = l2_trans,
obs = id
⦈"
lemmas l2_loc_defs =
l2_step1_def l2_step2_def l2_step3_def
l2_def l2_init_def l2_trans_def
l2_dy_fake_chan_def l2_dy_fake_msg_def
l2_lkr_after_def l2_lkr_others_def l2_skr_def
lemmas l2_defs = l2_loc_defs ik_dy_def
lemmas l2_nostep_defs = l2_def l2_init_def l2_trans_def
lemma l2_obs_id [simp]: "obs l2 = id"
by (simp add: l2_def)
text ‹Once a run is finished, it stays finished, therefore if the test is not finished at some
point then it was not finished before either›
declare domIff [iff]
lemma l2_run_ended_trans:
"run_ended (progress s R) ⟹
(s, s') ∈ trans l2 ⟹
run_ended (progress s' R)"
apply (auto simp add: l2_nostep_defs)
apply (simp add: l2_defs, fast ?)+
done
declare domIff [iff del]
lemma l2_can_signal_trans:
"can_signal s' A B ⟹
(s, s') ∈ trans l2 ⟹
can_signal s A B"
by (auto simp add: can_signal_def l2_run_ended_trans)
subsection ‹Invariants›
subsubsection ‹inv1›
text ‹If @{term "can_signal s A B"} (i.e., @{term "A"}, @{term "B"} are the test session
agents and the test is not finished), then @{term "A"}, @{term "B"} are honest.›
definition
l2_inv1 :: "l2_state set"
where
"l2_inv1 ≡ {s. ∀A B.
can_signal s A B ⟶
A ∉ bad s ∧ B ∉ bad s
}"
lemmas l2_inv1I = l2_inv1_def [THEN setc_def_to_intro, rule_format]
lemmas l2_inv1E [elim] = l2_inv1_def [THEN setc_def_to_elim, rule_format]
lemmas l2_inv1D = l2_inv1_def [THEN setc_def_to_dest, rule_format, rotated 1, simplified]
lemma l2_inv1_init [iff]:
"init l2 ⊆ l2_inv1"
by (auto simp add: l2_def l2_init_def l2_inv1_def can_signal_def bad_init_spec)
lemma l2_inv1_trans [iff]:
"{l2_inv1} trans l2 {> l2_inv1}"
proof (auto simp add: PO_hoare_defs intro!: l2_inv1I del: conjI)
fix s' s :: l2_state
fix A B
assume HI:"s ∈ l2_inv1"
assume HT:"(s, s') ∈ trans l2"
assume "can_signal s' A B"
with HT have HS:"can_signal s A B"
by (auto simp add: l2_can_signal_trans)
with HI have "A ∉ bad s ∧ B ∉ bad s"
by fast
with HS HT show "A ∉ bad s' ∧ B ∉ bad s'"
by (auto simp add: l2_nostep_defs can_signal_def)
(simp_all add: l2_defs)
qed
lemma PO_l2_inv1 [iff]: "reach l2 ⊆ l2_inv1"
by (rule inv_rule_basic) (auto)
subsubsection ‹inv2 (authentication guard)›
text ‹
If @{term "Auth A B (⟨Number 0, KE⟩) ∈ chan s"} and @{term "A"}, @{term "B"} are honest
then the message has indeed been sent by an initiator run (with the right agents etc.)›
definition
l2_inv2 :: "l2_state set"
where
"l2_inv2 ≡ {s. ∀ A B KE.
Auth A B ⟨Number 0, KE⟩ ∈ chan s ⟶
A ∉ bad s ∧ B ∉ bad s ⟶
(∃ Ra.
guessed_runs Ra = ⦇role=Init, owner=A, partner=B⦈ ∧
in_progress (progress s Ra) xpkE ∧
KE = epubKF (Ra$kE))
}"
lemmas l2_inv2I = l2_inv2_def [THEN setc_def_to_intro, rule_format]
lemmas l2_inv2E [elim] = l2_inv2_def [THEN setc_def_to_elim, rule_format]
lemmas l2_inv2D = l2_inv2_def [THEN setc_def_to_dest, rule_format, rotated 1, simplified]
lemma l2_inv2_init [iff]:
"init l2 ⊆ l2_inv2"
by (auto simp add: l2_def l2_init_def l2_inv2_def)
lemma l2_inv2_trans [iff]:
"{l2_inv2} trans l2 {> l2_inv2}"
apply (auto simp add: PO_hoare_defs l2_nostep_defs intro!: l2_inv2I)
apply (auto simp add: l2_defs dy_fake_chan_def)
apply force+
done
lemma PO_l2_inv2 [iff]: "reach l2 ⊆ l2_inv2"
by (rule inv_rule_basic) (auto)
subsubsection ‹inv3 (authentication guard)›
text ‹If @{term "Auth B A (Aenc K (epubKF (Ra $ kE))) ∈ chan s"}
and @{term "A"}, @{term "B"} are honest then the message has indeed been sent by a
responder run (etc).›
definition
l2_inv3 :: "l2_state set"
where
"l2_inv3 ≡ {s. ∀ Ra A B K.
Auth B A (Aenc K (epubKF (Ra $ kE))) ∈ chan s ⟶
A ∉ bad s ∧ B ∉ bad s ⟶
(∃ Rb.
guessed_runs Rb = ⦇role=Resp, owner=B, partner=A⦈ ∧
progress s Rb = Some {xpkE, xsk} ∧
guessed_frame Rb xpkE = Some (epubKF (Ra$kE))∧
K = NonceF (Rb$sk)
)
}"
lemmas l2_inv3I = l2_inv3_def [THEN setc_def_to_intro, rule_format]
lemmas l2_inv3E [elim] = l2_inv3_def [THEN setc_def_to_elim, rule_format]
lemmas l2_inv3D = l2_inv3_def [THEN setc_def_to_dest, rule_format, rotated 1, simplified]
lemma l2_inv3_init [iff]:
"init l2 ⊆ l2_inv3"
by (auto simp add: l2_def l2_init_def l2_inv3_def)
lemma l2_inv3_trans [iff]:
"{l2_inv3} trans l2 {> l2_inv3}"
apply (auto simp add: PO_hoare_defs l2_nostep_defs intro!: l2_inv3I)
apply (auto simp add: l2_defs dy_fake_chan_def)
apply (simp_all add: domIff)
apply force+
done
lemma PO_l2_inv3 [iff]: "reach l2 ⊆ l2_inv3"
by (rule inv_rule_basic) (auto)
subsubsection ‹inv4›
text ‹If the test run is finished and has the session key generated by a run,
then this run is also finished.›
definition
l2_inv4 :: "l2_state set"
where
"l2_inv4 ≡ {s. ∀Rb.
in_progress (progress s test) xsk ⟶
guessed_frame test xsk = Some (NonceF (Rb$sk)) ⟶
progress s Rb = Some {xpkE, xsk}
}"
lemmas l2_inv4I = l2_inv4_def [THEN setc_def_to_intro, rule_format]
lemmas l2_inv4E [elim] = l2_inv4_def [THEN setc_def_to_elim, rule_format]
lemmas l2_inv4D = l2_inv4_def [THEN setc_def_to_dest, rule_format, rotated 1, simplified]
lemma l2_inv4_init [iff]:
"init l2 ⊆ l2_inv4"
by (auto simp add: l2_def l2_init_def l2_inv4_def)
lemma l2_inv4_trans [iff]:
"{l2_inv4 ∩ l2_inv3 ∩ l2_inv1} trans l2 {> l2_inv4}"
apply (auto simp add: PO_hoare_defs l2_nostep_defs intro!: l2_inv4I)
apply (auto simp add: l2_defs dy_fake_chan_def)
apply (auto dest!: l2_inv4D simp add: domIff can_signal_def)
apply (auto dest!: l2_inv3D intro!:l2_inv1D simp add: can_signal_def)
done
lemma PO_l2_inv4 [iff]: "reach l2 ⊆ l2_inv4"
by (rule_tac J="l2_inv3 ∩ l2_inv1" in inv_rule_incr) (auto)
subsubsection ‹inv5›
text ‹The only confidential or secure messages on the channel have been put there
by the attacker.›
definition
l2_inv5 :: "l2_state set"
where
"l2_inv5 ≡ {s. ∀A B M.
(Confid A B M ∈ chan s ∨ Secure A B M ∈ chan s) ⟶
M ∈ dy_fake_msg (bad s) (ik s) (chan s)
}"
lemmas l2_inv5I = l2_inv5_def [THEN setc_def_to_intro, rule_format]
lemmas l2_inv5E [elim] = l2_inv5_def [THEN setc_def_to_elim, rule_format]
lemmas l2_inv5D = l2_inv5_def [THEN setc_def_to_dest, rule_format, rotated 1, simplified]
lemma l2_inv5_init [iff]:
"init l2 ⊆ l2_inv5"
by (auto simp add: l2_def l2_init_def l2_inv5_def)
lemma l2_inv5_trans [iff]:
"{l2_inv5} trans l2 {> l2_inv5}"
apply (auto simp add: PO_hoare_defs l2_nostep_defs intro!: l2_inv5I)
apply (auto simp add: l2_defs dy_fake_chan_def intro: l2_inv5D dy_fake_msg_monotone)
done
lemma PO_l2_inv5 [iff]: "reach l2 ⊆ l2_inv5"
by (rule inv_rule_basic) (auto)
subsubsection ‹inv6›
text ‹If an initiator @{term "Ra"} knows a session key @{term "K"}, then the attacker
knows @{term "Aenc K (epubKF (Ra$kE))"}.›
definition
l2_inv6 :: "l2_state set"
where
"l2_inv6 ≡ {s. ∀Ra K.
role (guessed_runs Ra) = Init ⟶
in_progress (progress s Ra) xsk ⟶
guessed_frame Ra xsk = Some K ⟶
Aenc K (epubKF (Ra$kE)) ∈ extr (bad s) (ik s) (chan s)
}"
lemmas l2_inv6I = l2_inv6_def [THEN setc_def_to_intro, rule_format]
lemmas l2_inv6E [elim] = l2_inv6_def [THEN setc_def_to_elim, rule_format]
lemmas l2_inv6D = l2_inv6_def [THEN setc_def_to_dest, rule_format, rotated 1, simplified]
lemma l2_inv6_init [iff]:
"init l2 ⊆ l2_inv6"
by (auto simp add: l2_def l2_init_def l2_inv6_def)
lemma l2_inv6_trans [iff]:
"{l2_inv6} trans l2 {> l2_inv6}"
apply (auto simp add: PO_hoare_defs l2_nostep_defs intro!: l2_inv6I)
apply (auto simp add: l2_defs dy_fake_chan_def dest: l2_inv6D)
done
lemma PO_l2_inv6 [iff]: "reach l2 ⊆ l2_inv6"
by (rule inv_rule_basic) (auto)
subsubsection ‹inv7›
text ‹Form of the messages in @{term "extr (bad s) (ik s) (chan s)"} =
@{term "synth (analz (generators))"}.›
abbreviation
"generators ≡ range epubK ∪
{Aenc (NonceF (Rb $ sk)) (epubKF (Ra$kE)) |Ra Rb. ∃ A B.
guessed_runs Ra = ⦇role=Init, owner=A, partner=B⦈ ∧
guessed_runs Rb = ⦇role=Resp, owner=B, partner=A⦈ ∧
guessed_frame Rb xpkE = Some (epubKF (Ra$kE))} ∪
{NonceF (R $ sk) |R. R ≠ test ∧ R ∉ partners}"
lemma analz_generators: "analz generators = generators"
by (rule, rule, erule analz.induct, auto)
definition
l2_inv7 :: "l2_state set"
where
"l2_inv7 ≡ {s.
extr (bad s) (ik s) (chan s) ⊆
synth (analz (generators))
}"
lemmas l2_inv7I = l2_inv7_def [THEN setc_def_to_intro, rule_format]
lemmas l2_inv7E [elim] = l2_inv7_def [THEN setc_def_to_elim, rule_format]
lemmas l2_inv7D = l2_inv7_def [THEN setc_def_to_dest, rule_format, rotated 1, simplified]
lemma l2_inv7_init [iff]:
"init l2 ⊆ l2_inv7"
by (auto simp add: l2_def l2_init_def l2_inv7_def)
lemma l2_inv7_step1:
"{l2_inv7} l2_step1 Ra A B {> l2_inv7}"
apply (auto simp add: PO_hoare_defs l2_defs intro!: l2_inv7I)
apply (auto dest: l2_inv7D [THEN [2] rev_subsetD])+
done
lemma l2_inv7_step2:
"{l2_inv1 ∩ l2_inv2 ∩ l2_inv4 ∩ l2_inv7} l2_step2 Rb A B KE {> l2_inv7}"
proof (auto simp add: PO_hoare_defs l2_nostep_defs intro!: l2_inv7I)
fix s' s :: l2_state
fix x
assume Hx:"x ∈ extr (bad s') (ik s') (chan s')"
assume Hi:"s ∈ l2_inv7"
assume Hi':"s ∈ l2_inv1"
assume Hi'':"s ∈ l2_inv2"
assume Hi''':"s ∈ l2_inv4"
assume Hs:"(s, s') ∈ l2_step2 Rb A B KE"
from Hx Hi Hs show " x ∈ synth (analz (generators))"
proof (auto simp add: l2_defs dest: l2_inv7D [THEN [2] rev_subsetD])
txt ‹first case: @{term "can_signal s A B"}, which implies that @{term "A"}, @{term "B"} are
honest, and therefore the public key received by @{term "B"} is not from the attacker,
which proves that the
message added to the channel is in @{term "{z. ∃x k. z = Aenc x (epubKF k)}"}›
assume Hc:"Auth A B ⟨Number 0, KE⟩ ∈ chan s"
assume HRb:"guessed_runs Rb = ⦇role = Resp, owner = B, partner = A⦈"
"guessed_frame Rb xpkE = Some KE"
assume Hcs: "can_signal s A B"
from Hcs Hi' have "A ∉ bad s ∧ B ∉ bad s"
by auto
with Hc Hi'' obtain Ra where "KE = epubKF (Ra$kE)"
and "guessed_runs Ra = ⦇role=Init, owner=A, partner=B⦈"
by (auto dest: l2_inv2D)
with HRb show "Aenc (NonceF (Rb $ sk)) KE ∈ synth (analz generators)"
by blast
next
txt ‹second case: @{term "¬ can_signal s A B"}. We show that @{term "Rb"} is not test and
not a partner:
- @{term "Rb"} is not test because in that case test is not finished and
@{term "A"}, @{term "B"} are the test agents, thus
@{term "can_signal s A B"}
- @{term "Rb"} is not a partner for the same reason
therefore the message added to the channel can be constructed from
@{term "{NonceF (R $ sk) |R. R ≠ test ∧ R ∉ partners}"}›
assume Hc:"Auth A B ⟨Number 0, KE⟩ ∈ chan s"
assume Hcs:"¬ can_signal s A B"
assume HRb:"Rb ∉ dom (progress s)"
"guessed_runs Rb = ⦇role = Resp, owner = B, partner = A⦈"
from Hcs HRb have "Rb ≠ test"
by (auto simp add: can_signal_def domIff)
moreover from HRb Hi''' Hcs have "Rb ∉ partners"
by (clarify, auto simp add: partners_def partner_runs_def can_signal_def matching_def domIff)
moreover from Hc Hi have "KE ∈ synth (analz (generators))"
by auto
ultimately show "Aenc (NonceF (Rb $ sk)) KE ∈ synth (analz (generators))"
by blast
qed
qed
lemma l2_inv7_step3:
"{l2_inv7} l2_step3 Rb A B K {> l2_inv7}"
by (auto simp add: PO_hoare_defs l2_defs intro!: l2_inv7I dest: l2_inv7D [THEN [2] rev_subsetD])
lemma l2_inv7_dy_fake_msg:
"{l2_inv7} l2_dy_fake_msg M {> l2_inv7}"
by (auto simp add: PO_hoare_defs l2_defs extr_insert_IK_eq
intro!: l2_inv7I
elim!: l2_inv7E dy_fake_msg_extr [THEN [2] rev_subsetD])
lemma l2_inv7_dy_fake_chan:
"{l2_inv7} l2_dy_fake_chan M {> l2_inv7}"
by (auto simp add: PO_hoare_defs l2_defs
intro!: l2_inv7I
dest: dy_fake_chan_extr_insert [THEN [2] rev_subsetD]
elim!: l2_inv7E dy_fake_msg_extr [THEN [2] rev_subsetD])
lemma l2_inv7_lkr_others:
"{l2_inv7 ∩ l2_inv5} l2_lkr_others A {> l2_inv7}"
apply (auto simp add: PO_hoare_defs l2_defs
intro!: l2_inv7I
dest!: extr_insert_bad [THEN [2] rev_subsetD]
elim!: l2_inv7E l2_inv5E)
apply (auto dest: dy_fake_msg_extr [THEN [2] rev_subsetD])
done
lemma l2_inv7_lkr_after:
"{l2_inv7 ∩ l2_inv5} l2_lkr_after A {> l2_inv7}"
apply (auto simp add: PO_hoare_defs l2_defs
intro!: l2_inv7I
dest!: extr_insert_bad [THEN [2] rev_subsetD]
elim!: l2_inv7E l2_inv5E)
apply (auto dest: dy_fake_msg_extr [THEN [2] rev_subsetD])
done
lemma l2_inv7_skr:
"{l2_inv7 ∩ l2_inv6} l2_skr R K {> l2_inv7}"
proof (auto simp add: PO_hoare_defs l2_defs extr_insert_IK_eq intro!: l2_inv7I,
auto elim: l2_inv7D [THEN subsetD])
fix s
assume HRtest: "R ≠ test" "R ∉ partners"
assume Hi: "s ∈ l2_inv7"
assume Hi': "s ∈ l2_inv6"
assume HRsk: "in_progress (progress s R) xsk" "guessed_frame R xsk = Some K"
show "K ∈ synth (analz generators)"
proof (cases "role (guessed_runs R)")
txt ‹first case: @{term "R"} is the initiator, then @{term "Aenc K epk"}
is in @{term "extr (bad s) (ik s) (chan s)"} (by invariant)
therefore either @{term "K ∈ synth (analz generators)"} which proves the goal
or @{term "Aenc K epk ∈ generators"}, which means that
@{term "K = NonceF (Rb$sk)"} where @{term "R"} and @{term "Rb"} are matching
and since @{term "R"} is not partner or test, neither is
@{term "Rb"}, and therefore @{term "K ∈ synth (analz (generators))"}›
assume HRI: "role (guessed_runs R) = Init"
with HRsk Hi Hi' have "Aenc K (epubKF (R$kE)) ∈ synth (analz generators)"
by (auto dest!: l2_inv7D)
then have "K ∈ synth (analz generators) ∨ Aenc K (epubKF (R$kE)) ∈ generators"
by (rule synth.cases, simp_all, simp add: analz_generators)
with HRsk show ?thesis
proof auto
fix Rb A B
assume HR: "guessed_runs R = ⦇role = Init, owner = A, partner = B⦈"
"guessed_frame R xsk = Some (NonceF (Rb $ sk))"
assume HRb: "guessed_runs Rb = ⦇role = Resp, owner = B, partner = A⦈"
"guessed_frame Rb xpkE = Some (epubKF (R $ kE))"
from HR HRb have "partner_runs Rb R"
by (auto simp add: partner_runs_def matching_def)
with HRtest have "Rb ≠ test ∧ Rb ∉ partners"
by (auto dest: partner_test, simp add:partners_def)
then show "NonceF (Rb $ sk) ∈ analz generators"
by blast
qed
next
txt ‹second case: @{term "R"} is the Responder, then @{term "K"} is @{term "R$sk"}
which is in @{term "synth (analz (generators))"}
since @{term "R"} is not test or partner›
assume HRI: "role (guessed_runs R) = Resp"
with HRsk HRtest show ?thesis
by auto
qed
qed
lemmas l2_inv7_trans_aux =
l2_inv7_step1 l2_inv7_step2 l2_inv7_step3
l2_inv7_dy_fake_msg l2_inv7_dy_fake_chan
l2_inv7_lkr_others l2_inv7_lkr_after l2_inv7_skr
lemma l2_inv7_trans [iff]:
"{l2_inv7 ∩ l2_inv1 ∩ l2_inv2 ∩ l2_inv4 ∩ l2_inv5 ∩ l2_inv6} trans l2 {> l2_inv7}"
by (auto simp add: l2_nostep_defs intro:l2_inv7_trans_aux)
lemma PO_l2_inv7 [iff]: "reach l2 ⊆ l2_inv7"
by (rule_tac J="l2_inv1 ∩ l2_inv2 ∩ l2_inv4 ∩ l2_inv5 ∩ l2_inv6" in inv_rule_incr) (auto)
lemma l2_inv7_aux:
"NonceF (R$sk) ∈ analz (ik s) ⟹ s ∈ l2_inv7 ⟹ R ≠ test ∧ R ∉ partners"
proof -
assume H:"s ∈ l2_inv7" and H':"NonceF (R$sk) ∈ analz (ik s)"
then have H'':"NonceF (R$sk) ∈ analz (extr (bad s) (ik s) (chan s))"
by (auto elim: analz_monotone)
from H have "analz (extr (bad s) (ik s) (chan s)) ⊆ analz (synth (analz generators))"
by (blast dest: analz_mono intro: l2_inv7D)
with H'' have "NonceF (R$sk) ∈ analz generators"
by auto
then have "NonceF (R$sk) ∈ generators"
by (simp add: analz_generators)
then show ?thesis
by auto
qed
subsubsection ‹inv8›
text ‹Form of the secrets = nonces generated by test or partners›
definition
l2_inv8 :: "l2_state set"
where
"l2_inv8 ≡ {s.
secret s ⊆ {NonceF (R$sk) | R. R = test ∨ R ∈ partners}
}"
lemmas l2_inv8I = l2_inv8_def [THEN setc_def_to_intro, rule_format]
lemmas l2_inv8E [elim] = l2_inv8_def [THEN setc_def_to_elim, rule_format]
lemmas l2_inv8D = l2_inv8_def [THEN setc_def_to_dest, rule_format, rotated 1, simplified]
lemma l2_inv8_init [iff]:
"init l2 ⊆ l2_inv8"
by (auto simp add: l2_def l2_init_def l2_inv8_def)
lemma l2_inv8_trans [iff]:
"{l2_inv8 ∩ l2_inv1 ∩ l2_inv3} trans l2 {> l2_inv8}"
supply [[simproc del: defined_all]]
apply (auto simp add: PO_hoare_defs l2_nostep_defs intro!: l2_inv8I)
apply (auto simp add: l2_defs dy_fake_chan_def)
apply (auto simp add: partners_def partner_runs_def matching_def dest!: l2_inv3D)
apply (simp_all add: can_signal_def)
done
lemma PO_l2_inv8 [iff]: "reach l2 ⊆ l2_inv8"
by (rule_tac J="l2_inv1 ∩ l2_inv3" in inv_rule_incr) (auto)
subsection ‹Refinement›
text ‹mediator function›
definition
med12s :: "l2_obs ⇒ l1_obs"
where
"med12s t ≡ ⦇
ik = ik t,
secret = secret t,
progress = progress t,
signals = signals t
⦈"
text ‹relation between states›
definition
R12s :: "(l1_state * l2_state) set"
where
"R12s ≡ {(s,s').
s = med12s s'
}"
lemmas R12s_defs = R12s_def med12s_def
lemma can_signal_R12 [simp]:
"(s1, s2) ∈ R12s ⟹
can_signal s1 A B ⟷ can_signal s2 A B"
by (auto simp add: can_signal_def R12s_defs)
text ‹protocol events›
lemma l2_step1_refines_step1:
"{R12s} l1_step1 Ra A B, l2_step1 Ra A B {>R12s}"
by (auto simp add: PO_rhoare_defs R12s_defs l1_step1_def l2_step1_def)
lemma l2_step2_refines_step2:
"{R12s ∩ UNIV × (l2_inv1 ∩ l2_inv2 ∩ l2_inv7)}
l1_step2 Rb A B KE, l2_step2 Rb A B KE
{>R12s}"
apply (auto simp add: PO_rhoare_defs R12s_defs l1_step2_def, simp_all add: l2_step2_def)
apply (auto dest!: l2_inv7_aux l2_inv2D)
done
text ‹auxiliary lemma needed to prove that the nonce received by the test in step 3
comes from a partner›
lemma l2_step3_partners:
"guessed_runs test = ⦇role = Init, owner = A, partner = B⦈ ⟹
guessed_frame test xsk = Some (NonceF (Rb$sk)) ⟹
guessed_runs Rb = ⦇role = Resp, owner = B, partner = A⦈ ⟹
guessed_frame Rb xpkE = Some (epubKF (test $ kE)) ⟹
Rb ∈ partners"
by (auto simp add: partners_def partner_runs_def matching_def)
lemma l2_step3_refines_step3:
"{R12s ∩ UNIV × (l2_inv1 ∩ l2_inv3 ∩ l2_inv7)}
l1_step3 Ra A B K, l2_step3 Ra A B K
{>R12s}"
supply [[simproc del: defined_all]]
apply (auto simp add: PO_rhoare_defs R12s_defs l1_step3_def, simp_all add: l2_step3_def)
apply (auto dest!: l2_inv3D l2_inv7_aux intro:l2_step3_partners)
apply (auto simp add: can_signal_def)
done
text ‹attacker events›
lemma l2_dy_fake_chan_refines_skip:
"{R12s} Id, l2_dy_fake_chan M {>R12s}"
by (auto simp add: PO_rhoare_defs R12s_defs l2_defs)
lemma l2_dy_fake_msg_refines_learn:
"{R12s ∩ UNIV × l2_inv7 ∩ UNIV × l2_inv8} l1_learn m, l2_dy_fake_msg m {>R12s}"
apply (auto simp add: PO_rhoare_defs R12s_defs l2_loc_defs l1_defs)
apply (drule Fake_insert_dy_fake_msg, erule l2_inv7D)
apply (auto simp add: analz_generators dest!: l2_inv8D)
apply (drule subsetD, simp, drule subsetD, simp, auto)
done
text ‹compromising events›
lemma l2_lkr_others_refines_skip:
"{R12s} Id, l2_lkr_others A {>R12s}"
by (auto simp add: PO_rhoare_defs R12s_defs l2_loc_defs l1_defs)
lemma l2_lkr_after_refines_skip:
"{R12s} Id, l2_lkr_after A {>R12s}"
by (auto simp add: PO_rhoare_defs R12s_defs l2_loc_defs l1_defs)
lemma l2_skr_refines_learn:
"{R12s ∩ UNIV × l2_inv7 ∩ UNIV × l2_inv6 ∩ UNIV × l2_inv8} l1_learn K, l2_skr R K {>R12s}"
proof (auto simp add: PO_rhoare_defs R12s_defs l2_loc_defs l1_defs)
fix s :: l2_state fix x
assume H:"s ∈ l2_inv7" "s ∈ l2_inv6"
"R ∉ partners" "R ≠ test" "run_ended (progress s R)" "guessed_frame R xsk = Some K"
assume Hx:"x ∈ synth (analz (insert K (ik s)))"
assume "x ∈ secret s" "s ∈ l2_inv8"
then obtain R where "x = NonceF (R$sk)" and "R = test ∨ R ∈ partners"
by auto
moreover from H have "s ⦇ik := insert K (ik s)⦈ ∈ l2_inv7"
by (auto intro: hoare_apply [OF l2_inv7_skr] simp add: l2_defs)
ultimately show False using Hx
by (auto dest: l2_inv7_aux [rotated 1])
qed
text ‹refinement proof›
lemmas l2_trans_refines_l1_trans =
l2_dy_fake_msg_refines_learn l2_dy_fake_chan_refines_skip
l2_lkr_others_refines_skip l2_lkr_after_refines_skip l2_skr_refines_learn
l2_step1_refines_step1 l2_step2_refines_step2 l2_step3_refines_step3
lemma l2_refines_init_l1 [iff]:
"init l2 ⊆ R12s `` (init l1)"
by (auto simp add: R12s_defs l1_defs l2_loc_defs)
lemma l2_refines_trans_l1 [iff]:
"{R12s ∩ (UNIV × (l2_inv1 ∩ l2_inv2 ∩ l2_inv3 ∩ l2_inv6 ∩ l2_inv7 ∩ l2_inv8))} trans l1, trans l2 {> R12s}"
by (auto 0 3 simp add: l1_def l2_def l1_trans_def l2_trans_def
intro!: l2_trans_refines_l1_trans)
lemma PO_obs_consistent_R12s [iff]:
"obs_consistent R12s med12s l1 l2"
by (auto simp add: obs_consistent_def R12s_def med12s_def l2_defs)
lemma l2_refines_l1 [iff]:
"refines
(R12s ∩
(reach l1 × (l2_inv1 ∩ l2_inv2 ∩ l2_inv3 ∩ l2_inv4 ∩ l2_inv5 ∩ l2_inv6 ∩ l2_inv7 ∩ l2_inv8)))
med12s l1 l2"
by (rule Refinement_using_invariants, auto)
lemma l2_implements_l1 [iff]:
"implements med12s l1 l2"
by (rule refinement_soundness) (auto)
subsection ‹Derived invariants›
text ‹
We want to prove @{term "l2_secrecy"}:
@{term "dy_fake_msg (bad s) (ik s) (chan s) ∩ secret s = {}"}
but by refinement we only get @{term "l2_partial_secrecy"}:
@{term "synth (analz (ik s)) ∩ secret s = {}"}
This is fine, since a message in
@{term "dy_fake_msg (bad s) (ik s) (chan s)"} could be added to @{term "ik s"},
and @{term "l2_partial_secrecy"} would still hold for this new state.
›
definition
l2_partial_secrecy :: "('a l2_state_scheme) set"
where
"l2_partial_secrecy ≡ {s. synth (analz (ik s)) ∩ secret s = {}}"
lemma l2_obs_partial_secrecy [iff]: "oreach l2 ⊆ l2_partial_secrecy"
apply (rule external_invariant_translation
[OF l1_obs_secrecy _ l2_implements_l1])
apply (auto simp add: med12s_def s0_secrecy_def l2_partial_secrecy_def)
done
lemma l2_oreach_dy_fake_msg:
"s ∈ oreach l2 ⟹ x ∈ dy_fake_msg (bad s) (ik s) (chan s) ⟹ s ⦇ik := insert x (ik s)⦈ ∈ oreach l2"
apply (auto simp add: oreach_def, rule, simp_all, simp add: l2_def l2_trans_def l2_dy_fake_msg_def)
apply blast
done
definition
l2_secrecy :: "('a l2_state_scheme) set"
where
"l2_secrecy ≡ {s. dy_fake_msg (bad s) (ik s) (chan s) ∩ secret s = {}}"
lemma l2_obs_secrecy [iff]: "oreach l2 ⊆ l2_secrecy"
apply (auto simp add:l2_secrecy_def)
apply (drule l2_oreach_dy_fake_msg, simp_all)
apply (drule l2_obs_partial_secrecy [THEN [2] rev_subsetD], simp add: l2_partial_secrecy_def)
apply blast
done
lemma l2_secrecy [iff]: "reach l2 ⊆ l2_secrecy"
by (rule external_to_internal_invariant [OF l2_obs_secrecy], auto)
abbreviation "l2_iagreement ≡ l1_iagreement"
lemma l2_obs_iagreement [iff]: "oreach l2 ⊆ l2_iagreement"
apply (rule external_invariant_translation
[OF l1_obs_iagreement _ l2_implements_l1])
apply (auto simp add: med12s_def l1_iagreement_def)
done
lemma l2_iagreement [iff]: "reach l2 ⊆ l2_iagreement"
by (rule external_to_internal_invariant [OF l2_obs_iagreement], auto)
end