Theory m3_enc
section ‹Refinement 3b: Encryption-based Dolev-Yao Protocol (Variant A)›
theory m3_enc imports m2_confid_chan "../Refinement/Message"
begin
text ‹This refines the channel protocol using public-key encryption and
adds a full-fledged Dolev-Yao adversary. In this variant, the adversary is
realized using Paulson's message derivation closure operators (as opposed to
a collection of one-step message construction and decomposition events a la
Strand spaces).›
text ‹Proof tool configuration. Avoid annoying automatic unfolding of
‹dom› (again).›
declare domIff [simp, iff del]
text ‹A general lemma about ‹parts› (move?!).›
lemmas parts_insertD = parts_insert [THEN equalityD1, THEN subsetD]
subsection ‹State and observations›
text ‹We extend the state of @{term m1} with two confidential channels
between each pair of agents, one channel for each protocol message.›
record m3_state = m1_state +
IK :: "msg set"
text ‹Observations: local agent states.›
type_synonym
m3_obs = m1_obs
definition
m3_obs :: "m3_state ⇒ m3_obs" where
"m3_obs s ≡ ⦇
runs = runs s
⦈"
subsection ‹Events›
definition
m3_step1 :: "[rid_t, agent, agent, nonce] ⇒ (m3_state × m3_state) set"
where
"m3_step1 Ra A B Na ≡ {(s, s1).
Ra ∉ dom (runs s) ∧
Na = Ra$0 ∧
s1 = s⦇
runs := (runs s)(Ra ↦ (Init, [A, B], [])),
IK := insert (Crypt (pubK B) ⦃Nonce Na, Agent A⦄) (IK s)
⦈
}"
definition
m3_step2 ::
"[rid_t, agent, agent, nonce, nonce] ⇒ (m3_state × m3_state) set"
where
"m3_step2 Rb A B Na Nb ≡ {(s, s1).
Rb ∉ dom (runs s) ∧
Nb = Rb$0 ∧
Crypt (pubK B) ⦃Nonce Na, Agent A⦄ ∈ IK s ∧
s1 = s⦇
runs := (runs s)(Rb ↦ (Resp, [A, B], [aNon Na])),
IK := insert (Crypt (pubK A) ⦃Nonce Na, Nonce Nb, Agent B⦄) (IK s)
⦈
}"
definition
m3_step3 :: "[rid_t, agent, agent, nonce, nonce] ⇒ (m3_state × m3_state) set"
where
"m3_step3 Ra A B Na Nb ≡ {(s, s1).
runs s Ra = Some (Init, [A, B], []) ∧
Na = Ra$0 ∧
Crypt (pubK A) ⦃Nonce Na, Nonce Nb, Agent B⦄ ∈ IK s ∧
s1 = s⦇
runs := (runs s)(Ra ↦ (Init, [A, B], [aNon Nb]))
⦈
}"
text ‹Standard Dolev-Yao intruder.›
definition
m3_DY_fake :: "(m3_state × m3_state) set"
where
"m3_DY_fake ≡ {(s, s1).
s1 = s⦇ IK := synth (analz (IK s)) ⦈
}"
text ‹Transition system.›
definition
m3_init :: "m3_state set"
where
"m3_init ≡ { ⦇
runs = Map.empty,
IK = (Key`priK`bad) ∪ (Key`range pubK) ∪ (Key`shrK`bad)
⦈ }"
definition
m3_trans :: "(m3_state × m3_state) set" where
"m3_trans ≡ (⋃ A B Ra Rb Na Nb.
m3_step1 Ra A B Na ∪
m3_step2 Rb A B Na Nb ∪
m3_step3 Ra A B Na Nb ∪
m3_DY_fake ∪
Id
)"
definition
m3 :: "(m3_state, m3_obs) spec" where
"m3 ≡ ⦇
init = m3_init,
trans = m3_trans,
obs = m3_obs
⦈"
lemmas m3_defs =
m3_def m3_init_def m3_trans_def m3_obs_def
m3_step1_def m3_step2_def m3_step3_def
m3_DY_fake_def
subsection ‹Invariants›
text ‹Automatic tool tuning. Tame too-agressive pair decomposition, which is
declared as a safe elim rule ([elim!]).›
lemmas MPair_parts [rule del, elim]
lemmas MPair_analz [rule del, elim]
text ‹Specialize injectiveness of @{term "parts"} and @{term "analz"} to
enable aggressive application.›
lemmas parts_Inj_IK = parts.Inj [where H="IK s" for s]
lemmas analz_Inj_IK = analz.Inj [where H="IK s" for s]
declare analz_into_parts [dest]
subsubsection ‹inv1: Key secrecy›
text ‹Decryption keys are secret, that is, the intruder only knows private
keys of corrupted agents.›
definition
m3_inv1_keys :: "m3_state set" where
"m3_inv1_keys ≡ {s. ∀ A.
Key (priK A) ∈ parts (IK s) ⟶ A ∈ bad
}"
lemmas m3_inv1_keysI = m3_inv1_keys_def [THEN setc_def_to_intro, rule_format]
lemmas m3_inv1_keysE [elim] =
m3_inv1_keys_def [THEN setc_def_to_elim, rule_format]
lemmas m3_inv1_keysD [dest] =
m3_inv1_keys_def [THEN setc_def_to_dest, rule_format, rotated 1]
lemma PO_m3_inv1_keys_init [iff]:
"init m3 ⊆ m3_inv1_keys"
by (auto simp add: PO_hoare_def m3_defs intro!: m3_inv1_keysI)
lemma PO_m3_inv1_keys_trans [iff]:
"{m3_inv1_keys} trans m3 {> m3_inv1_keys}"
by (auto simp add: PO_hoare_def m3_defs intro!: m3_inv1_keysI)
(auto)
lemma PO_m3_inv1_keys [iff]: "reach m3 ⊆ m3_inv1_keys"
by (rule inv_rule_basic, auto)
subsection ‹Simulation relation›
text ‹Simulation relation is canonical. It states that the protocol messages
appearing in the intruder knowledge refine those occurring on the abstract
confidential channels. Moreover, if the concrete intruder knows a nonce then so
does the abstract one (as defined by ‹ink›).›
text ‹Abstraction function on sets of messages.›
inductive_set
abs_msg :: "msg set ⇒ chmsg set"
for H :: "msg set"
where
am_msg1:
"Crypt (pubK B) ⦃Nonce Na, Agent A⦄ ∈ H
⟹ Confid A B (Msg [aNon Na]) ∈ abs_msg H"
| am_msg2:
"Crypt (pubK A) ⦃Nonce Na, Nonce Nb, Agent B⦄ ∈ H
⟹ Confid B A (Msg [aNon Na, aNon Nb]) ∈ abs_msg H"
declare abs_msg.intros [intro!]
declare abs_msg.cases [elim!]
text ‹The simulation relation is canonical. It states that the protocol
messages in the intruder knowledge refine the abstract messages appearing on
the confidential channels.›
definition
R23_msgs :: "(m2_state × m3_state) set" where
"R23_msgs ≡ {(s, t). abs_msg (parts (IK t)) ⊆ chan s}"
definition
R23_non :: "(m2_state × m3_state) set" where
"R23_non ≡ {(s, t). ∀N. Nonce N ∈ analz (IK t) ⟶ aNon N ∈ extr ik0 (chan s)}"
definition
R23_pres :: "(m2_state × m3_state) set" where
"R23_pres ≡ {(s, t). runs s = runs t}"
definition
R23 :: "(m2_state × m3_state) set" where
"R23 ≡ R23_msgs ∩ R23_non ∩ R23_pres"
lemmas R23_defs =
R23_def R23_msgs_def R23_non_def R23_pres_def
lemmas R23_msgsI =
R23_msgs_def [THEN rel_def_to_intro, simplified, rule_format]
lemmas R23_msgsE [elim] =
R23_msgs_def [THEN rel_def_to_elim, simplified, rule_format]
lemmas R23_msgsE' [elim] =
R23_msgs_def [THEN rel_def_to_dest, simplified, rule_format, THEN subsetD]
lemmas R23_nonI =
R23_non_def [THEN rel_def_to_intro, simplified, rule_format]
lemmas R23_nonE [elim] =
R23_non_def [THEN rel_def_to_elim, simplified, rule_format]
lemmas R23_presI =
R23_pres_def [THEN rel_def_to_intro, simplified, rule_format]
lemmas R23_presE [elim] =
R23_pres_def [THEN rel_def_to_elim, simplified, rule_format]
lemmas R23_intros = R23_msgsI R23_nonI R23_presI
text ‹Mediator function.›
abbreviation
med32 :: "m3_obs ⇒ m2_obs" where
"med32 ≡ id"
subsection ‹Misc lemmas›
text ‹General facts about @{term "abs_msg"}›
lemma abs_msg_empty: "abs_msg {} = {}"
by (auto)
lemma abs_msg_Un [simp]:
"abs_msg (G ∪ H) = abs_msg G ∪ abs_msg H"
by (auto)
lemma abs_msg_mono [elim]:
"⟦ m ∈ abs_msg G; G ⊆ H ⟧ ⟹ m ∈ abs_msg H"
by (auto)
lemma abs_msg_insert_mono [intro]:
"⟦ m ∈ abs_msg H ⟧ ⟹ m ∈ abs_msg (insert m' H)"
by (auto)
text ‹Abstraction of concretely fakeable message yields abstractly fakeable
messages. This is the key lemma for the refinement of the intruder.›
lemma abs_msg_DY_subset_fake:
"⟦ (s, t) ∈ R23_msgs; (s, t) ∈ R23_non; t ∈ m3_inv1_keys ⟧
⟹ abs_msg (synth (analz (IK t))) ⊆ fake ik0 (dom (runs s)) (chan s)"
apply (auto)
apply (rule fake_Inj, fastforce)
apply (rule fake_intros, auto)
apply (rule fake_Inj, fastforce)
apply (rule fake_intros, auto)
done
lemma abs_msg_parts_subset_fake:
"⟦ (s, t) ∈ R23_msgs ⟧
⟹ abs_msg (parts (IK t)) ⊆ fake ik0 (-dom (runs s)) (chan s)"
by (rule_tac B="chan s" in subset_trans) (auto)
declare abs_msg_DY_subset_fake [simp, intro!]
declare abs_msg_parts_subset_fake [simp, intro!]
subsection ‹Refinement proof›
text ‹Proofs obligations.›
lemma PO_m3_step1_refines_m2_step1:
"{R23 ∩ UNIV × m3_inv1_keys}
(m2_step1 Ra A B Na), (m3_step1 Ra A B Na)
{> R23}"
by (auto simp add: PO_rhoare_defs R23_def m2_defs m3_defs intro!: R23_intros)
(auto)
lemma PO_m3_step2_refines_m2_step2:
"{R23 ∩ UNIV × m3_inv1_keys}
(m2_step2 Rb A B Na Nb), (m3_step2 Rb A B Na Nb)
{> R23}"
by (auto simp add: PO_rhoare_defs R23_def m2_defs m3_defs intro!: R23_intros)
(auto)
lemma PO_m3_step3_refines_m2_step3:
"{R23}
(m2_step3 Ra A B Na Nb), (m3_step3 Ra A B Na Nb)
{> R23}"
by (auto simp add: PO_rhoare_defs R23_def m2_defs m3_defs intro!: R23_intros)
text ‹Dolev-Yao fake event refines abstract fake event.›
lemma PO_m3_DY_fake_refines_m2_fake:
"{R23 ∩ UNIV × m3_inv1_keys}
(m2_fake), (m3_DY_fake)
{> R23}"
by (auto simp add: PO_rhoare_defs R23_def m2_defs m3_defs)
(rule R23_intros, auto)+
text ‹All together now...›
lemmas PO_m3_trans_refines_m2_trans =
PO_m3_step1_refines_m2_step1 PO_m3_step2_refines_m2_step2
PO_m3_step3_refines_m2_step3 PO_m3_DY_fake_refines_m2_fake
lemma PO_m3_refines_init_m2 [iff]:
"init m3 ⊆ R23``(init m2)"
by (auto simp add: R23_defs m2_defs m3_defs)
lemma PO_m3_refines_trans_m2 [iff]:
"{R23 ∩ UNIV × m3_inv1_keys}
(trans m2), (trans m3)
{> R23}"
apply (auto simp add: m3_def m3_trans_def m2_def m2_trans_def)
apply (blast intro!: PO_m3_trans_refines_m2_trans)+
done
lemma PO_R23_obs_consistent [iff]:
"obs_consistent R23 med32 m2 m3"
by (auto simp add: obs_consistent_def R23_def m2_defs m3_defs)
lemma PO_m3_refines_m2 [iff]:
"refines
(R23 ∩ UNIV × m3_inv1_keys)
med32 m2 m3"
by (rule Refinement_using_invariants) (auto)
end