Theory sklvl2
section ‹SKEME Protocol (L2)›
theory sklvl2
imports sklvl1 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 =
skl1_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)
text ‹The unicity of the parther is actually protocol dependent:
it only holds if there are generated fresh nonces (which identify the runs) in the frames›
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 xgnx = Some (Exp Gen (NonceF (R'$nx)))"
by (simp add: matching_def)
moreover from Hrole Hm'' have "guessed_frame R xgnx = Some (Exp Gen (NonceF (R''$nx)))"
by (simp add: matching_def)
ultimately show ?thesis by (auto dest: Exp_Gen_inj)
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 xgny = Some (Exp Gen (NonceF (R'$ny)))"
by (simp add: matching_def)
moreover from Hrole Hm'' have "guessed_frame R xgny = Some (Exp Gen (NonceF (R''$ny)))"
by (simp add: matching_def)
ultimately show ?thesis by (auto dest: Exp_Gen_inj)
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 (with $K=H(ni, nr)$):
\begin{itemize}
\item step 1: create @{term "Ra"}, @{term "A"} generates @{term "nx"} and @{term "ni"},
confidentially sends @{term "ni"},
computes and insecurely sends $@{term "g"}^@{term "nx"}$
\item step 2: create @{term "Rb"}, @{term "B"} receives @{term "ni"} (confidentially)
and $@{term "g"}^@{term "nx"}$ (insecurely),
generates @{term "ny"} and @{term "nr"},
confidentially sends @{term "nr"}, insecurely sends $@{term "g"}^@{term "ny"}$ and
$MAC_K(@{term "g"}^@{term "nx"}, @{term "g"}^@{term "ny"}, @{term "B"}, @{term "A"})$
computes $@{term "g"}^@{term "nx*ny"}$,
emits a running signal for @{term "Init"}, @{term "ni"}, @{term "nr"}, $@{term "g"}^@{term "nx*ny"}$
\item step 3: @{term "A"} receives @{term "nr"} confidentially,
and $@{term "g"}^@{term "ny"}$ and the MAC insecurely,
sends $MAC_K(@{term "g"}^@{term "ny"}, @{term "g"}^@{term "nx"}, @{term "A"}, @{term "B"})$
insecurely, computes $@{term "g"}^@{term "ny*nx"}$, emits a commit signal for @{term "Init"},
@{term "ni"}, @{term "nr"}, $@{term "g"}^@{term "ny*nx"}$,
a running signal for @{term "Resp"}, @{term "ni"}, @{term "nr"}, $@{term "g"}^@{term "ny*nx"}$,
declares the secret $@{term "g"}^@{term "ny*nx"}$
\item step 4: @{term "B"} receives the MAC insecurely,
emits a commit signal for @{term "Resp"}, @{term "ni"}, @{term "nr"},
$@{term "g"}^@{term "nx*ny"}$,
declares the secret $@{term "g"}^@{term "nx*ny"}$
\end{itemize}
›
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 ↦ {xnx, xni, xgnx}),
chan := {Confid A B (NonceF (Ra$ni))} ∪
({Insec A B (Exp Gen (NonceF (Ra$nx)))} ∪
(chan s))
⦈
}"
definition
l2_step2 :: "rid_t ⇒ agent ⇒ agent ⇒ msg ⇒ msg ⇒ l2_trans"
where
"l2_step2 Rb A B Ni gnx ≡ {(s, s').
guessed_runs Rb = ⦇role=Resp, owner=B, partner=A⦈ ∧
Rb ∉ dom (progress s) ∧
guessed_frame Rb xgnx = Some gnx ∧
guessed_frame Rb xni = Some Ni ∧
guessed_frame Rb xsk = Some (Exp gnx (NonceF (Rb$ny))) ∧
Confid A B Ni ∈ chan s ∧
Insec A B gnx ∈ chan s ∧
s' = s⦇ progress := (progress s)(Rb ↦ {xny, xni, xnr, xgny, xgnx, xsk}),
chan := {Confid B A (NonceF (Rb$nr))} ∪
({Insec B A
⟨Exp Gen (NonceF (Rb$ny)),
hmac ⟨Number 0, gnx, Exp Gen (NonceF (Rb$ny)), Agent B, Agent A⟩
(Hash ⟨Ni, NonceF (Rb$nr)⟩)⟩ } ∪
(chan s)),
signalsInit :=
if can_signal s A B then
addSignal (signalsInit s)
(Running A B ⟨Ni, NonceF (Rb$nr), Exp gnx (NonceF (Rb$ny))⟩)
else
signalsInit s,
signalsInit2 :=
if can_signal s A B then
addSignal (signalsInit2 s) (Running A B (Exp gnx (NonceF (Rb$ny))))
else
signalsInit2 s
⦈
}"
definition
l2_step3 :: "rid_t ⇒ agent ⇒ agent ⇒ msg ⇒ msg ⇒ l2_trans"
where
"l2_step3 Ra A B Nr gny ≡ {(s, s').
guessed_runs Ra = ⦇role=Init, owner=A, partner=B⦈ ∧
progress s Ra = Some {xnx, xni, xgnx} ∧
guessed_frame Ra xgny = Some gny ∧
guessed_frame Ra xnr = Some Nr ∧
guessed_frame Ra xsk = Some (Exp gny (NonceF (Ra$nx))) ∧
Confid B A Nr ∈ chan s ∧
Insec B A ⟨gny, hmac ⟨Number 0, Exp Gen (NonceF (Ra$nx)), gny, Agent B, Agent A⟩
(Hash ⟨NonceF (Ra$ni), Nr⟩)⟩ ∈ chan s ∧
s' = s⦇ progress := (progress s)(Ra ↦ {xnx, xni, xnr, xgnx, xgny, xsk, xEnd}),
chan := {Insec A B
(hmac ⟨Number 1, gny, Exp Gen (NonceF (Ra$nx)), Agent A, Agent B⟩
(Hash ⟨NonceF (Ra$ni), Nr⟩))}
∪ chan s,
secret := {x. x = Exp gny (NonceF (Ra$nx)) ∧ Ra = test} ∪ secret s,
signalsInit :=
if can_signal s A B then
addSignal (signalsInit s)
(Commit A B ⟨NonceF (Ra$ni), Nr, Exp gny (NonceF (Ra$nx))⟩)
else
signalsInit s,
signalsInit2 :=
if can_signal s A B then
addSignal (signalsInit2 s) (Commit A B (Exp gny (NonceF (Ra$nx))))
else
signalsInit2 s,
signalsResp :=
if can_signal s A B then
addSignal (signalsResp s)
(Running A B ⟨NonceF (Ra$ni), Nr, Exp gny (NonceF (Ra$nx))⟩)
else
signalsResp s,
signalsResp2 :=
if can_signal s A B then
addSignal (signalsResp2 s) (Running A B (Exp gny (NonceF (Ra$nx))))
else
signalsResp2 s
⦈
}"
definition
l2_step4 :: "rid_t ⇒ agent ⇒ agent ⇒ msg ⇒ msg ⇒ l2_trans"
where
"l2_step4 Rb A B Ni gnx ≡ {(s, s').
guessed_runs Rb = ⦇role=Resp, owner=B, partner=A⦈ ∧
progress s Rb = Some {xny, xni, xnr, xgnx, xgny, xsk} ∧
guessed_frame Rb xgnx = Some gnx ∧
guessed_frame Rb xni = Some Ni ∧
Insec A B (hmac ⟨Number 1, Exp Gen (NonceF (Rb$ny)), gnx, Agent A, Agent B⟩
(Hash ⟨Ni, NonceF (Rb$nr)⟩)) ∈ chan s ∧
s' = s⦇ progress := (progress s)(Rb ↦ {xny, xni, xnr, xgnx, xgny, xsk, xEnd}),
secret := {x. x = Exp gnx (NonceF (Rb$ny)) ∧ Rb = test} ∪ secret s,
signalsResp :=
if can_signal s A B then
addSignal (signalsResp s)
(Commit A B ⟨Ni, NonceF (Rb$nr), Exp gnx (NonceF (Rb$ny))⟩)
else
signalsResp s,
signalsResp2 :=
if can_signal s A B then
addSignal (signalsResp2 s) (Commit A B (Exp gnx (NonceF (Rb$ny))))
else
signalsResp2 s
⦈
}"
text ‹specification›
definition
l2_init :: "l2_state set"
where
"l2_init ≡ { ⦇
ik = {},
secret = {},
progress = Map.empty,
signalsInit = λx. 0,
signalsResp = λx. 0,
signalsInit2 = λx. 0,
signalsResp2 = λx. 0,
chan = {},
bad = bad_init
⦈}"
definition
l2_trans :: "l2_trans" where
"l2_trans ≡ (⋃m M X Rb Ra A B K Y.
l2_step1 Ra A B ∪
l2_step2 Rb A B X Y ∪
l2_step3 Ra A B X Y ∪
l2_step4 Rb A B X Y ∪
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_step4_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
lemmas l2_step_defs =
l2_step1_def l2_step2_def l2_step3_def l2_step4_def
l2_dy_fake_chan_def l2_dy_fake_msg_def l2_lkr_after_def l2_lkr_others_def l2_skr_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 (auto simp add: l2_defs)
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)
lemma in_progressS_trans:
"in_progressS (progress s R) S ⟹ (s, s') ∈ trans l2 ⟹ in_progressS (progress s' R) S"
apply (auto simp add: l2_nostep_defs)
apply (auto simp add: l2_defs domIff)
done
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›
text ‹For a run @{term "R"} (with any role), the session key is always
$something^n$ where $n$ is a nonce generated by @{term "R"}.›
definition
l2_inv2 :: "l2_state set"
where
"l2_inv2 ≡ {s. ∀R.
in_progress (progress s R) xsk ⟶
(∃ X N.
guessed_frame R xsk = Some (Exp X (NonceF (R$N))))
}"
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 dest: l2_inv2D)
done
lemma PO_l2_inv2 [iff]: "reach l2 ⊆ l2_inv2"
by (rule inv_rule_basic) (auto)
subsubsection ‹inv3›
definition
"bad_runs s = {R. owner (guessed_runs R) ∈ bad s ∨ partner (guessed_runs R) ∈ bad s}"
abbreviation
generators :: "l2_state ⇒ msg set"
where
"generators s ≡
{x. ∃ N. x = Exp Gen (Nonce N)} ∪
{x. ∃ R ∈ bad_runs s. x = NonceF (R$ni) ∨ x = NonceF (R$nr)} ∪
{x. ∃ y y' z. x = hmac ⟨y, y'⟩ (Hash z)} ∪
{Exp y (NonceF (R$N)) | y N R. R ≠ test ∧ R ∉ partners}"
lemma analz_generators: "analz (generators s) = generators s"
by (rule, rule, erule analz.induct) (auto)
definition
faked_chan_msgs :: "l2_state ⇒ chan set"
where
"faked_chan_msgs s =
{Chan x A B M | x A B M. M ∈ synth (analz (extr (bad s) (ik s) (chan s)))}"
definition
chan_generators :: "chan set"
where
"chan_generators = {x. ∃ n R.
x = Confid (owner (guessed_runs R)) (partner (guessed_runs R)) (NonceF (R$n)) ∧
(n = ni ∨ n = nr)
}"
definition
l2_inv3 :: "l2_state set"
where
"l2_inv3 ≡ {s.
extr (bad s) (ik s) (chan s) ⊆ synth (analz (generators s)) ∧
chan s ⊆ faked_chan_msgs s ∪ chan_generators
}"
lemmas l2_inv3_aux_defs = faked_chan_msgs_def chan_generators_def
lemmas l2_inv3I = l2_inv3_def [THEN setc_def_to_intro, rule_format]
lemmas l2_inv3E = 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_step1:
"{l2_inv3} l2_step1 Ra A B {> l2_inv3}"
apply (auto simp add: PO_hoare_defs l2_nostep_defs intro!: l2_inv3I)
apply (auto simp add: l2_defs bad_runs_def intro: synth_analz_increasing dest!: l2_inv3D)
apply (auto simp add: l2_inv3_aux_defs intro: synth_analz_monotone
dest!: subsetD [where A="chan _"])
done
lemma l2_inv3_step2:
"{l2_inv3} l2_step2 Rb A B Ni gnx {> l2_inv3}"
apply (auto simp add: PO_hoare_defs l2_nostep_defs intro!: l2_inv3I)
apply (auto simp add: l2_defs)
apply (auto simp add: bad_runs_def intro: synth_analz_increasing dest!: l2_inv3D)
apply (auto simp add: l2_inv3_aux_defs)
apply (blast intro: synth_analz_monotone analz.intros insert_iff synth_analz_increasing
dest!: subsetD [where A="chan _"])+
done
lemma l2_inv3_step3:
"{l2_inv3} l2_step3 Ra A B Nr gny {> l2_inv3}"
apply (auto simp add: PO_hoare_defs l2_nostep_defs intro!: l2_inv3I)
apply (auto simp add: l2_defs bad_runs_def intro: synth_analz_increasing dest!: l2_inv3D)
apply (auto simp add: l2_inv3_aux_defs)
apply (blast intro: synth_analz_monotone dest!: subsetD [where A="chan _"])+
done
lemma l2_inv3_step4:
"{l2_inv3} l2_step4 Rb A B Ni gnx {> l2_inv3}"
apply (auto simp add: PO_hoare_defs l2_nostep_defs intro!: l2_inv3I, auto simp add: l2_defs)
apply (auto simp add: bad_runs_def intro:synth_analz_increasing dest!: l2_inv3D)
apply (auto simp add: l2_inv3_aux_defs dest!: subsetD [where A="chan _"])
done
lemma l2_inv3_dy_fake_msg:
"{l2_inv3} l2_dy_fake_msg M {> l2_inv3}"
apply (auto simp add: PO_hoare_defs l2_defs extr_insert_IK_eq
intro!: l2_inv3I
elim!: l2_inv3E dy_fake_msg_extr [THEN [2] rev_subsetD])
apply (auto intro!: fake_New
intro: synth_analz_increasing fake_monotone dy_fake_msg_monotone
dy_fake_msg_insert_chan
simp add: bad_runs_def elim!: l2_inv3E)
apply (auto simp add: l2_inv3_aux_defs intro: synth_analz_monotone
dest!: subsetD [where A="chan _"])
done
lemma l2_inv3_dy_fake_chan:
"{l2_inv3} l2_dy_fake_chan M {> l2_inv3}"
apply (auto simp add: PO_hoare_defs l2_defs
intro!: l2_inv3I
elim!: l2_inv3E)
apply (auto intro: synth_analz_increasing simp add: bad_runs_def elim!: l2_inv3E
dest:dy_fake_msg_extr [THEN [2] rev_subsetD]
dy_fake_chan_extr_insert [THEN [2] rev_subsetD]
dy_fake_chan_mono2)
apply (simp add: l2_inv3_aux_defs dy_fake_chan_def dy_fake_msg_def,
erule fake.cases, simp_all)
apply (auto simp add: l2_inv3_aux_defs elim!: synth_analz_monotone
dest!: subsetD [where A="chan _"])
done
lemma l2_inv3_lkr_others:
"{l2_inv3} l2_lkr_others A {> l2_inv3}"
apply (auto simp add: PO_hoare_defs l2_defs
intro!: l2_inv3I
dest!: extr_insert_bad [THEN [2] rev_subsetD]
elim!: l2_inv3E)
apply (auto simp add: l2_inv3_aux_defs bad_runs_def
intro: synth_analz_increasing synth_analz_monotone)
apply (drule synth_analz_mono [where G="extr _ _ _"], auto,
(drule rev_subsetD [where A="chan _"], simp)+, auto intro: synth_analz_increasing,
drule rev_subsetD [where A="synth (analz (extr _ _ _))"],
auto intro: synth_analz_monotone)+
done
lemma l2_inv3_lkr_after:
"{l2_inv3} l2_lkr_after A {> l2_inv3}"
apply (auto simp add: PO_hoare_defs l2_defs intro!: l2_inv3I
dest!: extr_insert_bad [THEN [2] rev_subsetD]
elim!: l2_inv3E)
apply (auto simp add: l2_inv3_aux_defs bad_runs_def
intro: synth_analz_increasing synth_analz_monotone)
apply (drule synth_analz_mono [where G="extr _ _ _"], auto,
(drule rev_subsetD [where A="chan _"], simp)+, auto intro: synth_analz_increasing,
drule rev_subsetD [where A="synth (analz (extr _ _ _))"],
auto intro: synth_analz_monotone)+
done
lemma l2_inv3_skr:
"{l2_inv3 ∩ l2_inv2} l2_skr R K {> l2_inv3}"
apply (auto simp add: PO_hoare_defs l2_defs intro!: l2_inv3I dest!: l2_inv2D)
apply (auto simp add: l2_inv3_aux_defs bad_runs_def intro: synth_analz_increasing
elim!: l2_inv3E)
apply (blast intro: synth_analz_monotone dest!: subsetD [where A="chan _"])+
done
lemmas l2_inv3_trans_aux =
l2_inv3_step1 l2_inv3_step2 l2_inv3_step3 l2_inv3_step4
l2_inv3_dy_fake_msg l2_inv3_dy_fake_chan
l2_inv3_lkr_others l2_inv3_lkr_after l2_inv3_skr
lemma l2_inv3_trans [iff]:
"{l2_inv3 ∩ l2_inv2} trans l2 {> l2_inv3}"
by (auto simp add: l2_nostep_defs intro:l2_inv3_trans_aux)
lemma PO_l2_inv3 [iff]: "reach l2 ⊆ l2_inv3"
by (rule_tac J="l2_inv2" in inv_rule_incr) (auto)
text ‹Auxiliary dest rule for inv3.›
lemmas l2_inv3D_aux =
l2_inv3D [THEN conjunct1,
THEN [2] subset_trans,
THEN synth_analz_mono, simplified,
THEN [2] rev_subsetD, rotated 1, OF IK_subset_extr]
lemma l2_inv3D_HashNonce1:
"s ∈ l2_inv3 ⟹
Hash ⟨NonceF (R$N), X⟩ ∈ synth (analz (extr (bad s) (ik s) (chan s))) ⟹
R ∈ bad_runs s"
apply (drule l2_inv3D, auto, drule synth_analz_monotone, auto simp add: analz_generators)
apply (erule synth.cases, auto)
done
lemma l2_inv3D_HashNonce2:
"s ∈ l2_inv3 ⟹
Hash ⟨X, NonceF (R$N)⟩ ∈ synth (analz (extr (bad s) (ik s) (chan s))) ⟹
R ∈ bad_runs s"
apply (drule l2_inv3D, auto, drule synth_analz_monotone, auto simp add: analz_generators)
apply (erule synth.cases, auto)
done
subsubsection ‹hmac preservation lemmas›
text ‹If @{term "(s, s') ∈ trans l2"} then the MACs (with secret keys) that the attacker knows in
@{term "s'"} (overapproximated by those in @{term "parts (extr (bad s') (ik s') (chan s'))"})
are already known in @{term "s"}, except in the case of the steps 2 and 3 of the protocol.
›
lemma hmac_key_unknown:
"hmac X K ∈ synth (analz H) ⟹ K ∉ synth (analz H) ⟹ hmac X K ∈ analz H"
by (erule synth.cases, auto)
lemma parts_exp [simp]:"parts {Exp X Y} = {Exp X Y}"
by (auto,erule parts.induct, auto)
lemma hmac_trans_1_4_skr_extr_fake:
"hmac X K ∈ parts (extr (bad s') (ik s') (chan s')) ⟹
K ∉ synth (analz (extr (bad s) (ik s) (chan s))) ⟹
s ∈ l2_inv2 ⟹
(s, s') ∈ l2_step1 Ra A B ∪ l2_step4 Rb A B Ni gnx ∪ l2_skr R KK ∪
l2_dy_fake_msg M ∪ l2_dy_fake_chan MM ⟹
hmac X K ∈ parts (extr (bad s) (ik s) (chan s))"
apply (auto simp add: l2_defs parts_insert [where H="extr _ _ _"]
parts_insert [where H="insert _ (extr _ _ _)"])
apply (auto dest!:l2_inv2D)
apply (auto dest!:dy_fake_chan_extr_insert_parts [THEN [2] rev_subsetD]
parts_monotone [of _ "{M}" "synth (analz (extr (bad s) (ik s) (chan s)))"],
auto simp add: dy_fake_msg_def)
done
lemma hmac_trans_2:
"hmac X K ∈ parts (extr (bad s') (ik s') (chan s')) ⟹
(s, s') ∈ l2_step2 Rb A B Ni gnx ⟹
hmac X K ∈ parts (extr (bad s) (ik s) (chan s)) ∨
(X = ⟨Number 0, gnx, Exp Gen (NonceF (Rb$ny)), Agent B, Agent A⟩ ∧
K = Hash ⟨Ni, NonceF (Rb$nr)⟩ ∧
guessed_runs Rb = ⦇role=Resp, owner=B, partner=A⦈ ∧
progress s' Rb = Some {xny, xni, xnr, xgnx, xgny, xsk} ∧
guessed_frame Rb xgnx = Some gnx ∧
guessed_frame Rb xni = Some Ni )"
apply (auto simp add: l2_defs parts_insert [where H="extr _ _ _"]
parts_insert [where H="insert _ (extr _ _ _)"])
done
lemma hmac_trans_3:
"hmac X K ∈ parts (extr (bad s') (ik s') (chan s')) ⟹
(s, s') ∈ l2_step3 Ra A B Nr gny ⟹
hmac X K ∈ parts (extr (bad s) (ik s) (chan s)) ∨
(X = ⟨Number 1, gny, Exp Gen (NonceF (Ra$nx)), Agent A, Agent B⟩ ∧
K = Hash ⟨NonceF (Ra$ni), Nr⟩ ∧
guessed_runs Ra = ⦇role=Init, owner=A, partner=B⦈ ∧
progress s' Ra = Some {xnx, xni, xnr, xgnx, xgny, xsk, xEnd} ∧
guessed_frame Ra xgny = Some gny ∧
guessed_frame Ra xnr = Some Nr)"
apply (auto simp add: l2_defs parts_insert [where H="extr _ _ _"]
parts_insert [where H="insert _ (extr _ _ _)"])
done
lemma hmac_trans_lkr_aux:
"hmac X K ∈ parts {M. ∃ x A B. Chan x A B M ∈ chan s} ⟹
K ∉ synth (analz (extr (bad s) (ik s) (chan s))) ⟹
s ∈ l2_inv3 ⟹
hmac X K ∈ parts (extr (bad s) (ik s) (chan s))"
proof -
assume A:"K ∉ synth (analz (extr (bad s) (ik s) (chan s)))" "s ∈ l2_inv3"
assume "hmac X K ∈ parts {M. ∃ x A B. Chan x A B M ∈ chan s}"
then obtain x A B M where H:"hmac X K ∈ parts {M}" and H':"Chan x A B M ∈ chan s"
by (auto dest: parts_singleton)
assume "s ∈ l2_inv3"
with H' have "M ∈ range Nonce ∨ M ∈ synth (analz (extr (bad s) (ik s) (chan s)))"
by (auto simp add: l2_inv3_aux_defs dest!: l2_inv3D, auto)
with H show ?thesis
proof (auto)
assume "M ∈ synth (analz (extr (bad s) (ik s) (chan s)))"
then have "{M} ⊆ synth (analz (extr (bad s) (ik s) (chan s)))" by (auto)
then have "parts {M} ⊆ parts (synth (analz (extr (bad s) (ik s) (chan s))))"
by (rule parts_mono)
with H have "hmac X K ∈ parts (synth (analz (extr (bad s) (ik s) (chan s))))" by auto
with A show ?thesis by auto
qed
qed
lemma hmac_trans_lkr:
"hmac X K ∈ parts (extr (bad s') (ik s') (chan s')) ⟹
K ∉ synth (analz (extr (bad s) (ik s) (chan s))) ⟹
s ∈ l2_inv3 ⟹
(s, s') ∈ l2_lkr_others A ∪ l2_lkr_after A ⟹
hmac X K ∈ parts (extr (bad s) (ik s) (chan s))"
apply (auto simp add: l2_defs
dest!: parts_monotone [OF _ extr_insert_bad])
apply (auto intro: parts_monotone intro!:hmac_trans_lkr_aux)
done
lemmas hmac_trans = hmac_trans_1_4_skr_extr_fake hmac_trans_lkr hmac_trans_2 hmac_trans_3
subsubsection ‹inv4 (authentication guard)›
text ‹If HMAC is @{term "parts (extr (bad s) (ik s) (chan s))"} and @{term "A"}, @{term "B"}
are honest then the message has indeed been sent by a responder run (etc).›
definition
l2_inv4 :: "l2_state set"
where
"l2_inv4 ≡ {s. ∀ Ra A B gny Nr.
hmac ⟨Number 0, Exp Gen (NonceF (Ra$nx)), gny, Agent B, Agent A⟩
(Hash ⟨NonceF (Ra$ni), Nr⟩) ∈ parts (extr (bad s) (ik s) (chan s)) ⟶
guessed_runs Ra = ⦇role=Init, owner=A, partner=B⦈ ⟶
A ∉ bad s ∧ B ∉ bad s ⟶
(∃ Rb. guessed_runs Rb = ⦇role=Resp, owner=B, partner=A⦈ ∧
in_progressS (progress s Rb) {xny, xni, xnr, xgnx, xgny, xsk} ∧
guessed_frame Rb xgny = Some gny ∧
guessed_frame Rb xnr = Some Nr ∧
guessed_frame Rb xni = Some (NonceF (Ra$ni)) ∧
guessed_frame Rb xgnx = Some (Exp Gen (NonceF (Ra$nx))))
}"
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_inv2 ∩ l2_inv3} trans l2 {> l2_inv4}"
proof (auto simp add: PO_hoare_defs intro!: l2_inv4I)
fix s' s :: l2_state
fix Ra A B gny Nr
assume HHparts:"hmac ⟨Number 0, Exp Gen (NonceF (Ra $ nx)), gny, Agent B, Agent A⟩
(Hash ⟨NonceF (Ra $ ni), Nr⟩)
∈ parts (extr (bad s') (ik s') (chan s'))"
assume HRa: "guessed_runs Ra = ⦇role=Init, owner=A, partner=B⦈"
assume Hi:"s ∈ l2_inv4" "s ∈ l2_inv2" "s ∈ l2_inv3"
assume Ht:"(s, s') ∈ trans l2"
assume "A ∉ bad s'" "B ∉ bad s'"
with Ht have Hb:"A ∉ bad s" "B ∉ bad s"
by (auto simp add: l2_nostep_defs) (simp_all add: l2_defs)
with HRa Hi
have HH:"Hash ⟨NonceF (Ra$ ni), Nr⟩ ∉ synth (analz (extr (bad s) (ik s) (chan s)))"
by (auto dest!: l2_inv3D_HashNonce1 simp add: bad_runs_def)
from Ht Hi HHparts HH
have "hmac ⟨Number 0, Exp Gen (NonceF (Ra $ nx)), gny, Agent B, Agent A⟩
(Hash ⟨NonceF (Ra $ ni), Nr⟩) ∈ parts (extr (bad s) (ik s) (chan s)) ∨
(∃ Rb. (s, s') ∈ l2_step2 Rb A B (NonceF (Ra$ni)) (Exp Gen (NonceF (Ra $ nx))) ∧
gny = Exp Gen (NonceF (Rb$ny)) ∧
Nr = NonceF (Rb$nr) ∧
guessed_runs Rb = ⦇role=Resp, owner=B, partner=A⦈ ∧
progress s' Rb = Some {xny, xni, xnr, xgnx, xgny, xsk} ∧
guessed_frame Rb xgnx = Some (Exp Gen (NonceF (Ra$nx))) ∧
guessed_frame Rb xni = Some (NonceF (Ra$ni)))"
apply (auto simp add: l2_nostep_defs)
apply (drule hmac_trans_1_4_skr_extr_fake, auto)
apply (drule hmac_trans_2, auto)
apply (drule hmac_trans_3, auto)
apply (drule hmac_trans_1_4_skr_extr_fake, auto)
apply (drule hmac_trans_1_4_skr_extr_fake, auto)
apply (drule hmac_trans_1_4_skr_extr_fake, auto)
apply (drule hmac_trans_lkr, auto)
apply (drule hmac_trans_lkr, auto)
apply (drule hmac_trans_1_4_skr_extr_fake, auto)
done
then show "∃Rb. guessed_runs Rb = ⦇role = Resp, owner = B, partner = A⦈ ∧
in_progressS (progress s' Rb) {xny, xni, xnr, xgnx, xgny, xsk} ∧
guessed_frame Rb xgny = Some gny ∧
guessed_frame Rb xnr = Some Nr ∧
guessed_frame Rb xni = Some (NonceF (Ra $ ni)) ∧
guessed_frame Rb xgnx = Some (Exp Gen (NonceF (Ra $ nx)))"
proof (auto)
assume
"hmac ⟨Number 0, Exp Gen (NonceF (Ra $ nx)), gny, Agent B, Agent A⟩
(hmac (NonceF (Ra $ ni)) Nr)
∈ parts (extr (bad s) (ik s) (chan s))"
with Hi Hb HRa obtain Rb where
HRb: "guessed_runs Rb = ⦇role = Resp, owner = B, partner = A⦈"
"in_progressS (progress s Rb) {xny, xni, xnr, xgnx, xgny, xsk}"
"guessed_frame Rb xgny = Some gny"
"guessed_frame Rb xnr = Some Nr"
"guessed_frame Rb xni = Some (NonceF (Ra $ ni))"
"guessed_frame Rb xgnx = Some (Exp Gen (NonceF (Ra $ nx)))"
by (auto dest!: l2_inv4D)
with Ht have "in_progressS (progress s' Rb) {xny, xni, xnr, xgnx, xgny, xsk}"
by (auto elim: in_progressS_trans)
with HRb show ?thesis by auto
qed
qed
lemma PO_l2_inv4 [iff]: "reach l2 ⊆ l2_inv4"
by (rule_tac J="l2_inv2 ∩ l2_inv3" in inv_rule_incr) (auto)
lemma auth_guard_step3:
"s ∈ l2_inv4 ⟹
s ∈ l2_inv1 ⟹
Insec B A ⟨gny, hmac ⟨Number 0, Exp Gen (NonceF (Ra$nx)), gny, Agent B, Agent A⟩
(Hash ⟨NonceF (Ra$ni), Nr⟩)⟩
∈ chan s ⟹
guessed_runs Ra = ⦇role=Init, owner=A, partner=B⦈ ⟹
can_signal s A B ⟹
(∃ Rb. guessed_runs Rb = ⦇role=Resp, owner=B, partner=A⦈ ∧
in_progressS (progress s Rb) {xny, xni, xnr, xgnx, xgny, xsk} ∧
guessed_frame Rb xgny = Some gny ∧
guessed_frame Rb xnr = Some Nr ∧
guessed_frame Rb xni = Some (NonceF (Ra$ni)) ∧
guessed_frame Rb xgnx = Some (Exp Gen (NonceF (Ra$nx))))"
proof -
assume "s ∈ l2_inv1" "can_signal s A B"
hence Hb:"A ∉ bad s" "B ∉ bad s" by auto
assume "Insec B A ⟨gny, hmac ⟨Number 0, Exp Gen (NonceF (Ra$nx)), gny, Agent B, Agent A⟩
(Hash ⟨NonceF (Ra$ni), Nr⟩)⟩ ∈ chan s"
hence HH:
"hmac ⟨Number 0, Exp Gen (NonceF (Ra$nx)), gny, Agent B, Agent A⟩
(Hash ⟨NonceF (Ra$ni), Nr⟩)
∈ parts (extr (bad s) (ik s) (chan s))" by auto
assume "s ∈ l2_inv4" "guessed_runs Ra = ⦇role=Init, owner=A, partner=B⦈"
with Hb HH show ?thesis by auto
qed
subsubsection ‹inv5 (authentication guard)›
text ‹If MAC is in @{term "parts (extr (bad s) (ik s) (chan s))"} and @{term "A"}, @{term "B"}
are honest then the message has indeed been sent by an initiator run (etc).›
definition
l2_inv5 :: "l2_state set"
where
"l2_inv5 ≡ {s. ∀ Rb A B gnx Ni.
hmac ⟨Number 1, Exp Gen (NonceF (Rb$ny)), gnx, Agent A, Agent B⟩
(Hash ⟨Ni, NonceF (Rb$nr)⟩) ∈ parts (extr (bad s) (ik s) (chan s)) ⟶
guessed_runs Rb = ⦇role=Resp, owner=B, partner=A⦈ ⟶
A ∉ bad s ∧ B ∉ bad s ⟶
(∃ Ra. guessed_runs Ra = ⦇role=Init, owner=A, partner=B⦈ ∧
in_progressS (progress s Ra) {xnx, xni, xnr, xgnx, xgny, xsk, xEnd} ∧
guessed_frame Ra xgnx = Some gnx ∧
guessed_frame Ra xni = Some Ni ∧
guessed_frame Ra xnr = Some (NonceF (Rb$nr)) ∧
guessed_frame Ra xgny = Some (Exp Gen (NonceF (Rb$ny))))
}"
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 ∩ l2_inv2 ∩ l2_inv3} trans l2 {> l2_inv5}"
proof (auto simp add: PO_hoare_defs intro!: l2_inv5I)
fix s' s :: l2_state
fix Rb A B gnx Ni
assume HHparts:"hmac ⟨Number (Suc 0), Exp Gen (NonceF (Rb$ny)), gnx, Agent A, Agent B⟩
(Hash ⟨Ni, NonceF (Rb$nr)⟩)
∈ parts (extr (bad s') (ik s') (chan s'))"
assume HRb: "guessed_runs Rb = ⦇role=Resp, owner=B, partner=A⦈"
assume Hi:"s ∈ l2_inv5" "s ∈ l2_inv2" "s ∈ l2_inv3"
assume Ht:"(s, s') ∈ trans l2"
assume "A ∉ bad s'" "B ∉ bad s'"
with Ht have Hb:"A ∉ bad s" "B ∉ bad s"
by (auto simp add: l2_nostep_defs) (simp_all add: l2_defs)
with HRb Hi have HH:"Hash ⟨Ni, NonceF (Rb$nr)⟩ ∉ synth (analz (extr (bad s) (ik s) (chan s)))"
by (auto dest!: l2_inv3D_HashNonce2 simp add: bad_runs_def)
from Ht Hi HHparts HH have "hmac ⟨Number 1, Exp Gen (NonceF (Rb$ny)), gnx, Agent A, Agent B⟩
(Hash ⟨Ni, NonceF (Rb$nr)⟩) ∈ parts (extr (bad s) (ik s) (chan s)) ∨
(∃ Ra. (s, s') ∈ l2_step3 Ra A B (NonceF (Rb$nr)) (Exp Gen (NonceF (Rb$ny))) ∧
gnx = Exp Gen (NonceF (Ra$nx)) ∧
Ni = NonceF (Ra$ni) ∧
guessed_runs Ra = ⦇role=Init, owner=A, partner=B⦈ ∧
progress s' Ra = Some {xnx, xni, xnr, xgnx, xgny, xsk, xEnd} ∧
guessed_frame Ra xgny = Some (Exp Gen (NonceF (Rb$ny))) ∧
guessed_frame Ra xnr = Some (NonceF (Rb$nr)))"
apply (auto simp add: l2_nostep_defs)
apply (drule hmac_trans_1_4_skr_extr_fake, auto)
apply (drule hmac_trans_2, auto)
apply (drule hmac_trans_3, auto)
apply (drule hmac_trans_1_4_skr_extr_fake, auto)
apply (drule hmac_trans_1_4_skr_extr_fake, auto)
apply (drule hmac_trans_1_4_skr_extr_fake, auto)
apply (drule hmac_trans_lkr, auto)
apply (drule hmac_trans_lkr, auto)
apply (drule hmac_trans_1_4_skr_extr_fake, auto)
done
then show "∃Ra. guessed_runs Ra = ⦇role=Init, owner=A, partner=B⦈ ∧
in_progressS (progress s' Ra) {xnx, xni, xnr, xgnx, xgny, xsk, xEnd} ∧
guessed_frame Ra xgnx = Some gnx ∧
guessed_frame Ra xni = Some Ni ∧
guessed_frame Ra xnr = Some (NonceF (Rb$nr)) ∧
guessed_frame Ra xgny = Some (Exp Gen (NonceF (Rb$ny)))"
proof (auto)
assume
"hmac ⟨Number (Suc 0), Exp Gen (NonceF (Rb$ny)), gnx, Agent A, Agent B⟩
(Hash ⟨Ni, NonceF (Rb$nr)⟩)
∈ parts (extr (bad s) (ik s) (chan s))"
with Hi Hb HRb obtain Ra where HRa:"guessed_runs Ra = ⦇role=Init, owner=A, partner=B⦈"
"in_progressS (progress s Ra) {xnx, xni, xnr, xgnx, xgny, xsk, xEnd}"
"guessed_frame Ra xgnx = Some gnx"
"guessed_frame Ra xni = Some Ni"
"guessed_frame Ra xnr = Some (NonceF (Rb$nr))"
"guessed_frame Ra xgny = Some (Exp Gen (NonceF (Rb$ny)))"
by (auto dest!: l2_inv5D)
with Ht have "in_progressS (progress s' Ra) {xnx, xni, xnr, xgnx, xgny, xsk, xEnd}"
by (auto elim: in_progressS_trans)
with HRa show ?thesis by auto
qed
qed
lemma PO_l2_inv5 [iff]: "reach l2 ⊆ l2_inv5"
by (rule_tac J="l2_inv2 ∩ l2_inv3" in inv_rule_incr) (auto)
lemma auth_guard_step4:
"s ∈ l2_inv5 ⟹
s ∈ l2_inv1 ⟹
Insec A B (hmac ⟨Number 1, Exp Gen (NonceF (Rb$ny)), gnx, Agent A, Agent B⟩
(Hash ⟨Ni, NonceF (Rb$nr)⟩))
∈ chan s ⟹
guessed_runs Rb = ⦇role=Resp, owner=B, partner=A⦈ ⟹
can_signal s A B ⟹
(∃ Ra. guessed_runs Ra = ⦇role=Init, owner=A, partner=B⦈ ∧
in_progressS (progress s Ra) {xnx, xni, xnr, xgnx, xgny, xsk, xEnd} ∧
guessed_frame Ra xgnx = Some gnx ∧
guessed_frame Ra xni = Some Ni ∧
guessed_frame Ra xnr = Some (NonceF (Rb$nr)) ∧
guessed_frame Ra xgny = Some (Exp Gen (NonceF (Rb$ny))))"
proof -
assume "s ∈ l2_inv1" "can_signal s A B"
hence Hb:"A ∉ bad s" "B ∉ bad s" by auto
assume "Insec A B (hmac ⟨Number 1, Exp Gen (NonceF (Rb$ny)), gnx, Agent A, Agent B⟩
(Hash ⟨Ni, NonceF (Rb$nr)⟩)) ∈ chan s"
hence HH:
"hmac ⟨Number 1, Exp Gen (NonceF (Rb$ny)), gnx, Agent A, Agent B⟩
(Hash ⟨Ni, NonceF (Rb$nr)⟩)
∈ parts (extr (bad s) (ik s) (chan s))" by auto
assume "s ∈ l2_inv5" "guessed_runs Rb = ⦇role=Resp, owner=B, partner=A⦈"
with Hb HH show ?thesis by auto
qed
subsubsection ‹inv6›
text ‹For an initiator, the session key is always $@{term "gny"}^@{term "nx"}$.›
definition
l2_inv6 :: "l2_state set"
where
"l2_inv6 ≡ {s. ∀Ra A B gny.
guessed_runs Ra = ⦇role=Init, owner=A, partner=B⦈ ⟶
in_progress (progress s Ra) xsk ⟶
guessed_frame Ra xgny = Some gny ⟶
guessed_frame Ra xsk = Some (Exp gny (NonceF (Ra$nx)))
}"
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)
done
lemma PO_l2_inv6 [iff]: "reach l2 ⊆ l2_inv6"
by (rule inv_rule_basic) (auto)
subsubsection ‹inv6'›
text ‹For a responder, the session key is always $@{term "gnx"}^@{term "ny"}$.›
definition
l2_inv6' :: "l2_state set"
where
"l2_inv6' ≡ {s. ∀Rb A B gnx.
guessed_runs Rb = ⦇role=Resp, owner=B, partner=A⦈ ⟶
in_progress (progress s Rb) xsk ⟶
guessed_frame Rb xgnx = Some gnx ⟶
guessed_frame Rb xsk = Some (Exp gnx (NonceF (Rb$ny)))
}"
lemmas l2_inv6'I = l2_inv6'_def [THEN setc_def_to_intro, rule_format]
lemmas l2_inv6'E [elim] = l2_inv6'_def [THEN setc_def_to_elim, rule_format]
lemmas l2_inv6'D = 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_inv6'I)
apply (auto simp add: l2_defs dy_fake_chan_def)
done
lemma PO_l2_inv6' [iff]: "reach l2 ⊆ l2_inv6'"
by (rule inv_rule_basic) (auto)
subsubsection ‹inv7: form of the secrets›
definition
l2_inv7 :: "l2_state set"
where
"l2_inv7 ≡ {s.
secret s ⊆ {Exp (Exp Gen (NonceF (R$N))) (NonceF (R'$N')) | N N' R R'.
R = test ∧ R' ∈ partners ∧ (N=nx ∨ N=ny) ∧ (N'=nx ∨ N'=ny)}
}"
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)
text ‹Steps 3 and 4 are the hard part.›
lemma l2_inv7_step3:
"{l2_inv7 ∩ l2_inv1 ∩ l2_inv4 ∩ l2_inv6'} l2_step3 Ra A B Nr gny {> l2_inv7}"
proof (auto simp add: PO_hoare_defs intro!: l2_inv7I)
fix s s' :: l2_state fix x
assume Hi:"s ∈ l2_inv1" "s ∈ l2_inv7" "s ∈ l2_inv4" "s ∈ l2_inv6'"
assume Ht:"(s, s') ∈ l2_step3 Ra A B Nr gny"
assume Hs:"x ∈ secret s'"
from Hs Ht have "x ∈ secret s ∨ (Ra = test ∧ x = Exp gny (NonceF (Ra$nx)))"
by (auto simp add: l2_defs)
with Hi Ht
show "∃N N' R'. x = Exp (Exp Gen (NonceF (R' $ N'))) (NonceF (test $ N)) ∧
R' ∈ partners ∧ (N = nx ∨ N = ny) ∧ (N' = nx ∨ N' = ny)"
proof (auto dest: l2_inv7D simp add: l2_defs)
assume Htest: "guessed_runs test = ⦇role = Init, owner = A, partner = B⦈"
"guessed_frame test xgny = Some gny"
"guessed_frame test xnr = Some Nr"
"guessed_frame test xsk = Some (Exp gny (NonceF (test $ nx)))"
assume
"Insec B A ⟨gny, hmac ⟨Number 0, Exp Gen (NonceF (test$nx)), gny, Agent B, Agent A⟩
(Hash ⟨NonceF (test$ni), Nr⟩)⟩
∈ chan s"
"can_signal s A B"
with Htest Hi obtain Rb where HRb:
"guessed_runs Rb = ⦇role=Resp, owner=B, partner=A⦈"
"in_progressS (progress s Rb) {xny, xni, xnr, xgnx, xgny, xsk}"
"gny = Exp Gen (NonceF (Rb$ny))"
"Nr = NonceF (Rb$nr)"
"guessed_frame Rb xni = Some (NonceF (test$ni))"
"guessed_frame Rb xgnx = Some (Exp Gen (NonceF (test$nx)))"
by (auto dest!: auth_guard_step3)
with Hi
have "guessed_frame Rb xsk = Some (Exp (Exp Gen (NonceF (Rb$ny))) (NonceF (test$nx)))"
by (auto dest: l2_inv6'D)
with HRb Htest have "Rb ∈ partners"
by (auto simp add: partners_def partner_runs_def, simp add: matching_def)
with HRb have "Exp gny (NonceF (test $ nx)) =
Exp (Exp Gen (NonceF (Rb $ ny))) (NonceF (test $ nx)) ∧ Rb ∈ partners"
by auto
then show "∃N N' R'.
Exp gny (NonceF (test $ nx)) = Exp (Exp Gen (NonceF (R' $ N'))) (NonceF (test $ N)) ∧
R' ∈ partners ∧ (N = nx ∨ N = ny) ∧ (N' = nx ∨ N' = ny)"
by blast
qed (auto simp add: can_signal_def)
qed
lemma l2_inv7_step4:
"{l2_inv7 ∩ l2_inv1 ∩ l2_inv5 ∩ l2_inv6 ∩ l2_inv6'} l2_step4 Rb A B Ni gnx {> l2_inv7}"
proof (auto simp add: PO_hoare_defs intro!: l2_inv7I)
fix s s' :: l2_state fix x
assume Hi:"s ∈ l2_inv1" "s ∈ l2_inv7" "s ∈ l2_inv5" "s ∈ l2_inv6" "s ∈ l2_inv6'"
assume Ht:"(s, s') ∈ l2_step4 Rb A B Ni gnx"
assume Hs:"x ∈ secret s'"
from Hs Ht have "x ∈ secret s ∨ (Rb = test ∧ x = Exp gnx (NonceF (Rb$ny)))"
by (auto simp add: l2_defs)
with Hi Ht
show "∃N N' R'. x = Exp (Exp Gen (NonceF (R' $ N'))) (NonceF (test $ N)) ∧ R' ∈ partners
∧ (N = nx ∨ N = ny) ∧ (N' = nx ∨ N' = ny)"
proof (auto dest: l2_inv7D simp add: l2_defs)
assume Htest: "guessed_runs test = ⦇role = Resp, owner = B, partner = A⦈"
"guessed_frame test xgnx = Some gnx"
"guessed_frame test xni = Some Ni"
assume "progress s test = Some {xny, xni, xnr, xgnx, xgny, xsk}"
with Htest Hi have Htest': "guessed_frame test xsk = Some (Exp gnx (NonceF (test $ ny)))"
by (auto dest: l2_inv6'D)
assume
"Insec A B (hmac ⟨Number (Suc 0), Exp Gen (NonceF (test$ny)), gnx, Agent A, Agent B⟩
(Hash ⟨Ni, NonceF (test $ nr)⟩))
∈ chan s"
"can_signal s A B"
with Hi Htest obtain Ra where HRa:
"guessed_runs Ra = ⦇role=Init, owner=A, partner=B⦈"
"in_progressS (progress s Ra) {xnx, xni, xnr, xgnx, xgny, xsk, xEnd}"
"gnx = Exp Gen (NonceF (Ra$nx))"
"Ni = NonceF (Ra$ni)"
"guessed_frame Ra xgny = Some (Exp Gen (NonceF (test$ny)))"
"guessed_frame Ra xnr = Some (NonceF (test$nr))"
by (auto dest!: auth_guard_step4)
with Hi
have "guessed_frame Ra xsk = Some (Exp (Exp Gen (NonceF (Ra$nx))) (NonceF (test$ny)))"
by (auto dest: l2_inv6D)
with HRa Htest Htest' have "Ra ∈ partners"
by (auto simp add: partners_def partner_runs_def, simp add: matching_def)
with HRa have "Exp gnx (NonceF (test $ ny)) =
Exp (Exp Gen (NonceF (Ra $ nx))) (NonceF (test $ ny)) ∧ Ra ∈ partners"
by auto
then show "∃N N' R'.
Exp gnx (NonceF (test $ ny))
= Exp (Exp Gen (NonceF (R' $ N'))) (NonceF (test $ N)) ∧
R' ∈ partners ∧ (N = nx ∨ N = ny) ∧ (N' = nx ∨ N' = ny)"
by auto
qed (auto simp add: can_signal_def)
qed
lemma l2_inv7_trans [iff]:
"{l2_inv7 ∩ l2_inv1 ∩ l2_inv4 ∩ l2_inv5 ∩ l2_inv6 ∩ l2_inv6'} trans l2 {> l2_inv7}"
apply (auto simp add: l2_nostep_defs intro!: l2_inv7_step3 l2_inv7_step4)
apply (auto simp add: PO_hoare_defs intro!: l2_inv7I)
apply (auto simp add: l2_defs dy_fake_chan_def dest: l2_inv7D)
done
lemma PO_l2_inv7 [iff]: "reach l2 ⊆ l2_inv7"
by (rule_tac J="l2_inv1 ∩ l2_inv4 ∩ l2_inv5 ∩ l2_inv6 ∩ l2_inv6'" in inv_rule_incr) (auto)
text ‹auxiliary dest rule for inv7›
lemma Exp_Exp_Gen_synth:
"Exp (Exp Gen X) Y ∈ synth H ⟹ Exp (Exp Gen X) Y ∈ H ∨ X ∈ synth H ∨ Y ∈ synth H"
by (erule synth.cases, auto dest: Exp_Exp_Gen_inj2)
lemma l2_inv7_aux:
"s ∈ l2_inv7 ⟹
x ∈ secret s ⟹
x ∉ synth (analz (generators s))"
apply (auto simp add: analz_generators dest!: l2_inv7D [THEN [2] rev_subsetD])
apply (auto dest!: Exp_Exp_Gen_synth Exp_Exp_Gen_inj2)
done
subsection ‹Refinement›
text ‹Mediator function.›
definition
med12s :: "l2_obs ⇒ skl1_obs"
where
"med12s t ≡ ⦇
ik = ik t,
secret = secret t,
progress = progress t,
signalsInit = signalsInit t,
signalsResp = signalsResp t,
signalsInit2 = signalsInit2 t,
signalsResp2 = signalsResp2 t
⦈"
text ‹Relation between states.›
definition
R12s :: "(skl1_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} skl1_step1 Ra A B, l2_step1 Ra A B {>R12s}"
by (auto simp add: PO_rhoare_defs R12s_defs skl1_step1_def l2_step1_def)
lemma l2_step2_refines_step2:
"{R12s} skl1_step2 Rb A B Ni gnx, l2_step2 Rb A B Ni gnx {>R12s}"
by (auto simp add: PO_rhoare_defs R12s_defs skl1_step2_def, simp_all add: l2_step2_def)
text ‹for step3 and 4, we prove the level 1 guard, i.e.,
"the future session key is not in @{term "synth (analz (ik s))"}",
using the fact that inv8 also holds for the future state in which the session key is already in
@{term "secret s"}›
lemma l2_step3_refines_step3:
"{R12s ∩ UNIV × (l2_inv1 ∩ l2_inv3 ∩ l2_inv4 ∩ l2_inv6' ∩ l2_inv7)}
skl1_step3 Ra A B Nr gny, l2_step3 Ra A B Nr gny
{>R12s}"
proof (auto simp add: PO_rhoare_defs R12s_defs)
fix s s'
assume Hi:"s ∈ l2_inv1" "s ∈ l2_inv4" "s∈ l2_inv6'"
assume Ht: "(s, s') ∈ l2_step3 Ra A B Nr gny"
assume "s ∈ l2_inv7" "s ∈ l2_inv3"
with Hi Ht l2_inv7_step3 l2_inv3_step3 have Hi':"s' ∈ l2_inv7" "s'∈ l2_inv3"
by (auto simp add: PO_hoare_defs, blast, blast)
from Ht have "Ra = test ⟶ Exp gny (NonceF (Ra$nx)) ∈ secret s'"
by (auto simp add: l2_defs)
with Hi' have "Ra = test ⟶ Exp gny (NonceF (Ra$nx)) ∉ synth (analz (generators s'))"
by (auto dest: l2_inv7_aux)
with Hi' have G2:"Ra = test ⟶ Exp gny (NonceF (Ra$nx)) ∉ synth (analz (ik s'))"
by (auto dest!: l2_inv3D_aux)
from Ht Hi have G1:
"can_signal s A B ⟶ (∃ Rb. guessed_runs Rb = ⦇role=Resp, owner=B, partner=A⦈ ∧
in_progressS (progress s Rb) {xny, xni, xnr, xgnx, xgny, xsk} ∧
gny = Exp Gen (NonceF (Rb$ny)) ∧
Nr = NonceF (Rb$nr) ∧
guessed_frame Rb xgnx = Some (Exp Gen (NonceF (Ra$nx))) ∧
guessed_frame Rb xni = Some (NonceF (Ra$ni)))"
by (auto dest!: auth_guard_step3 simp add: l2_defs)
with Ht G1 G2 show
"(⦇ik = ik s, secret = secret s, progress = progress s,
signalsInit = signalsInit s, signalsResp = signalsResp s,
signalsInit2 = signalsInit2 s, signalsResp2 = signalsResp2 s⦈,
⦇ik = ik s', secret = secret s', progress = progress s',
signalsInit = signalsInit s', signalsResp = signalsResp s',
signalsInit2 = signalsInit2 s', signalsResp2 = signalsResp2 s'⦈)
∈ skl1_step3 Ra A B Nr gny"
apply (auto simp add: l2_step3_def, auto simp add: skl1_step3_def)
apply (auto simp add: can_signal_def)
done
qed
lemma l2_step4_refines_step4:
"{R12s ∩ UNIV × (l2_inv1 ∩ l2_inv3 ∩ l2_inv5 ∩ l2_inv6 ∩ l2_inv6' ∩ l2_inv7)}
skl1_step4 Rb A B Ni gnx, l2_step4 Rb A B Ni gnx
{>R12s}"
proof (auto simp add: PO_rhoare_defs R12s_defs)
fix s s'
assume Hi:"s ∈ l2_inv1" "s ∈ l2_inv5" "s ∈ l2_inv6" "s ∈ l2_inv6'"
assume Ht: "(s, s') ∈ l2_step4 Rb A B Ni gnx"
assume "s ∈ l2_inv7" "s ∈ l2_inv3"
with Hi Ht l2_inv7_step4 l2_inv3_step4 have Hi':"s' ∈ l2_inv7" "s' ∈ l2_inv3"
by (auto simp add: PO_hoare_defs, blast, blast)
from Ht have "Rb = test ⟶ Exp gnx (NonceF (Rb$ny)) ∈ secret s'"
by (auto simp add: l2_defs)
with Hi' have "Rb = test ⟶ Exp gnx (NonceF (Rb$ny)) ∉ synth (analz (generators s'))"
by (auto dest: l2_inv7_aux)
with Hi' have G2:"Rb = test ⟶ Exp gnx (NonceF (Rb$ny)) ∉ synth (analz (ik s'))"
by (auto dest!: l2_inv3D_aux)
from Ht Hi have G1:
"can_signal s A B ⟶ (∃ Ra. guessed_runs Ra = ⦇role=Init, owner=A, partner=B⦈ ∧
in_progressS (progress s Ra) {xnx, xni, xnr, xgnx, xgny, xsk, xEnd} ∧
guessed_frame Ra xgnx = Some gnx ∧
guessed_frame Ra xni = Some Ni ∧
guessed_frame Ra xgny = Some (Exp Gen (NonceF (Rb$ny))) ∧
guessed_frame Ra xnr = Some (NonceF (Rb$nr)))"
by (auto dest!: auth_guard_step4 simp add: l2_defs)
with Ht G1 G2 show
"(⦇ik = ik s, secret = secret s, progress = progress s,
signalsInit = signalsInit s, signalsResp = signalsResp s,
signalsInit2 = signalsInit2 s, signalsResp2 = signalsResp2 s⦈,
⦇ik = ik s', secret = secret s', progress = progress s',
signalsInit = signalsInit s', signalsResp = signalsResp s',
signalsInit2 = signalsInit2 s', signalsResp2 = signalsResp2 s'⦈)
∈ skl1_step4 Rb A B Ni gnx"
apply (auto simp add: l2_step4_def, auto simp add: skl1_step4_def)
apply (auto simp add: can_signal_def)
done
qed
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_inv3 ∩ l2_inv7)} 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_inv3D [THEN conjunct1])
apply (auto dest!: l2_inv7_aux)
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_inv2 ∩ l2_inv3 ∩ l2_inv7)} 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_inv2" "s ∈ l2_inv3"
"R ∉ partners" "R ≠ test" "in_progress (progress s R) xsk" "guessed_frame R xsk = Some K"
assume Hx:"x ∈ synth (analz (insert K (ik s)))"
assume "x ∈ secret s" "s ∈ l2_inv7"
then obtain R R' N N' where Hx':"x = Exp (Exp Gen (NonceF (R$N))) (NonceF (R'$N'))"
"R = test ∧ R' ∈ partners ∧ (N=nx ∨ N=ny) ∧ (N'=nx ∨ N'=ny)"
by (auto dest!: l2_inv7D subsetD)
from H have "s ⦇ik := insert K (ik s)⦈ ∈ l2_inv3"
by (auto intro: hoare_apply [OF l2_inv3_skr] simp add: l2_defs)
with Hx have "x ∈ synth (analz (generators (s ⦇ik := insert K (ik s)⦈)))"
by (auto dest: l2_inv3D_aux)
with Hx' show False
by (auto dest!: Exp_Exp_Gen_synth dest: Exp_Exp_Gen_inj2 simp add: analz_generators)
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 l2_step4_refines_step4
lemma l2_refines_init_l1 [iff]:
"init l2 ⊆ R12s `` (init skl1)"
by (auto simp add: R12s_defs skl1_defs l2_loc_defs)
lemma l2_refines_trans_l1 [iff]:
"{R12s ∩ (UNIV × (l2_inv1 ∩ l2_inv2 ∩ l2_inv3 ∩ l2_inv4 ∩ l2_inv5 ∩
l2_inv6 ∩ l2_inv6' ∩ l2_inv7))}
trans skl1, trans l2
{> R12s}"
by (auto 0 3 simp add: skl1_def l2_def skl1_trans_def l2_trans_def
intro!: l2_trans_refines_l1_trans)
lemma PO_obs_consistent_R12s [iff]:
"obs_consistent R12s med12s skl1 l2"
by (auto simp add: obs_consistent_def R12s_def med12s_def l2_defs)
lemma l2_refines_l1 [iff]:
"refines
(R12s ∩
(reach skl1 × (l2_inv1 ∩ l2_inv2 ∩ l2_inv3 ∩ l2_inv4 ∩ l2_inv5 ∩
l2_inv6 ∩ l2_inv6' ∩ l2_inv7)))
med12s skl1 l2"
by (rule Refinement_using_invariants, auto)
lemma l2_implements_l1 [iff]:
"implements med12s skl1 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 skl1_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_Init ≡ l1_iagreement_Init"
lemma l2_obs_iagreement_Init [iff]: "oreach l2 ⊆ l2_iagreement_Init"
apply (rule external_invariant_translation
[OF skl1_obs_iagreement_Init _ l2_implements_l1])
apply (auto simp add: med12s_def l1_iagreement_Init_def)
done
lemma l2_iagreement_Init [iff]: "reach l2 ⊆ l2_iagreement_Init"
by (rule external_to_internal_invariant [OF l2_obs_iagreement_Init], auto)
abbreviation "l2_iagreement_Resp ≡ l1_iagreement_Resp"
lemma l2_obs_iagreement_Resp [iff]: "oreach l2 ⊆ l2_iagreement_Resp"
apply (rule external_invariant_translation
[OF skl1_obs_iagreement_Resp _ l2_implements_l1])
apply (auto simp add: med12s_def l1_iagreement_Resp_def)
done
lemma l2_iagreement_Resp [iff]: "reach l2 ⊆ l2_iagreement_Resp"
by (rule external_to_internal_invariant [OF l2_obs_iagreement_Resp], auto)
end