Theory m1_ds
section ‹Abstract Denning-Sacco protocol (L1)›
theory m1_ds imports m1_keydist_inrn "../Refinement/a0n_agree"
begin
text ‹We augment the basic abstract key distribution model such that
the server sends a timestamp along with the session key. We check the
timestamp's validity to ensure recentness of the session key.
We establish one refinement for this model, namely that this model refines
the basic authenticated key transport model ‹m1_keydist_inrn›,
which guarantees non-injective agreement with the server on the session key
and the server-generated timestamp.
›
subsection ‹State›
text ‹We extend the basic key distribution by adding timestamps.
We add a clock variable modeling the current time. The frames, runs, and
observations remain the same as in the previous model, but we will use
the @{typ "nat list"}'s to store timestamps.
›
type_synonym
time = "nat"
consts
Ls :: "time"
text ‹State and observations›
record
m1_state = "m1x_state" +
clk :: "time"
type_synonym
m1_obs = "m1_state"
type_synonym
'x m1_pred = "'x m1_state_scheme set"
type_synonym
'x m1_trans = "('x m1_state_scheme × 'x m1_state_scheme) set"
text ‹Instantiate parameters regarding list of freshness identifiers stored
at server.›
overloading is_len' ≡ "is_len" rs_len' ≡ "rs_len" begin
definition is_len_def [simp]: "is_len' ≡ 1::nat"
definition rs_len_def [simp]: "rs_len' ≡ 1::nat"
end
subsection ‹Events›
definition
m1_step1 :: "[rid_t, agent, agent] ⇒ 'x m1_trans"
where
"m1_step1 ≡ m1a_step1"
definition
m1_step2 :: "[rid_t, agent, agent] ⇒ 'x m1_trans"
where
"m1_step2 ≡ m1a_step2"
definition
m1_step3 :: "[rid_t, agent, agent, key, time] ⇒ 'x m1_trans"
where
"m1_step3 Rs A B Kab Ts ≡ {(s, s').
Ts = clk s ∧
(s, s') ∈ m1a_step3 Rs A B Kab [aNum Ts]
}"
definition
m1_step4 :: "[rid_t, agent, agent, key, time] ⇒ 'x m1_trans"
where
"m1_step4 Ra A B Kab Ts ≡ {(s, s').
clk s < Ts + Ls ∧
(s, s') ∈ m1a_step4 Ra A B Kab [aNum Ts]
}"
definition
m1_step5 :: "[rid_t, agent, agent, key, time] ⇒ 'x m1_trans"
where
"m1_step5 Rb A B Kab Ts ≡ {(s, s').
clk s < Ts + Ls ∧
(s, s') ∈ m1a_step5 Rb A B Kab [aNum Ts]
}"
definition
m1_tick :: "time ⇒ 'x m1_trans"
where
"m1_tick T ≡ {(s, s').
s' = s⦇ clk := clk s + T ⦈
}"
definition
m1_leak :: "[rid_t] ⇒ 'x m1_trans"
where
"m1_leak ≡ m1a_leak"
subsection ‹Specification›
definition
m1_init :: "unit m1_pred"
where
"m1_init ≡ { ⦇ runs = Map.empty, leak = corrKey, clk = 0 ⦈ }"
definition
m1_trans :: "'x m1_trans" where
"m1_trans ≡ (⋃A B Ra Rb Rs Kab Ts T.
m1_step1 Ra A B ∪
m1_step2 Rb A B ∪
m1_step3 Rs A B Kab Ts ∪
m1_step4 Ra A B Kab Ts ∪
m1_step5 Rb A B Kab Ts ∪
m1_tick T ∪
m1_leak Rs ∪
Id
)"
definition
m1 :: "(m1_state, m1_obs) spec" where
"m1 ≡ ⦇
init = m1_init,
trans = m1_trans,
obs = id
⦈"
lemmas m1_loc_defs =
m1_def m1_init_def m1_trans_def
m1_step1_def m1_step2_def m1_step3_def m1_step4_def m1_step5_def
m1_leak_def m1_tick_def
lemmas m1_defs = m1_loc_defs m1a_defs
lemma m1_obs_id [simp]: "obs m1 = id"
by (simp add: m1_def)
subsection ‹Invariants›
subsubsection ‹inv0: Finite domain›
text ‹There are only finitely many runs. This is needed to establish
the responder/initiator agreement.›
definition
m1_inv0_fin :: "'x m1_pred"
where
"m1_inv0_fin ≡ {s. finite (dom (runs s))}"
lemmas m1_inv0_finI = m1_inv0_fin_def [THEN setc_def_to_intro, rule_format]
lemmas m1_inv0_finE [elim] = m1_inv0_fin_def [THEN setc_def_to_elim, rule_format]
lemmas m1_inv0_finD = m1_inv0_fin_def [THEN setc_def_to_dest, rule_format]
text ‹Invariance proofs.›
lemma PO_m1_inv0_fin_init [iff]:
"init m1 ⊆ m1_inv0_fin"
by (auto simp add: m1_defs intro!: m1_inv0_finI)
lemma PO_m1_inv0_fin_trans [iff]:
"{m1_inv0_fin} trans m1 {> m1_inv0_fin}"
by (auto simp add: PO_hoare_defs m1_defs intro!: m1_inv0_finI)
lemma PO_m1_inv0_fin [iff]: "reach m1 ⊆ m1_inv0_fin"
by (rule inv_rule_incr, auto del: subsetI)
subsection ‹Refinement of ‹m1a››
subsubsection ‹Simulation relation›
text ‹R1a1: The simulation relation and mediator function are identities.›
definition
med1a1 :: "m1_obs ⇒ m1a_obs" where
"med1a1 t ≡ ⦇ runs = runs t, leak = leak t ⦈"
definition
R1a1 :: "(m1a_state × m1_state) set" where
"R1a1 ≡ {(s, t). s = med1a1 t}"
lemmas R1a1_defs = R1a1_def med1a1_def
subsubsection ‹Refinement proof›
lemma PO_m1_step1_refines_m1a_step1:
"{R1a1}
(m1a_step1 Ra A B), (m1_step1 Ra A B)
{> R1a1}"
by (auto simp add: PO_rhoare_defs R1a1_defs m1_defs)
lemma PO_m1_step2_refines_m1a_step2:
"{R1a1}
(m1a_step2 Rb A B), (m1_step2 Rb A B)
{> R1a1}"
by (auto simp add: PO_rhoare_defs R1a1_defs m1_defs)
lemma PO_m1_step3_refines_m1a_step3:
"{R1a1}
(m1a_step3 Rs A B Kab [aNum Ts]), (m1_step3 Rs A B Kab Ts)
{> R1a1}"
by (auto simp add: PO_rhoare_defs R1a1_defs m1_defs)
lemma PO_m1_step4_refines_m1a_step4:
"{R1a1}
(m1a_step4 Ra A B Kab [aNum Ts]), (m1_step4 Ra A B Kab Ts)
{> R1a1}"
by (auto simp add: PO_rhoare_defs R1a1_defs m1_defs)
lemma PO_m1_step5_refines_m1a_step5:
"{R1a1}
(m1a_step5 Rb A B Kab [aNum Ts]), (m1_step5 Rb A B Kab Ts)
{> R1a1}"
by (auto simp add: PO_rhoare_defs R1a1_defs m1_defs)
lemma PO_m1_leak_refines_m1a_leak:
"{R1a1}
(m1a_leak Rs), (m1_leak Rs)
{> R1a1}"
by (auto simp add: PO_rhoare_defs R1a1_defs m1_defs)
lemma PO_m1_tick_refines_m1a_skip:
"{R1a1}
Id, (m1_tick T)
{> R1a1}"
by (auto simp add: PO_rhoare_defs R1a1_defs m1_defs)
text ‹All together now...›
lemmas PO_m1_trans_refines_m1a_trans =
PO_m1_step1_refines_m1a_step1 PO_m1_step2_refines_m1a_step2
PO_m1_step3_refines_m1a_step3 PO_m1_step4_refines_m1a_step4
PO_m1_step5_refines_m1a_step5 PO_m1_leak_refines_m1a_leak
PO_m1_tick_refines_m1a_skip
lemma PO_m1_refines_init_m1a [iff]:
"init m1 ⊆ R1a1``(init m1a)"
by (auto simp add: R1a1_defs m1_defs intro!: s0g_secrecyI)
lemma PO_m1_refines_trans_m1a [iff]:
"{R1a1}
(trans m1a), (trans m1)
{> R1a1}"
apply (auto simp add: m1_def m1_trans_def m1a_def m1a_trans_def
intro!: PO_m1_trans_refines_m1a_trans)
apply (force intro!: PO_m1_trans_refines_m1a_trans)+
done
text ‹Observation consistency.›
lemma obs_consistent_med1a1 [iff]:
"obs_consistent R1a1 med1a1 m1a m1"
by (auto simp add: obs_consistent_def R1a1_def m1a_def m1_def)
text ‹Refinement result.›
lemma PO_m1_refines_m1a [iff]:
"refines R1a1 med1a1 m1a m1"
by (rule Refinement_basic) (auto del: subsetI)
lemma m1_implements_m1: "implements med1a1 m1a m1"
by (rule refinement_soundness) (fast)
end