Theory m1_keydist_iirn
section ‹Abstract (i/n)-authenticated key transport (L1)›
theory m1_keydist_iirn imports m1_keydist "../Refinement/a0i_agree"
begin
text ‹We add authentication for the initiator and responder to the basic
server-based key transport protocol:
\begin{enumerate}
\item the initiator injectively agrees with the server on the key and some
additional data
\item the responder non-injectively agrees with the server on the key and
some additional data.
\end{enumerate}
The "additional data" is a parameter of this model.›
declare option.split [split]
consts
na :: "nat"
subsection ‹State›
text ‹The state type remains the same, but in this model we will record
nonces and timestamps in the run frame.›
type_synonym m1a_state = "m1x_state"
type_synonym m1a_obs = "m1x_obs"
type_synonym 'x m1a_pred = "'x m1x_pred"
type_synonym 'x m1a_trans = "'x m1x_trans"
text ‹We need some parameters regarding the list of freshness values
stored by the server. These should be defined in further refinements.›
consts
is_len :: "nat"
rs_len :: "nat"
subsection ‹Events›
definition
m1a_step1 :: "[rid_t, agent, agent, nonce] ⇒ 'x m1r_trans"
where
"m1a_step1 Ra A B Na ≡ {(s, s1).
Ra ∉ dom (runs s) ∧
Na = Ra$na ∧
s1 = s⦇ runs := (runs s)(Ra ↦ (Init, [A, B], [])) ⦈
}"
definition
m1a_step2 :: "[rid_t, agent, agent] ⇒ 'x m1r_trans"
where
"m1a_step2 ≡ m1x_step2"
definition
m1a_step3 :: "[rid_t, agent, agent, key, nonce, atom list] ⇒ 'x m1r_trans"
where
"m1a_step3 Rs A B Kab Na al ≡ {(s, s1).
Rs ∉ dom (runs s) ∧
Kab = sesK (Rs$sk) ∧
s1 = s⦇ runs := (runs s)(Rs ↦ (Serv, [A, B], aNon Na # al)) ⦈
}"
definition
m1a_step4 :: "[rid_t, agent, agent, nonce, key, atom list] ⇒ 'x m1a_trans"
where
"m1a_step4 Ra A B Na Kab nla ≡ {(s, s').
runs s Ra = Some (Init, [A, B], []) ∧
(Kab ∉ leak s ⟶ (Kab, A) ∈ azC (runs s)) ∧
Na = Ra$na ∧
(A ∉ bad ⟶ (∃Rs. Kab = sesK (Rs$sk) ∧
runs s Rs = Some (Serv, [A, B], aNon Na # take is_len nla))) ∧
s' = s⦇ runs := (runs s)(Ra ↦ (Init, [A, B], aKey Kab # nla)) ⦈
}"
definition
m1a_step5 :: "[rid_t, agent, agent, key, atom list] ⇒ 'x m1a_trans"
where
"m1a_step5 Rb A B Kab nlb ≡ {(s, s1).
runs s Rb = Some (Resp, [A, B], []) ∧
(Kab ∉ leak s ⟶ (Kab, B) ∈ azC (runs s)) ∧
(B ∉ bad ⟶ (∃Rs Na. Kab = sesK (Rs$sk) ∧
runs s Rs = Some (Serv, [A, B], aNon Na # take rs_len nlb))) ∧
s1 = s⦇ runs := (runs s)(Rb ↦ (Resp, [A, B], aKey Kab # nlb)) ⦈
}"
definition
m1a_leak :: "rid_t ⇒ 'x m1x_trans"
where
"m1a_leak = m1x_leak"
subsection ‹Specification›
definition
m1a_init :: "m1a_state set"
where
"m1a_init ≡ m1x_init"
definition
m1a_trans :: "'x m1a_trans" where
"m1a_trans ≡ (⋃A B Ra Rb Rs Na Kab nls nla nlb.
m1a_step1 Ra A B Na ∪
m1a_step2 Rb A B ∪
m1a_step3 Rs A B Kab Na nls ∪
m1a_step4 Ra A B Na Kab nla ∪
m1a_step5 Rb A B Kab nlb ∪
m1a_leak Rs ∪
Id
)"
definition
m1a :: "(m1a_state, m1a_obs) spec" where
"m1a ≡ ⦇
init = m1a_init,
trans = m1a_trans,
obs = id
⦈"
lemma init_m1a: "init m1a = m1a_init"
by (simp add: m1a_def)
lemma trans_m1a: "trans m1a = m1a_trans"
by (simp add: m1a_def)
lemma obs_m1a [simp]: "obs m1a = id"
by (simp add: m1a_def)
lemmas m1a_loc_defs =
m1a_def m1a_init_def m1a_trans_def
m1a_step1_def m1a_step2_def m1a_step3_def m1a_step4_def m1a_step5_def
m1a_leak_def
lemmas m1a_defs = m1a_loc_defs m1x_defs
subsection ‹Invariants›
subsubsection ‹inv0: Finite domain›
text ‹There are only finitely many runs. This is needed to establish
the responder/initiator agreement.›
definition
m1a_inv0_fin :: "'x m1r_pred"
where
"m1a_inv0_fin ≡ {s. finite (dom (runs s))}"
lemmas m1a_inv0_finI = m1a_inv0_fin_def [THEN setc_def_to_intro, rule_format]
lemmas m1a_inv0_finE [elim] = m1a_inv0_fin_def [THEN setc_def_to_elim, rule_format]
lemmas m1a_inv0_finD = m1a_inv0_fin_def [THEN setc_def_to_dest, rule_format]
text ‹Invariance proof.›
lemma PO_m1a_inv0_fin_init [iff]:
"init m1a ⊆ m1a_inv0_fin"
by (auto simp add: m1a_defs intro!: m1a_inv0_finI)
lemma PO_m1a_inv0_fin_trans [iff]:
"{m1a_inv0_fin} trans m1a {> m1a_inv0_fin}"
by (auto simp add: PO_hoare_defs m1a_defs intro!: m1a_inv0_finI)
lemma PO_m1a_inv0_fin [iff]: "reach m1a ⊆ m1a_inv0_fin"
by (rule inv_rule_incr, auto del: subsetI)
subsection ‹Refinement of ‹m1x››
subsubsection ‹Simulation relation›
text ‹Define run abstraction.›
fun
rm1x1a :: "role_t ⇒ atom list ⇒ atom list"
where
"rm1x1a Init = take 1"
| "rm1x1a Resp = take 1"
| "rm1x1a Serv = take 0"
abbreviation
runs1x1a :: "runs_t ⇒ runs_t" where
"runs1x1a ≡ map_runs rm1x1a"
text ‹med1x1: The mediator function maps a concrete observation to an
abstract one.›
definition
med1x1a :: "m1a_obs ⇒ m1x_obs" where
"med1x1a t ≡ ⦇ runs = runs1x1a (runs t), leak = leak t ⦈"
text ‹R1x1a: The simulation relation is defined in terms of the mediator
function.›
definition
R1x1a :: "(m1x_state × m1a_state) set" where
"R1x1a ≡ {(s, t). s = med1x1a t}"
lemmas R1x1a_defs =
R1x1a_def med1x1a_def
subsubsection ‹Refinement proof›
lemma PO_m1a_step1_refines_m1x_step1:
"{R1x1a}
(m1x_step1 Ra A B), (m1a_step1 Ra A B Na)
{> R1x1a}"
by (auto simp add: PO_rhoare_defs R1x1a_defs m1a_defs)
lemma PO_m1a_step2_refines_m1x_step2:
"{R1x1a}
(m1x_step2 Rb A B), (m1a_step2 Rb A B)
{> R1x1a}"
by (auto simp add: PO_rhoare_defs R1x1a_defs m1a_defs)
lemma PO_m1a_step3_refines_m1x_step3:
"{R1x1a}
(m1x_step3 Rs A B Kab), (m1a_step3 Rs A B Kab Na nls)
{> R1x1a}"
by (auto simp add: PO_rhoare_defs R1x1a_defs m1a_defs)
lemma PO_m1a_step4_refines_m1x_step4:
"{R1x1a}
(m1x_step4 Ra A B Kab), (m1a_step4 Ra A B Na Kab nla)
{> R1x1a}"
by (auto simp add: PO_rhoare_defs R1x1a_defs m1a_defs map_runs_def)
lemma PO_m1a_step5_refines_m1x_step5:
"{R1x1a}
(m1x_step5 A B Rb Kab), (m1a_step5 A B Rb Kab nlb)
{> R1x1a}"
by (auto simp add: PO_rhoare_defs R1x1a_defs m1a_defs map_runs_def)
lemma PO_m1a_leak_refines_m1x_leak:
"{R1x1a}
(m1x_leak Rs), (m1a_leak Rs)
{> R1x1a}"
by (auto simp add: PO_rhoare_defs R1x1a_defs m1a_defs map_runs_def)
text ‹All together now...›
lemmas PO_m1a_trans_refines_m1x_trans =
PO_m1a_step1_refines_m1x_step1 PO_m1a_step2_refines_m1x_step2
PO_m1a_step3_refines_m1x_step3 PO_m1a_step4_refines_m1x_step4
PO_m1a_step5_refines_m1x_step5 PO_m1a_leak_refines_m1x_leak
lemma PO_m1a_refines_init_m1x [iff]:
"init m1a ⊆ R1x1a``(init m1x)"
by (auto simp add: R1x1a_defs m1a_defs)
lemma PO_m1a_refines_trans_m1x [iff]:
"{R1x1a}
(trans m1x), (trans m1a)
{> R1x1a}"
apply (auto simp add: m1a_def m1a_trans_def m1x_def m1x_trans_def
intro!: PO_m1a_trans_refines_m1x_trans)
apply (force intro!: PO_m1a_trans_refines_m1x_trans)+
done
text ‹Observation consistency.›
lemma obs_consistent_med1x1a [iff]:
"obs_consistent R1x1a med1x1a m1x m1a"
by (auto simp add: obs_consistent_def R1x1a_def m1a_defs)
text ‹Refinement result.›
lemma PO_m1a_refines_m1x [iff]:
"refines R1x1a med1x1a m1x m1a"
by (rule Refinement_basic) (auto del: subsetI)
lemma m1a_implements_m1x [iff]: "implements med1x1a m1x m1a"
by (rule refinement_soundness) (fast)
text ‹By transitivity:›
lemma m1a_implements_s0g [iff]: "implements (med01x o med1x1a) s0g m1a"
by (rule implements_trans, auto)
subsubsection ‹inv (inherited): Secrecy›
text ‹Secrecy preserved from ‹m1x›.›
lemma knC_runs1x1a [simp]: "knC (runs1x1a runz) = knC runz"
apply (auto simp add: map_runs_def elim!: knC.cases, auto)
apply (rename_tac b, case_tac b, auto)
apply (rename_tac b, case_tac b, auto)
apply (rule knC_init, auto simp add: map_runs_def)
apply (rule knC_resp, auto simp add: map_runs_def)
apply (rule knC_serv, auto simp add: map_runs_def)
done
lemma PO_m1a_obs_secrecy [iff]: "oreach m1a ⊆ m1x_secrecy"
apply (rule_tac Q=m1x_secrecy in external_invariant_translation)
apply (auto del: subsetI)
apply (auto simp add: med1x1a_def m1x_secrecy_def)
done
lemma PO_m1a_secrecy [iff]: "reach m1a ⊆ m1x_secrecy"
by (rule external_to_internal_invariant) (auto del: subsetI)
subsection ‹Refinement of ‹a0i› for initiator/server›
text ‹For the initiator, we get an injective agreement with the server on
the session key, the responder name, the initiator's nonce and the list of
freshness values @{term "isl"}.›
subsubsection ‹Simulation relation›
text ‹We define two auxiliary functions to reconstruct the signals of the
initial model from completed initiator and server runs.›
type_synonym
issig = "key × agent × nonce × atom list"
fun
is_runs2sigs :: "runs_t ⇒ issig signal ⇒ nat"
where
"is_runs2sigs runz (Running [A, Sv] (Kab, B, Na, nl)) =
(if ∃Rs. Kab = sesK (Rs$sk) ∧
runz Rs = Some (Serv, [A, B], aNon Na # nl)
then 1 else 0)"
| "is_runs2sigs runz (Commit [A, Sv] (Kab, B, Na, nl)) =
(if ∃Ra nla. Na = Ra$na ∧
runz Ra = Some (Init, [A, B], aKey Kab # nla) ∧
take is_len nla = nl
then 1 else 0)"
| "is_runs2sigs runz _ = 0"
text ‹Simulation relation and mediator function. We map completed initiator
and responder runs to commit and running signals, respectively.›
definition
med_a0m1a_is :: "m1a_obs ⇒ issig a0i_obs" where
"med_a0m1a_is o1 ≡ ⦇ signals = is_runs2sigs (runs o1), corrupted = {} ⦈"
definition
R_a0m1a_is :: "(issig a0i_state × m1a_state) set" where
"R_a0m1a_is ≡ {(s, t). signals s = is_runs2sigs (runs t) ∧ corrupted s = {} }"
lemmas R_a0m1a_is_defs = R_a0m1a_is_def med_a0m1a_is_def
subsubsection ‹Lemmas about the auxiliary functions›
lemma is_runs2sigs_empty [simp]:
"runz = Map.empty ⟹ is_runs2sigs runz = (λs. 0)"
by (rule ext, erule rev_mp)
(rule is_runs2sigs.induct, auto)
text ‹Update lemmas›
lemma is_runs2sigs_upd_init_none [simp]:
"⟦ Ra ∉ dom runz ⟧
⟹ is_runs2sigs (runz(Ra ↦ (Init, [A, B], []))) = is_runs2sigs runz"
by (rule ext, erule rev_mp)
(rule is_runs2sigs.induct, auto dest: dom_lemmas)
lemma is_runs2sigs_upd_resp_none [simp]:
"⟦ Rb ∉ dom runz ⟧
⟹ is_runs2sigs (runz(Rb ↦ (Resp, [A, B], []))) = is_runs2sigs runz"
by (rule ext, erule rev_mp)
(rule is_runs2sigs.induct, auto dest: dom_lemmas)
lemma is_runs2sigs_upd_serv [simp]:
"⟦ Rs ∉ dom runz ⟧
⟹ is_runs2sigs (runz(Rs ↦ (Serv, [A, B], aNon Na # ils))) =
(is_runs2sigs runz)(Running [A, Sv] (sesK (Rs$sk), B, Na, ils) := 1)"
apply (rule ext, (erule rev_mp)+)
apply (rule is_runs2sigs.induct)
apply (safe, simp_all)+
apply (fastforce simp add: domIff)+
done
lemma is_runs2sigs_upd_init_some [simp]:
"⟦ runz Ra = Some (Init, [A, B], []); ils = take is_len nla ⟧
⟹ is_runs2sigs (runz(Ra ↦ (Init, [A, B], aKey Kab # nla))) =
(is_runs2sigs runz)(Commit [A, Sv] (Kab, B, Ra$na, ils) := 1)"
apply (rule ext, (erule rev_mp)+)
apply (rule is_runs2sigs.induct)
apply (safe, simp_all)+
apply (fastforce)+
done
lemma is_runs2sigs_upd_resp_some [simp]:
"⟦ runz Rb = Some (Resp, [A, B], []) ⟧
⟹ is_runs2sigs (runz(Rb ↦ (Resp, [A, B], aKey Kab # nlb))) =
is_runs2sigs runz"
apply (rule ext, erule rev_mp)
apply (rule is_runs2sigs.induct, auto)
done
subsubsection ‹Refinement proof›
lemma PO_m1a_step1_refines_a0_is_skip:
"{R_a0m1a_is}
Id, (m1a_step1 Ra A B Na)
{> R_a0m1a_is}"
by (auto simp add: PO_rhoare_defs R_a0m1a_is_defs m1a_defs)
lemma PO_m1a_step2_refines_a0_is_skip:
"{R_a0m1a_is}
Id, (m1a_step2 Rb A B)
{> R_a0m1a_is}"
by (auto simp add: PO_rhoare_defs R_a0m1a_is_defs m1a_defs)
lemma PO_m1a_step3_refines_a0_is_running:
"{R_a0m1a_is}
(a0i_running [A, Sv] (Kab, B, Na, nls)),
(m1a_step3 Rs A B Kab Na nls)
{> R_a0m1a_is}"
by (auto simp add: PO_rhoare_defs R_a0m1a_is_defs a0i_defs m1a_defs
dest: dom_lemmas)
lemma PO_m1a_step4_refines_a0_is_commit:
"{R_a0m1a_is ∩ UNIV × m1a_inv0_fin}
(a0i_commit [A, Sv] (Kab, B, Na, take is_len nla)),
(m1a_step4 Ra A B Na Kab nla)
{> R_a0m1a_is}"
by (auto simp add: PO_rhoare_defs R_a0m1a_is_defs a0i_defs m1a_defs)
lemma PO_m1a_step5_refines_a0_is_skip:
"{R_a0m1a_is}
Id, (m1a_step5 A B Rb Kab nlb)
{> R_a0m1a_is}"
by (auto simp add: PO_rhoare_defs R_a0m1a_is_defs m1a_defs)
lemma PO_m1a_leak_refines_a0_is_skip:
"{R_a0m1a_is}
Id, (m1a_leak Rs)
{> R_a0m1a_is}"
by (auto simp add: PO_rhoare_defs R_a0m1a_is_defs m1a_defs)
text ‹All together now...›
lemmas PO_m1a_trans_refines_a0_is_trans =
PO_m1a_step1_refines_a0_is_skip PO_m1a_step2_refines_a0_is_skip
PO_m1a_step3_refines_a0_is_running PO_m1a_step4_refines_a0_is_commit
PO_m1a_step5_refines_a0_is_skip PO_m1a_leak_refines_a0_is_skip
lemma PO_m1a_refines_init_a0_is [iff]:
"init m1a ⊆ R_a0m1a_is``(init a0i)"
by (auto simp add: R_a0m1a_is_defs a0i_defs m1a_defs)
lemma PO_m1a_refines_trans_a0_is [iff]:
"{R_a0m1a_is ∩ a0i_inv1_iagree × m1a_inv0_fin}
(trans a0i), (trans m1a)
{> R_a0m1a_is}"
by (force simp add: m1a_def m1a_trans_def a0i_def a0i_trans_def
intro!: PO_m1a_trans_refines_a0_is_trans)
lemma obs_consistent_med_a0m1a_is [iff]:
"obs_consistent R_a0m1a_is med_a0m1a_is a0i m1a"
by (auto simp add: obs_consistent_def R_a0m1a_is_def med_a0m1a_is_def
a0i_def m1a_def)
text ‹Refinement result.›
lemma PO_m1a_refines_a0_is [iff]:
"refines (R_a0m1a_is ∩ a0i_inv1_iagree × m1a_inv0_fin) med_a0m1a_is a0i m1a"
by (rule Refinement_using_invariants)
(auto del: subsetI)
lemma m1a_implements_a0_is: "implements med_a0m1a_is a0i m1a"
by (rule refinement_soundness) (fast)
subsubsection ‹inv2i (inherited): Initiator and server›
text ‹This is a translation of the agreement property to Level 1. It
follows from the refinement and is needed to prove inv1.›
definition
m1a_inv2i_serv :: "'x m1x_state_scheme set"
where
"m1a_inv2i_serv ≡ {s. ∀A B Ra Kab nla.
A ∉ bad ⟶
runs s Ra = Some (Init, [A, B], aKey Kab # nla) ⟶
(∃Rs. Kab = sesK (Rs$sk) ∧
runs s Rs = Some (Serv, [A, B], aNon (Ra$na) # take is_len nla))
}"
lemmas m1a_inv2i_servI =
m1a_inv2i_serv_def [THEN setc_def_to_intro, rule_format]
lemmas m1a_inv2i_servE =
m1a_inv2i_serv_def [THEN setc_def_to_elim, rule_format]
lemmas m1a_inv2i_servD =
m1a_inv2i_serv_def [THEN setc_def_to_dest, rule_format, rotated -1]
text ‹Invariance proof, see below after init/serv authentication proof.›
lemma PO_m1a_inv2i_serv [iff]:
"reach m1a ⊆ m1a_inv2i_serv"
apply (rule INV_from_Refinement_basic [OF PO_m1a_refines_a0_is])
apply (auto simp add: R_a0m1a_is_def a0i_inv1_iagree_def
intro!: m1a_inv2i_servI)
apply (drule_tac x="[A, Sv]" in spec, force)
done
subsubsection ‹inv1: Key freshness for initiator›
text ‹The initiator obtains key freshness from the injective agreement
with the server AND the fact that there is only one server run with a
given key.›
definition
m1a_inv1_ifresh :: "'x m1a_pred"
where
"m1a_inv1_ifresh ≡ {s. ∀A A' B B' Ra Ra' Kab nl nl'.
runs s Ra = Some (Init, [A, B], aKey Kab # nl) ⟶
runs s Ra' = Some (Init, [A', B'], aKey Kab # nl') ⟶
A ∉ bad ⟶ B ∉ bad ⟶ Kab ∉ leak s ⟶
Ra = Ra'
}"
lemmas m1a_inv1_ifreshI = m1a_inv1_ifresh_def [THEN setc_def_to_intro, rule_format]
lemmas m1a_inv1_ifreshE [elim] = m1a_inv1_ifresh_def [THEN setc_def_to_elim, rule_format]
lemmas m1a_inv1_ifreshD = m1a_inv1_ifresh_def [THEN setc_def_to_dest, rule_format, rotated 1]
text ‹Invariance proof›
lemma PO_m1a_inv1_ifresh_init [iff]:
"init m1a ⊆ m1a_inv1_ifresh"
by (auto simp add: m1a_defs intro!: m1a_inv1_ifreshI)
lemma PO_m1a_inv1_ifresh_step4:
"{m1a_inv1_ifresh ∩ m1a_inv2i_serv ∩ m1x_secrecy}
m1a_step4 Ra A B Na Kab nla
{> m1a_inv1_ifresh}"
proof (auto simp add: PO_hoare_defs m1a_defs intro!: m1a_inv1_ifreshI,
auto dest: m1a_inv1_ifreshD, auto dest: m1a_inv2i_servD)
fix Rs Ra' A' B' nl' s
assume H:
"(sesK (Rs $ sk), A) ∈ azC (runs s)" "sesK (Rs $ sk) ∉ leak s"
"A ∉ bad" "B ∉ bad" "Ra' ≠ Ra"
"runs s Ra = Some (Init, [A, B], [])"
"runs s Rs = Some (Serv, [A, B], aNon (Ra $ na) # take is_len nla)"
"runs s Ra' = Some (Init, [A', B'], aKey (sesK (Rs $ sk)) # nl')"
"s ∈ m1x_secrecy" "s ∈ m1a_inv2i_serv"
thus False
proof (cases "A' ∈ bad")
case True
from H have "(sesK (Rs$sk), A') ∈ azC (runs s)" by (elim m1x_secrecyE, auto)
with H True show ?thesis by (elim azC.cases) (auto dest: m1a_inv2i_servD)
next
case False thus ?thesis using H by (auto dest: m1a_inv2i_servD)
qed
next
fix A' B' Ra' nl s
assume
"(Kab, A) ∈ azC (runs s)" "Kab ∉ leak s"
"A' ∉ bad" "B' ∉ bad" "A ∈ bad" "Ra' ≠ Ra"
"runs s Ra' = Some (Init, [A', B'], aKey Kab # nl)"
"runs s Ra = Some (Init, [A, B], [])"
"s ∈ m1a_inv2i_serv"
thus False
by (elim azC.cases, auto dest: m1a_inv2i_servD)
qed
lemma PO_m1a_inv1_ifresh_trans [iff]:
"{m1a_inv1_ifresh ∩ m1a_inv2i_serv ∩ m1x_secrecy} trans m1a {> m1a_inv1_ifresh}"
proof (simp add: m1a_def m1a_trans_def, safe)
fix Ra A B Kab Ts nla
show
"{m1a_inv1_ifresh ∩ m1a_inv2i_serv ∩ m1x_secrecy}
m1a_step4 Ra A B Kab Ts nla
{> m1a_inv1_ifresh}"
by (rule PO_m1a_inv1_ifresh_step4)
qed (auto simp add: PO_hoare_defs m1a_defs intro!: m1a_inv1_ifreshI)
lemma PO_m1a_inv1_ifresh [iff]: "reach m1a ⊆ m1a_inv1_ifresh"
by (rule_tac J=" m1a_inv2i_serv ∩ m1x_secrecy" in inv_rule_incr)
(auto simp add: Int_assoc del: subsetI)
subsection ‹Refinement of ‹a0n› for responder/server›
text ‹For the responder, we get a non-injective agreement with the server on
the session key, the initiator's name, and additional data.›
subsubsection ‹Simulation relation›
text ‹We define two auxiliary functions to reconstruct the signals of the
initial model from completed responder and server runs.›
type_synonym
= "key × agent × atom list"
abbreviation
rs_commit :: "[runs_t, agent, agent, key, atom list] ⇒ rid_t set"
where
"rs_commit runz A B Kab rsl ≡ {Rb. ∃nlb.
runz Rb = Some (Resp, [A, B], aKey Kab # nlb) ∧ take rs_len nlb = rsl
}"
fun
rs_runs2sigs :: "runs_t ⇒ rssig signal ⇒ nat"
where
"rs_runs2sigs runz (Running [B, Sv] (Kab, A, rsl)) =
(if (∃Rs Na. Kab = sesK (Rs$sk) ∧
runz Rs = Some (Serv, [A, B], aNon Na # rsl))
then 1 else 0)"
| "rs_runs2sigs runz (Commit [B, Sv] (Kab, A, rsl)) =
card (rs_commit runz A B Kab rsl)"
| "rs_runs2sigs runz _ = 0"
text ‹Simulation relation and mediator function. We map completed initiator
and responder runs to commit and running signals, respectively.›
definition
med_a0m1a_rs :: "m1a_obs ⇒ rssig a0n_obs" where
"med_a0m1a_rs o1 ≡ ⦇ signals = rs_runs2sigs (runs o1), corrupted = {} ⦈"
definition
R_a0m1a_rs :: "(rssig a0n_state × m1a_state) set" where
"R_a0m1a_rs ≡ {(s, t). signals s = rs_runs2sigs (runs t) ∧ corrupted s = {} }"
lemmas R_a0m1a_rs_defs = R_a0m1a_rs_def med_a0m1a_rs_def
subsubsection ‹Lemmas about the auxiliary functions›
text ‹Other lemmas›
lemma rs_runs2sigs_empty [simp]:
"runz = Map.empty ⟹ rs_runs2sigs runz = (λs. 0)"
by (rule ext, erule rev_mp)
(rule rs_runs2sigs.induct, auto)
lemma rs_commit_finite [simp, intro]:
"finite (dom runz) ⟹ finite (rs_commit runz A B Kab nls)"
by (auto intro: finite_subset dest: dom_lemmas)
text ‹Update lemmas›
lemma rs_runs2sigs_upd_init_none [simp]:
"⟦ Ra ∉ dom runz ⟧
⟹ rs_runs2sigs (runz(Ra ↦ (Init, [A, B], []))) = rs_runs2sigs runz"
by (rule ext, erule rev_mp)
(rule rs_runs2sigs.induct, auto dest: dom_lemmas)
lemma rs_runs2sigs_upd_resp_none [simp]:
"⟦ Rb ∉ dom runz ⟧
⟹ rs_runs2sigs (runz(Rb ↦ (Resp, [A, B], []))) = rs_runs2sigs runz"
by (rule ext, erule rev_mp)
(rule rs_runs2sigs.induct, auto dest: dom_lemmas)
lemma rs_runs2sigs_upd_serv [simp]:
"⟦ Rs ∉ dom runz ⟧
⟹ rs_runs2sigs (runz(Rs ↦ (Serv, [A, B], aNon Na # nls))) =
(rs_runs2sigs runz)(Running [B, Sv] (sesK (Rs$sk), A, nls) := 1)"
by (rule ext, erule rev_mp)
(rule rs_runs2sigs.induct, auto dest: dom_lemmas)
lemma rs_runs2sigs_upd_init_some [simp]:
"⟦ runz Ra = Some (Init, [A, B], []) ⟧
⟹ rs_runs2sigs (runz(Ra ↦ (Init, [A, B], aKey Kab # nl))) =
rs_runs2sigs runz"
by (rule ext, erule rev_mp)
(rule rs_runs2sigs.induct, auto dest: dom_lemmas)
lemma rs_runs2sigs_upd_resp_some [simp]:
"⟦ runz Rb = Some (Resp, [A, B], []); finite (dom runz);
rsl = take rs_len nlb ⟧
⟹ rs_runs2sigs (runz(Rb ↦ (Resp, [A, B], aKey Kab # nlb))) =
(rs_runs2sigs runz)(
Commit [B, Sv] (Kab, A, rsl) := Suc (card (rs_commit runz A B Kab rsl)))"
apply (rule ext, (erule rev_mp)+)
apply (rule rs_runs2sigs.induct, auto dest: dom_lemmas)
apply (rule_tac s="card (insert Rb (rs_commit runz A B Kab (take rs_len nlb)))"
in trans, fast, auto)
done
subsubsection ‹Refinement proof›
lemma PO_m1a_step1_refines_a0_rs_skip:
"{R_a0m1a_rs}
Id, (m1a_step1 Ra A B Na)
{> R_a0m1a_rs}"
by (auto simp add: PO_rhoare_defs R_a0m1a_rs_defs m1a_defs)
lemma PO_m1a_step2_refines_a0_rs_skip:
"{R_a0m1a_rs}
Id, (m1a_step2 Rb A B)
{> R_a0m1a_rs}"
by (auto simp add: PO_rhoare_defs R_a0m1a_rs_defs m1a_defs)
lemma PO_m1a_step3_refines_a0_rs_running:
"{R_a0m1a_rs}
(a0n_running [B, Sv] (Kab, A, nls)),
(m1a_step3 Rs A B Kab Na nls)
{> R_a0m1a_rs}"
by (auto simp add: PO_rhoare_defs R_a0m1a_rs_defs a0i_defs m1a_defs
dest: dom_lemmas)
lemma PO_m1a_step4_refines_a0_rs_skip:
"{R_a0m1a_rs}
Id, (m1a_step4 Ra A B Na Kab nla)
{> R_a0m1a_rs}"
by (auto simp add: PO_rhoare_defs R_a0m1a_rs_defs a0i_defs m1a_defs)
lemma PO_m1a_step5_refines_a0_rs_commit:
"{R_a0m1a_rs ∩ UNIV × m1a_inv0_fin}
(a0n_commit [B, Sv] (Kab, A, take rs_len nlb)),
(m1a_step5 Rb A B Kab nlb)
{> R_a0m1a_rs}"
by (auto simp add: PO_rhoare_defs R_a0m1a_rs_defs a0i_defs m1a_defs)
lemma PO_m1a_leak_refines_a0_rs_skip:
"{R_a0m1a_rs}
Id, (m1a_leak Rs)
{> R_a0m1a_rs}"
by (auto simp add: PO_rhoare_defs R_a0m1a_rs_defs a0i_defs m1a_defs)
text ‹All together now...›
lemmas PO_m1a_trans_refines_a0_rs_trans =
PO_m1a_step1_refines_a0_rs_skip PO_m1a_step2_refines_a0_rs_skip
PO_m1a_step3_refines_a0_rs_running PO_m1a_step4_refines_a0_rs_skip
PO_m1a_step5_refines_a0_rs_commit PO_m1a_leak_refines_a0_rs_skip
lemma PO_m1a_refines_init_ra0n [iff]:
"init m1a ⊆ R_a0m1a_rs``(init a0n)"
by (auto simp add: R_a0m1a_rs_defs a0n_defs m1a_defs)
lemma PO_m1a_refines_trans_ra0n [iff]:
"{R_a0m1a_rs ∩ a0n_inv1_niagree × m1a_inv0_fin}
(trans a0n), (trans m1a)
{> R_a0m1a_rs}"
by (force simp add: m1a_def m1a_trans_def a0n_def a0n_trans_def
intro!: PO_m1a_trans_refines_a0_rs_trans)
lemma obs_consistent_med_a0m1a_rs [iff]:
"obs_consistent
(R_a0m1a_rs ∩ a0n_inv1_niagree × m1a_inv0_fin)
med_a0m1a_rs a0n m1a"
by (auto simp add: obs_consistent_def R_a0m1a_rs_def med_a0m1a_rs_def
a0n_def m1a_def)
text ‹Refinement result.›
lemma PO_m1a_refines_a0_rs [iff]:
"refines (R_a0m1a_rs ∩ a0n_inv1_niagree × m1a_inv0_fin) med_a0m1a_rs a0n m1a"
by (rule Refinement_using_invariants) (auto)
lemma m1a_implements_ra0n: "implements med_a0m1a_rs a0n m1a"
by (rule refinement_soundness) (fast)
subsubsection ‹inv2r (inherited): Responder and server›
text ‹This is a translation of the agreement property to Level 1. It
follows from the refinement and not needed here but later.›
definition
m1a_inv2r_serv :: "'x m1x_state_scheme set"
where
"m1a_inv2r_serv ≡ {s. ∀A B Rb Kab nlb.
B ∉ bad ⟶
runs s Rb = Some (Resp, [A, B], aKey Kab # nlb) ⟶
(∃Rs Na. Kab = sesK (Rs$sk) ∧
runs s Rs = Some (Serv, [A, B], aNon Na # take rs_len nlb))
}"
lemmas m1a_inv2r_servI =
m1a_inv2r_serv_def [THEN setc_def_to_intro, rule_format]
lemmas m1a_inv2r_servE [elim] =
m1a_inv2r_serv_def [THEN setc_def_to_elim, rule_format]
lemmas m1a_inv2r_servD =
m1a_inv2r_serv_def [THEN setc_def_to_dest, rule_format, rotated -1]
text ‹Invariance proof›
lemma PO_m1a_inv2r_serv [iff]:
"reach m1a ⊆ m1a_inv2r_serv"
apply (rule INV_from_Refinement_basic [OF PO_m1a_refines_a0_rs])
apply (auto simp add: R_a0m1a_rs_def a0n_inv1_niagree_def intro!: m1a_inv2r_servI)
apply (rename_tac x A B Rb Kab nlb a, drule_tac x="[B, Sv]" in spec, clarsimp)
apply (rename_tac x A B Rb Kab nlb a, drule_tac x="Kab" in spec, force)
done
end