Theory dhlvl2
section ‹Authenticated Diffie-Hellman Protocol (L2)›
theory dhlvl2
imports dhlvl1 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)
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:
\begin{itemize}
\item step 1: create @{term "Ra"}, @{term "A"} generates @{term "nx"},
computes and insecurely sends $@{term "g"}^@{term "nx"}$
\item step 2: create @{term "Rb"}, @{term "B"} receives $@{term "g"}^@{term "nx"}$ insecurely,
generates @{term "ny"}, computes $@{term "g"}^@{term "ny"}$,
authentically sends $(@{term "g"}^@{term "ny"}, @{term "g"}^@{term "nx"})$,
computes $@{term "g"}^@{term "nx*ny"}$,
emits a running signal for @{term "Init"}, $@{term "g"}^@{term "nx*ny"}$
\item step 3: @{term "A"} receives $@{term "g"}^@{term "ny"}$ and $@{term "g"}^@{term "nx"}$
authentically,
sends $(@{term "g"}^@{term "nx"}, @{term "g"}^@{term "ny"})$ authentically,
computes $@{term "g"}^@{term "ny*nx"}$, emits a commit signal for @{term "Init"},
$@{term "g"}^@{term "ny*nx"}$, a running signal for @{term "Resp"}, $@{term "g"}^@{term "ny*nx"}$,
declares the secret $@{term "g"}^@{term "ny*nx"}$
\item step 4: @{term "B"} receives $@{term "g"}^@{term "nx"}$ and $@{term "g"}^@{term "ny"}$
authentically,
emits a commit signal for @{term "Resp"}, $@{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, xgnx}),
chan := {Insec A B (Exp Gen (NonceF (Ra$nx)))} ∪ (chan s)
⦈
}"
definition
l2_step2 :: "rid_t ⇒ agent ⇒ agent ⇒ msg ⇒ l2_trans"
where
"l2_step2 Rb A B 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 xsk = Some (Exp gnx (NonceF (Rb$ny))) ∧
Insec A B gnx ∈ chan s ∧
s' = s⦇ progress := (progress s)(Rb ↦ {xny, xgny, xgnx, xsk}),
chan := {Auth B A ⟨Number 0, Exp Gen (NonceF (Rb$ny)), gnx⟩} ∪ (chan s),
signalsInit := if can_signal s A B then
addSignal (signalsInit s) (Running A B (Exp gnx (NonceF (Rb$ny))))
else
signalsInit s
⦈
}"
definition
l2_step3 :: "rid_t ⇒ agent ⇒ agent ⇒ msg ⇒ l2_trans"
where
"l2_step3 Ra A B gny ≡ {(s, s').
guessed_runs Ra = ⦇role=Init, owner=A, partner=B⦈ ∧
progress s Ra = Some {xnx, xgnx} ∧
guessed_frame Ra xgny = Some gny ∧
guessed_frame Ra xsk = Some (Exp gny (NonceF (Ra$nx))) ∧
Auth B A ⟨Number 0, gny, Exp Gen (NonceF (Ra$nx))⟩ ∈ chan s ∧
s' = s⦇ progress := (progress s)(Ra ↦ {xnx, xgnx, xgny, xsk, xEnd}),
chan := {Auth A B ⟨Number 1, Exp Gen (NonceF (Ra$nx)), gny⟩} ∪ 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 (Exp gny (NonceF (Ra$nx))))
else
signalsInit s,
signalsResp := if can_signal s A B then
addSignal (signalsResp s) (Running A B (Exp gny (NonceF (Ra$nx))))
else
signalsResp s
⦈
}"
definition
l2_step4 :: "rid_t ⇒ agent ⇒ agent ⇒ msg ⇒ l2_trans"
where
"l2_step4 Rb A B gnx ≡ {(s, s').
guessed_runs Rb = ⦇role=Resp, owner=B, partner=A⦈ ∧
progress s Rb = Some {xny, xgnx, xgny, xsk} ∧
guessed_frame Rb xgnx = Some gnx ∧
Auth A B ⟨Number 1, gnx, Exp Gen (NonceF (Rb$ny))⟩ ∈ chan s ∧
s' = s⦇ progress := (progress s)(Rb ↦ {xny, 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 (Exp gnx (NonceF (Rb$ny))))
else
signalsResp s
⦈
}"
text ‹Specification.›
definition
l2_init :: "l2_state set"
where
"l2_init ≡ { ⦇
ik = {},
secret = {},
progress = Map.empty,
signalsInit = λx. 0,
signalsResp = λx. 0,
chan = {},
bad = bad_init
⦈}"
definition
l2_trans :: "l2_trans" where
"l2_trans ≡ (⋃m M X Rb Ra A B K.
l2_step1 Ra A B ∪
l2_step2 Rb A B X ∪
l2_step3 Ra A B X ∪
l2_step4 Rb A B X ∪
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
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)
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 A and 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 B A ⟨Number 0, gny, Exp Gen (NonceF (Ra$nx))⟩ ∈ chan s"} and @{term "A"},
@{term "B"} are honest then the message has indeed been sent by a responder run (etc).›
definition
l2_inv2 :: "l2_state set"
where
"l2_inv2 ≡ {s. ∀ Ra A B gny.
Auth B A ⟨Number 0, gny, Exp Gen (NonceF (Ra$nx))⟩ ∈ chan s ⟶
A ∉ bad s ∧ B ∉ bad s ⟶
(∃ Rb. guessed_runs Rb = ⦇role=Resp, owner=B, partner=A⦈ ∧
in_progressS (progress s Rb) {xny, xgnx, xgny, xsk} ∧
gny = Exp Gen (NonceF (Rb$ny)) ∧
guessed_frame Rb xgnx = Some (Exp Gen (NonceF (Ra$nx))))
}"
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 ‹Auth A B ⟨Number 1, gnx, Exp Gen (NonceF (Rb$ny))⟩ ∈ chan s› and @{term "A"},
@{term "B"} are honest
then the message has indeed been sent by an initiator run (etc).›
definition
l2_inv3 :: "l2_state set"
where
"l2_inv3 ≡ {s. ∀ Rb A B gnx.
Auth A B ⟨Number 1, gnx, Exp Gen (NonceF (Rb$ny))⟩ ∈ chan s ⟶
A ∉ bad s ∧ B ∉ bad s ⟶
(∃ Ra. guessed_runs Ra = ⦇role=Init, owner=A, partner=B⦈ ∧
in_progressS (progress s Ra) {xnx, xgnx, xgny, xsk, xEnd} ∧
guessed_frame Ra xgnx = Some gnx ∧
guessed_frame Ra xgny = Some (Exp Gen (NonceF (Rb$ny))))
}"
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 insert_ident)
apply force+
done
lemma PO_l2_inv3 [iff]: "reach l2 ⊆ l2_inv3"
by (rule inv_rule_basic) (auto)
subsubsection ‹inv4›
text ‹For an initiator, the session key is always ‹gny^nx›.›
definition
l2_inv4 :: "l2_state set"
where
"l2_inv4 ≡ {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_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} 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)
done
lemma PO_l2_inv4 [iff]: "reach l2 ⊆ l2_inv4"
by (rule inv_rule_basic) (auto)
subsubsection ‹inv4'›
text ‹For a responder, the session key is always ‹gnx^ny›.›
definition
l2_inv4' :: "l2_state set"
where
"l2_inv4' ≡ {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_inv4'I = l2_inv4'_def [THEN setc_def_to_intro, rule_format]
lemmas l2_inv4'E [elim] = l2_inv4'_def [THEN setc_def_to_elim, rule_format]
lemmas l2_inv4'D = 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'} trans l2 {> l2_inv4'}"
apply (auto simp add: PO_hoare_defs l2_nostep_defs intro!: l2_inv4'I)
apply (auto simp add: l2_defs dy_fake_chan_def)
done
lemma PO_l2_inv4' [iff]: "reach l2 ⊆ l2_inv4'"
by (rule inv_rule_basic) (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 ‹For a run @{term "R"} (with any role), the session key always has the form
$something^n$ where $n$ is a nonce generated by @{term "R"}.›
definition
l2_inv6 :: "l2_state set"
where
"l2_inv6 ≡ {s. ∀R.
in_progress (progress s R) xsk ⟶
(∃ X N.
guessed_frame R xsk = Some (Exp X (NonceF (R$N))))
}"
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 ≡ {x. ∃ N. x = Exp Gen (Nonce N)} ∪
{Exp y (NonceF (R$N)) |y N 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 intro: synth_analz_increasing)
done
lemma l2_inv7_step2:
"{l2_inv7} l2_step2 Rb A B gnx {> l2_inv7}"
apply (auto simp add: PO_hoare_defs l2_nostep_defs intro!: l2_inv7I, auto simp add: l2_defs)
apply (auto intro: synth_analz_increasing)
done
lemma l2_inv7_step3:
"{l2_inv7} l2_step3 Ra A B gny {> l2_inv7}"
apply (auto simp add: PO_hoare_defs l2_nostep_defs intro!: l2_inv7I, auto simp add: l2_defs)
apply (auto intro: synth_analz_increasing)
apply (auto dest:l2_inv7D [THEN [2] rev_subsetD] dest!:extr_Chan)
done
lemma l2_inv7_step4:
"{l2_inv7} l2_step4 Rb A B gnx {> l2_inv7}"
by (auto simp add: PO_hoare_defs l2_nostep_defs intro!: l2_inv7I, auto simp add: l2_defs)
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}"
apply (auto simp add: PO_hoare_defs l2_defs intro!: l2_inv7I)
apply (auto simp add: extr_insert_IK_eq dest!: l2_inv6D)
apply (auto intro: synth_analz_increasing)
done
lemmas l2_inv7_trans_aux =
l2_inv7_step1 l2_inv7_step2 l2_inv7_step3 l2_inv7_step4
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_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_inv5 ∩ l2_inv6" in inv_rule_incr) (auto)
text ‹Auxiliary dest rule for inv7.›
lemmas l2_inv7D_aux =
l2_inv7D [THEN [2] subset_trans, THEN synth_analz_mono, simplified,
THEN [2] rev_subsetD, rotated 1, OF IK_subset_extr]
subsubsection ‹inv8: form of the secrets›
definition
l2_inv8 :: "l2_state set"
where
"l2_inv8 ≡ {s.
secret s ⊆ {Exp (Exp Gen (NonceF (R$N))) (NonceF (R'$N')) | N N' R 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)
text ‹Steps 3 and 4 are the hard part.›
lemma l2_inv8_step3:
"{l2_inv8 ∩ l2_inv1 ∩ l2_inv2 ∩ l2_inv4'} l2_step3 Ra A B gny {> l2_inv8}"
proof (auto simp add: PO_hoare_defs intro!: l2_inv8I)
fix s s' :: l2_state fix x
assume Hi:"s ∈ l2_inv1" "s ∈ l2_inv8" "s ∈ l2_inv2" "s ∈ l2_inv4'"
assume Ht:"(s, s') ∈ l2_step3 Ra A B 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"
proof (auto dest: l2_inv8D simp add: l2_defs)
assume Hx: "x = Exp gny (NonceF (test $ nx))"
assume "can_signal s A B"
with Hi have HA: "A ∉ bad s ∧ B ∉ bad s"
by auto
assume Htest: "guessed_runs test = ⦇role = Init, owner = A, partner = B⦈"
"guessed_frame test xgny = Some gny"
"guessed_frame test xsk = Some (Exp gny (NonceF (test $ nx)))"
assume "Auth B A ⟨Number 0, gny, Exp Gen (NonceF (test $ nx))⟩ ∈ chan s"
with Hi HA obtain Rb where HRb:
"guessed_runs Rb = ⦇role=Resp, owner=B, partner=A⦈"
"in_progressS (progress s Rb) {xny, xgnx, xgny, xsk}"
"gny = Exp Gen (NonceF (Rb$ny))"
"guessed_frame Rb xgnx = Some (Exp Gen (NonceF (test$nx)))"
by (auto dest!: l2_inv2D)
with Hi
have "guessed_frame Rb xsk = Some (Exp (Exp Gen (NonceF (Rb$ny))) (NonceF (test$nx)))"
by (auto dest: l2_inv4'D)
with HRb Htest have "Rb ∈ partners"
by (auto simp add: partners_def partner_runs_def 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"
by blast
qed (auto simp add: can_signal_def)
qed
lemma l2_inv8_step4:
"{l2_inv8 ∩ l2_inv1 ∩ l2_inv3 ∩ l2_inv4 ∩ l2_inv4'} l2_step4 Rb A B gnx {> l2_inv8}"
proof (auto simp add: PO_hoare_defs intro!: l2_inv8I)
fix s s' :: l2_state fix x
assume Hi:"s ∈ l2_inv1" "s ∈ l2_inv8" "s ∈ l2_inv3" "s ∈ l2_inv4" "s ∈ l2_inv4'"
assume Ht:"(s, s') ∈ l2_step4 Rb A B 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"
proof (auto dest: l2_inv8D simp add: l2_defs)
assume Hx: "x = Exp gnx (NonceF (test $ ny))"
assume "can_signal s A B"
with Hi have HA: "A ∉ bad s ∧ B ∉ bad s"
by auto
assume Htest: "guessed_runs test = ⦇role = Resp, owner = B, partner = A⦈"
"guessed_frame test xgnx = Some gnx"
assume "progress s test = Some {xny, xgnx, xgny, xsk}"
with Htest Hi have Htest': "guessed_frame test xsk = Some (Exp gnx (NonceF (test $ ny)))"
by (auto dest: l2_inv4'D)
assume "Auth A B ⟨Number (Suc 0), gnx, Exp Gen (NonceF (test $ ny))⟩ ∈ chan s"
with Hi HA obtain Ra where HRa:
"guessed_runs Ra = ⦇role=Init, owner=A, partner=B⦈"
"in_progressS (progress s Ra) {xnx, xgnx, xgny, xsk, xEnd}"
"gnx = Exp Gen (NonceF (Ra$nx))"
"guessed_frame Ra xgny = Some (Exp Gen (NonceF (test$ny)))"
by (auto dest!: l2_inv3D)
with Hi
have "guessed_frame Ra xsk = Some (Exp (Exp Gen (NonceF (Ra$nx))) (NonceF (test$ny)))"
by (auto dest: l2_inv4D)
with HRa Htest Htest' have "Ra ∈ partners"
by (auto simp add: partners_def partner_runs_def 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"
by auto
qed (auto simp add: can_signal_def)
qed
lemma l2_inv8_trans [iff]:
"{l2_inv8 ∩ l2_inv1 ∩ l2_inv2 ∩ l2_inv3 ∩ l2_inv4 ∩ l2_inv4'} trans l2 {> l2_inv8}"
apply (auto simp add: l2_nostep_defs intro!: l2_inv8_step3 l2_inv8_step4)
apply (auto simp add: PO_hoare_defs intro!: l2_inv8I)
apply (auto simp add: l2_defs dy_fake_chan_def dest: l2_inv8D)
done
lemma PO_l2_inv8 [iff]: "reach l2 ⊆ l2_inv8"
by (rule_tac J="l2_inv1 ∩ l2_inv2 ∩ l2_inv3 ∩ l2_inv4 ∩ l2_inv4'" in inv_rule_incr) (auto)
text ‹Auxiliary destruction rule for inv8.›
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_inv8_aux:
"s ∈ l2_inv8 ⟹
x ∈ secret s ⟹
x ∉ synth (analz generators)"
apply (auto simp add: analz_generators dest!: l2_inv8D [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 ⇒ l1_obs"
where
"med12s t ≡ ⦇
ik = ik t,
secret = secret t,
progress = progress t,
signalsInit = signalsInit t,
signalsResp = signalsResp 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} l1_step2 Rb A B gnx, l2_step2 Rb A B gnx {>R12s}"
by (auto simp add: PO_rhoare_defs R12s_defs l1_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_inv2 ∩ l2_inv4' ∩ l2_inv7 ∩ l2_inv8)}
l1_step3 Ra A B gny, l2_step3 Ra A B gny
{>R12s}"
proof (auto simp add: PO_rhoare_defs R12s_defs)
fix s s'
assume Hi:"s ∈ l2_inv1" "s ∈ l2_inv2" "s ∈ l2_inv4'" "s ∈ l2_inv7"
assume Ht: "(s, s') ∈ l2_step3 Ra A B gny"
assume "s ∈ l2_inv8"
with Hi Ht l2_inv8_step3 have Hi':"s' ∈ l2_inv8"
by (auto simp add: PO_hoare_defs, 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)"
by (auto dest: l2_inv8_aux)
with Hi have G2:"Ra = test ⟶ Exp gny (NonceF (Ra$nx)) ∉ synth (analz (ik s))"
by (auto dest!: l2_inv7D_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, xgnx, xgny, xsk} ∧
gny = Exp Gen (NonceF (Rb$ny)) ∧
guessed_frame Rb xgnx = Some (Exp Gen (NonceF (Ra$nx))))"
by (auto dest!: l2_inv2D [rotated 2] simp add: l2_defs)
with Ht G1 G2 show
"(⦇ ik = ik s, secret = secret s, progress = progress s,
signalsInit = signalsInit s, signalsResp = signalsResp s ⦈,
⦇ ik = ik s', secret = secret s', progress = progress s',
signalsInit = signalsInit s', signalsResp = signalsResp s' ⦈)
∈ l1_step3 Ra A B gny"
apply (auto simp add: l2_step3_def, auto simp add: l1_step3_def)
apply (auto simp add: can_signal_def)
done
qed
lemma l2_step4_refines_step4:
"{R12s ∩ UNIV × (l2_inv1 ∩ l2_inv3 ∩ l2_inv4 ∩ l2_inv4' ∩ l2_inv7 ∩ l2_inv8)}
l1_step4 Rb A B gnx, l2_step4 Rb A B gnx
{>R12s}"
proof (auto simp add: PO_rhoare_defs R12s_defs)
fix s s'
assume Hi:"s ∈ l2_inv1" "s ∈ l2_inv3" "s ∈ l2_inv4" "s ∈ l2_inv4'" "s ∈ l2_inv7"
assume Ht: "(s, s') ∈ l2_step4 Rb A B gnx"
assume "s ∈ l2_inv8"
with Hi Ht l2_inv8_step4 have Hi':"s' ∈ l2_inv8"
by (auto simp add: PO_hoare_defs, 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)"
by (auto dest: l2_inv8_aux)
with Hi have G2:"Rb = test ⟶ Exp gnx (NonceF (Rb$ny)) ∉ synth (analz (ik s))"
by (auto dest!: l2_inv7D_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, xgnx, xgny, xsk, xEnd} ∧
guessed_frame Ra xgnx = Some gnx ∧
guessed_frame Ra xgny = Some (Exp Gen (NonceF (Rb$ny))))"
by (auto dest!: l2_inv3D [rotated 2] simp add: l2_defs)
with Ht G1 G2 show
"(⦇ ik = ik s, secret = secret s, progress = progress s,
signalsInit = signalsInit s, signalsResp = signalsResp s ⦈,
⦇ ik = ik s', secret = secret s', progress = progress s',
signalsInit = signalsInit s', signalsResp = signalsResp s' ⦈)
∈ l1_step4 Rb A B gnx"
apply (auto simp add: l2_step4_def, auto simp add: l1_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_inv7 ∩ 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 dest!: l2_inv8_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_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" "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_inv8"
then obtain R R' N N' where Hx':"x = Exp (Exp Gen (NonceF (R$N))) (NonceF (R'$N'))"
"R = test ∧ R' ∈ partners"
by (auto dest!: l2_inv8D subsetD)
from H have "s ⦇ik := insert K (ik s)⦈ ∈ l2_inv7"
by (auto intro: hoare_apply [OF l2_inv7_skr] simp add: l2_defs)
with Hx have "x ∈ synth (analz (generators))"
by (auto dest: l2_inv7D_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 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_inv4 ∩ l2_inv4' ∩
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_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_Init ≡ l1_iagreement_Init"
lemma l2_obs_iagreement_Init [iff]: "oreach l2 ⊆ l2_iagreement_Init"
apply (rule external_invariant_translation
[OF l1_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 l1_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