Theory m1_auth
chapter ‹Unidirectional Authentication Protocols›
text ‹In this chapter, we derive some simple unilateral authentication
protocols. We have a single abstract model at Level 1. We then refine this model
into two channel protocols (Level 2), one using authentic channels and one using
confidential channels. We then refine these in turn into cryptographic protocols
(Level 3) respectively using signatures and public-key encryption.
›
section ‹Refinement 1: Abstract Protocol›
theory m1_auth imports "../Refinement/Runs" "../Refinement/a0i_agree"
begin
declare domIff [simp, iff del]
subsection ‹State›
text ‹We introduce protocol runs.›
record m1_state =
runs :: runs_t
type_synonym
m1_obs = m1_state
definition
m1_init :: "m1_state set" where
"m1_init ≡ { ⦇
runs = Map.empty
⦈ }"
subsection ‹Events›
definition
m1_step1 :: "[rid_t, agent, agent, nonce] ⇒ (m1_state × m1_state) set"
where
"m1_step1 Ra A B Na ≡ {(s, s1).
Ra ∉ dom (runs s) ∧
Na = Ra$0 ∧
s1 = s⦇
runs := (runs s)(
Ra ↦ (Init, [A, B], [])
)
⦈
}"
definition
m1_step2 :: "[rid_t, agent, agent, nonce, nonce] ⇒ (m1_state × m1_state) set"
where
"m1_step2 Rb A B Na Nb ≡ {(s, s1).
Rb ∉ dom (runs s) ∧
Nb = Rb$0 ∧
s1 = s⦇
runs := (runs s)(Rb ↦ (Resp, [A, B], [aNon Na]))
⦈
}"
definition
m1_step3 ::
"[rid_t, agent, agent, nonce, nonce] ⇒ (m1_state × m1_state) set"
where
"m1_step3 Ra A B Na Nb ≡ {(s, s1).
runs s Ra = Some (Init, [A, B], []) ∧
Na = Ra$0 ∧
(A ∉ bad ∧ B ∉ bad ⟶ (∃Rb.
Nb = Rb$0 ∧ runs s Rb = Some (Resp, [A, B], [aNon Na]))) ∧
s1 = s⦇
runs := (runs s)(Ra ↦ (Init, [A, B], [aNon Nb]))
⦈
}"
text ‹Transition system.›
definition
m1_trans :: "(m1_state × m1_state) set" where
"m1_trans ≡ (⋃ A B Ra Rb Na Nb.
m1_step1 Ra A B Na ∪
m1_step2 Rb A B Na Nb ∪
m1_step3 Ra A B Na Nb ∪
Id
)"
definition
m1 :: "(m1_state, m1_obs) spec" where
"m1 ≡ ⦇
init = m1_init,
trans = m1_trans,
obs = id
⦈"
lemmas m1_defs =
m1_def m1_init_def m1_trans_def
m1_step1_def m1_step2_def m1_step3_def
subsection ‹Simulation relation›
text ‹We define two auxiliary functions to reconstruct the signals of the
initial model from completed initiator and responder runs of the current one.›
type_synonym
irsig = "nonce × nonce"
fun
runs2sigs :: "runs_t ⇒ irsig signal ⇒ nat"
where
"runs2sigs runz (Commit [A, B] (Ra$0, Nb)) =
(if runz Ra = Some (Init, [A, B], [aNon Nb]) then 1 else 0)"
| "runs2sigs runz (Running [A, B] (Na, Rb$0)) =
(if runz Rb = Some (Resp, [A, B], [aNon Na]) then 1 else 0)"
| "runs2sigs runz _ = 0"
text ‹Simulation relation and mediator function. We map completed initiator
and responder runs to commit and running signals, respectively.›
definition
med10 :: "m1_obs ⇒ irsig a0i_obs" where
"med10 o1 ≡ ⦇ signals = runs2sigs (runs o1), corrupted = {} ⦈"
definition
R01 :: "(irsig a0i_state × m1_state) set" where
"R01 ≡ {(s, t). signals s = runs2sigs (runs t) ∧ corrupted s = {} }"
lemmas R01_defs = R01_def med10_def
subsubsection ‹Lemmas about the auxiliary functions›
text ‹Basic lemmas›
lemma runs2sigs_empty [simp]:
"runz = Map.empty ⟹ runs2sigs runz = (λx. 0)"
by (rule ext, erule rev_mp)
(rule runs2sigs.induct, auto)
text ‹Update lemmas›
lemma runs2sigs_upd_init_none [simp]:
"⟦ Ra ∉ dom runz ⟧
⟹ runs2sigs (runz(Ra ↦ (Init, [A, B], []))) = runs2sigs runz"
by (rule ext, erule rev_mp)
(rule runs2sigs.induct, auto dest: dom_lemmas)
lemma runs2sigs_upd_init_some [simp]:
"⟦ runz Ra = Some (Init, [A, B], []) ⟧
⟹ runs2sigs (runz(Ra ↦ (Init, [A, B], [aNon Nb]))) =
(runs2sigs runz)(Commit [A, B] (Ra$0, Nb) := 1)"
by (rule ext, erule rev_mp)
(rule runs2sigs.induct, auto)
lemma runs2sigs_upd_resp [simp]:
"⟦ Rb ∉ dom runz ⟧
⟹ runs2sigs (runz(Rb ↦ (Resp, [A, B], [aNon Na]))) =
(runs2sigs runz)(Running [A, B] (Na, Rb$0) := 1)"
by (rule ext, (erule rev_mp)+)
(rule runs2sigs.induct, auto dest: dom_lemmas)
subsection ‹Refinement›
lemma PO_m1_step1_refines_skip:
"{R01}
Id, (m1_step1 Ra A B Na)
{> R01}"
by (auto simp add: PO_rhoare_def R01_defs a0i_defs m1_defs)
lemma PO_m1_step2_refines_a0i_running:
"{R01}
(a0i_running [A, B] (Na, Nb)), (m1_step2 Rb A B Na Nb)
{> R01}"
by (auto simp add: PO_rhoare_defs R01_defs a0i_defs m1_defs dest: dom_lemmas)
lemma PO_m1_step3_refines_a0i_commit:
"{R01}
(a0i_commit [A, B] (Na, Nb)), (m1_step3 Ra A B Na Nb)
{> R01}"
by (auto simp add: PO_rhoare_defs R01_defs a0i_defs m1_defs)
lemmas PO_m1_trans_refines_a0i_trans =
PO_m1_step1_refines_skip PO_m1_step2_refines_a0i_running
PO_m1_step3_refines_a0i_commit
text ‹All together now...›
lemma PO_m1_refines_init_a0i [iff]:
"init m1 ⊆ R01``(init a0i)"
by (auto simp add: R01_defs a0i_defs m1_defs)
lemma PO_m1_refines_trans_a0i [iff]:
"{R01}
(trans a0i), (trans m1)
{> R01}"
by (auto simp add: m1_def m1_trans_def a0i_def a0i_trans_def
intro!: PO_m1_trans_refines_a0i_trans)
lemma PO_obs_consistent [iff]:
"obs_consistent R01 med10 a0i m1"
by (auto simp add: obs_consistent_def R01_defs a0i_def m1_def)
lemma PO_m1_refines_a0i:
"refines R01 med10 a0i m1"
by (rule Refinement_basic) (auto)
end