Theory Infra
chapter ‹Protocol Modeling and Refinement Infrastructure›
text ‹This chapter sets up our theory of refinement and the protocol
modeling infrastructure.›
section ‹Proving infrastructure›
theory Infra imports Main
begin
subsection ‹Prover configuration›
declare if_split_asm [split]
subsection ‹Forward reasoning ("attributes")›
text ‹The following lemmas are used to produce intro/elim rules from
set definitions and relation definitions.›
lemmas set_def_to_intro = meta_eq_to_obj_eq [THEN eqset_imp_iff, THEN iffD2]
lemmas set_def_to_dest = meta_eq_to_obj_eq [THEN eqset_imp_iff, THEN iffD1]
lemmas set_def_to_elim = set_def_to_dest [elim_format]
lemmas setc_def_to_intro =
set_def_to_intro [where B="{x. P x}" for P, to_pred]
lemmas setc_def_to_dest =
set_def_to_dest [where B="{x. P x}" for P, to_pred]
lemmas setc_def_to_elim = setc_def_to_dest [elim_format]
lemmas rel_def_to_intro = setc_def_to_intro [where x="(s, t)" for s t]
lemmas rel_def_to_dest = setc_def_to_dest [where x="(s, t)" for s t]
lemmas rel_def_to_elim = rel_def_to_dest [elim_format]
subsection ‹General results›
subsubsection ‹Maps›
text ‹We usually remove @{term"domIff"} from the simpset and clasets due
to annoying behavior. Sometimes the lemmas below are more well-behaved than
@{term "domIff"}. Usually to be used as "dest: dom\_lemmas". However, adding
them as permanent dest rules slows down proofs too much, so we refrain from
doing this.›
lemma map_definedness:
"f x = Some y ⟹ x ∈ dom f"
by (simp add: domIff)
lemma map_definedness_contra:
"⟦ f x = Some y; z ∉ dom f ⟧ ⟹ x ≠ z"
by (auto simp add: domIff)
lemmas dom_lemmas = map_definedness map_definedness_contra
subsubsection ‹Set›
lemma vimage_image_subset: "A ⊆ f-`(f`A)"
by (auto simp add: image_def vimage_def)
subsubsection ‹Relations›
lemma Image_compose [simp]:
"(R1 O R2)``A = R2``(R1``A)"
by (auto)
subsubsection ‹Lists›
lemma map_id: "map id = id"
by (simp)
lemma map_comp: "map (g o f) = map g o map f"
by (simp)
declare map_comp_map [simp del]
lemma take_prefix: "⟦ take n l = xs ⟧ ⟹ ∃xs'. l = xs @ xs'"
by (induct l arbitrary: n xs, auto)
(case_tac n, auto)
subsubsection ‹Finite sets›
text ‹Cardinality.›
declare arg_cong [where f=card, intro]
lemma finite_positive_cardI [intro!]:
"⟦ A ≠ {}; finite A ⟧ ⟹ 0 < card A"
by (auto)
lemma finite_positive_cardD [dest!]:
"⟦ 0 < card A; finite A ⟧ ⟹ A ≠ {}"
by (auto)
lemma finite_zero_cardI [intro!]:
"⟦ A = {}; finite A ⟧ ⟹ card A = 0"
by (auto)
lemma finite_zero_cardD [dest!]:
"⟦ card A = 0; finite A ⟧ ⟹ A = {}"
by (auto)
end
Theory Refinement
section ‹Models, Invariants and Refinements›
theory Refinement imports Infra
begin
subsection ‹Specifications, reachability, and behaviours.›
text ‹Transition systems are multi-pointed graphs.›
record 's TS =
init :: "'s set"
trans :: "('s × 's) set"
text ‹The inductive set of reachable states.›
inductive_set
reach :: "('s, 'a) TS_scheme ⇒ 's set"
for T :: "('s, 'a) TS_scheme"
where
r_init [intro]: "s ∈ init T ⟹ s ∈ reach T"
| r_trans [intro]: "⟦ (s, t) ∈ trans T; s ∈ reach T ⟧ ⟹ t ∈ reach T"
subsubsection ‹Finite behaviours›
text ‹Note that behaviours grow at the head of the list, i.e., the initial
state is at the end.›
inductive_set
beh :: "('s, 'a) TS_scheme ⇒ ('s list) set"
for T :: "('s, 'a) TS_scheme"
where
b_empty [iff]: "[] ∈ beh T"
| b_init [intro]: "s ∈ init T ⟹ [s] ∈ beh T"
| b_trans [intro]: "⟦ s # b ∈ beh T; (s, t) ∈ trans T ⟧ ⟹ t # s # b ∈ beh T"
inductive_cases beh_non_empty: "s # b ∈ beh T"
text ‹Behaviours are prefix closed.›
lemma beh_immediate_prefix_closed:
"s # b ∈ beh T ⟹ b ∈ beh T"
by (erule beh_non_empty, auto)
lemma beh_prefix_closed:
"c @ b ∈ beh T ⟹ b ∈ beh T"
by (induct c, auto dest!: beh_immediate_prefix_closed)
text ‹States in behaviours are exactly reachable.›
lemma beh_in_reach [rule_format]:
"b ∈ beh T ⟹ (∀s ∈ set b. s ∈ reach T)"
by (erule beh.induct) (auto)
lemma reach_in_beh:
assumes "s ∈ reach T" shows "∃b ∈ beh T. s ∈ set b"
using assms
proof (induction s rule: reach.induct)
case (r_init s)
hence "s ∈ set [s]" and "[s] ∈ beh T" by auto
thus ?case by fastforce
next
case (r_trans s t)
then obtain b where "b ∈ beh T" and "s ∈ set b" by blast
from ‹s ∈ set b› obtain b1 b2 where "b = b2 @ s # b1" by (blast dest: split_list)
with ‹b ∈ beh T› have "s # b1 ∈ beh T" by (blast intro: beh_prefix_closed)
with ‹(s, t) ∈ trans T› have "t # s # b1 ∈ beh T" by blast
thus ?case by force
qed
lemma reach_equiv_beh_states: "reach T = ⋃ (set`(beh T))"
by (auto intro!: reach_in_beh beh_in_reach)
subsubsection ‹Specifications, observability, and implementation›
text ‹Specifications add an observer function to transition systems.›
record ('s, 'o) spec = "'s TS" +
obs :: "'s ⇒ 'o"
lemma beh_obs_upd [simp]: "beh (S(| obs := x |)) = beh S"
by (safe) (erule beh.induct, auto)+
lemma reach_obs_upd [simp]: "reach (S(| obs := x |)) = reach S"
by (safe) (erule reach.induct, auto)+
text ‹Observable behaviour and reachability.›
definition
obeh :: "('s, 'o) spec ⇒ ('o list) set" where
"obeh S ≡ (map (obs S))`(beh S)"
definition
oreach :: "('s, 'o) spec ⇒ 'o set" where
"oreach S ≡ (obs S)`(reach S)"
lemma oreach_equiv_obeh_states:
"oreach S = ⋃ (set`(obeh S))"
by (auto simp add: reach_equiv_beh_states oreach_def obeh_def)
lemma obeh_pi_translation:
"(map pi)`(obeh S) = obeh (S(| obs := pi o (obs S) |))"
by (auto simp add: obeh_def image_comp)
lemma oreach_pi_translation:
"pi`(oreach S) = oreach (S(| obs := pi o (obs S) |))"
by (auto simp add: oreach_def)
text ‹A predicate $P$ on the states of a specification is \emph{observable}
if it cannot distinguish between states yielding the same observation.
Equivalently, $P$ is observable if it is the inverse image under the
observation function of a predicate on observations.›
definition
observable :: "['s ⇒ 'o, 's set] ⇒ bool"
where
"observable ob P ≡ ∀s s'. ob s = ob s' ⟶ s' ∈ P ⟶ s ∈ P"
definition
observable2 :: "['s ⇒ 'o, 's set] ⇒ bool"
where
"observable2 ob P ≡ ∃Q. P = ob-`Q"
definition
observable3 :: "['s ⇒ 'o, 's set] ⇒ bool"
where
"observable3 ob P ≡ ob-`ob`P ⊆ P"
lemma observableE [elim]:
"⟦observable ob P; ob s = ob s'; s' ∈ P⟧ ⟹ s ∈ P"
by (unfold observable_def) (fast)
lemma observable2_equiv_observable: "observable2 ob P = observable ob P"
by (unfold observable_def observable2_def) (auto)
lemma observable3_equiv_observable2: "observable3 ob P = observable2 ob P"
by (unfold observable3_def observable2_def) (auto)
lemma observable_id [simp]: "observable id P"
by (simp add: observable_def)
text ‹The set extension of a function @{term "ob"} is the left adjoint of
a Galois connection on the powerset lattices over domain and range of @{term "ob"}
where the right adjoint is the inverse image function.›
lemma image_vimage_adjoints: "(ob`P ⊆ Q) = (P ⊆ ob-`Q)"
by auto
declare image_vimage_subset [simp, intro]
declare vimage_image_subset [simp, intro]
text ‹Similar but "reversed" (wrt to adjointness) relationships only hold under
additional conditions.›
lemma image_r_vimage_l: "⟦ Q ⊆ ob`P; observable ob P ⟧ ⟹ ob-`Q ⊆ P"
by (auto)
lemma vimage_l_image_r: "⟦ ob-`Q ⊆ P; Q ⊆ range ob ⟧ ⟹ Q ⊆ ob`P"
by (drule image_mono [where f=ob], auto)
text ‹Internal and external invariants›
lemma external_from_internal_invariant:
"⟦ reach S ⊆ P; (obs S)`P ⊆ Q ⟧
⟹ oreach S ⊆ Q"
by (auto simp add: oreach_def)
lemma external_from_internal_invariant_vimage:
"⟦ reach S ⊆ P; P ⊆ (obs S)-`Q ⟧
⟹ oreach S ⊆ Q"
by (erule external_from_internal_invariant) (auto)
lemma external_to_internal_invariant_vimage:
"⟦ oreach S ⊆ Q; (obs S)-`Q ⊆ P ⟧
⟹ reach S ⊆ P"
by (auto simp add: oreach_def)
lemma external_to_internal_invariant:
"⟦ oreach S ⊆ Q; Q ⊆ (obs S)`P; observable (obs S) P ⟧
⟹ reach S ⊆ P"
by (erule external_to_internal_invariant_vimage) (auto)
lemma external_equiv_internal_invariant_vimage:
"⟦ P = (obs S)-`Q ⟧
⟹ (oreach S ⊆ Q) = (reach S ⊆ P)"
by (fast intro: external_from_internal_invariant_vimage
external_to_internal_invariant_vimage
del: subsetI)
lemma external_equiv_internal_invariant:
"⟦ (obs S)`P = Q; observable (obs S) P ⟧
⟹ (oreach S ⊆ Q) = (reach S ⊆ P)"
by (rule external_equiv_internal_invariant_vimage) (auto)
text ‹Our notion of implementation is inclusion of observable behaviours.›
definition
implements :: "['p ⇒ 'o, ('s, 'o) spec, ('t, 'p) spec] ⇒ bool" where
"implements pi Sa Sc ≡ (map pi)`(obeh Sc) ⊆ obeh Sa"
text ‹Reflexivity and transitivity›
lemma implements_refl: "implements id S S"
by (auto simp add: implements_def)
lemma implements_trans:
"⟦ implements pi1 S1 S2; implements pi2 S2 S3 ⟧
⟹ implements (pi1 o pi2) S1 S3"
by (fastforce simp add: implements_def image_subset_iff)
text ‹Preservation of external invariants›
lemma implements_oreach:
"implements pi Sa Sc ⟹ pi`(oreach Sc) ⊆ oreach Sa"
by (auto simp add: implements_def oreach_equiv_obeh_states dest!: subsetD)
lemma external_invariant_preservation:
"⟦ oreach Sa ⊆ Q; implements pi Sa Sc ⟧
⟹ pi`(oreach Sc) ⊆ Q"
by (rule subset_trans [OF implements_oreach]) (auto)
lemma external_invariant_translation:
"⟦ oreach Sa ⊆ Q; pi-`Q ⊆ P; implements pi Sa Sc ⟧
⟹ oreach Sc ⊆ P"
apply (rule subset_trans [OF vimage_image_subset, of pi])
apply (rule subset_trans [where B="pi-`Q"])
apply (intro vimage_mono external_invariant_preservation, auto)
done
text ‹Preservation of internal invariants›
lemma internal_invariant_translation:
"⟦ reach Sa ⊆ Pa; Pa ⊆ obs Sa -` Qa; pi -` Qa ⊆ Q; obs S -` Q ⊆ P;
implements pi Sa S ⟧
⟹ reach S ⊆ P"
by (rule external_from_internal_invariant_vimage [
THEN external_invariant_translation,
THEN external_to_internal_invariant_vimage])
subsection ‹Invariants›
text ‹First we define Hoare triples over transition relations and then
we derive proof rules to establish invariants.›
subsubsection ‹Hoare triples›
definition
PO_hoare :: "['s set, ('s × 's) set, 's set] ⇒ bool"
("(3{_} _ {> _})" [0, 0, 0] 90)
where
"{pre} R {> post} ≡ R``pre ⊆ post"
lemmas PO_hoare_defs = PO_hoare_def Image_def
lemma "{P} R {> Q} = (∀s t. s ∈ P ⟶ (s, t) ∈ R ⟶ t ∈ Q)"
by (auto simp add: PO_hoare_defs)
text ‹Some essential facts about Hoare triples.›
lemma hoare_conseq_left [intro]:
"⟦ {P'} R {> Q}; P ⊆ P' ⟧
⟹ {P} R {> Q}"
by (auto simp add: PO_hoare_defs)
lemma hoare_conseq_right:
"⟦ {P} R {> Q'}; Q' ⊆ Q ⟧
⟹ {P} R {> Q}"
by (auto simp add: PO_hoare_defs)
lemma hoare_false_left [simp]:
"{{}} R {> Q}"
by (auto simp add: PO_hoare_defs)
lemma hoare_true_right [simp]:
"{P} R {> UNIV}"
by (auto simp add: PO_hoare_defs)
lemma hoare_conj_right [intro!]:
"⟦ {P} R {> Q1}; {P} R {> Q2} ⟧
⟹ {P} R {> Q1 ∩ Q2}"
by (auto simp add: PO_hoare_defs)
text ‹Special transition relations.›
lemma hoare_stop [simp, intro!]:
"{P} {} {> Q}"
by (auto simp add: PO_hoare_defs)
lemma hoare_skip [simp, intro!]:
"P ⊆ Q ⟹ {P} Id {> Q}"
by (auto simp add: PO_hoare_defs)
lemma hoare_trans_Un [iff]:
"{P} R1 ∪ R2 {> Q} = ({P} R1 {> Q} ∧ {P} R2 {> Q})"
by (auto simp add: PO_hoare_defs)
lemma hoare_trans_UN [iff]:
"{P} ⋃ x. R x {> Q} = (∀x. {P} R x {> Q})"
by (auto simp add: PO_hoare_defs)
subsubsection ‹Characterization of reachability›
lemma reach_init: "reach T ⊆ I ⟹ init T ⊆ I"
by (auto dest: subsetD)
lemma reach_trans: "reach T ⊆ I ⟹ {reach T} trans T {> I}"
by (auto simp add: PO_hoare_defs)
text ‹Useful consequences.›
corollary init_reach [iff]: "init T ⊆ reach T"
by (rule reach_init, simp)
corollary trans_reach [iff]: "{reach T} trans T {> reach T}"
by (rule reach_trans, simp)
subsubsection ‹Invariant proof rules›
text ‹Basic proof rule for invariants.›
lemma inv_rule_basic:
"⟦ init T ⊆ P; {P} (trans T) {> P} ⟧
⟹ reach T ⊆ P"
by (safe, erule reach.induct, auto simp add: PO_hoare_def)
text ‹General invariant proof rule. This rule is complete (set
@{term "I = reach T"}).›
lemma inv_rule:
"⟦ init T ⊆ I; I ⊆ P; {I} (trans T) {> I} ⟧
⟹ reach T ⊆ P"
apply (rule subset_trans, auto)
apply (erule reach.induct, auto simp add: PO_hoare_def)
done
text ‹The following rule is equivalent to the previous one.›
lemma INV_rule:
"⟦ init T ⊆ I; {I ∩ reach T} (trans T) {> I} ⟧
⟹ reach T ⊆ I"
by (safe, erule reach.induct, auto simp add: PO_hoare_defs)
text ‹Proof of equivalence.›
lemma inv_rule_from_INV_rule:
"⟦ init T ⊆ I; I ⊆ P; {I} (trans T) {> I} ⟧
⟹ reach T ⊆ P"
apply (rule subset_trans, auto del: subsetI)
apply (rule INV_rule, auto)
done
lemma INV_rule_from_inv_rule:
"⟦ init T ⊆ I; {I ∩ reach T} (trans T) {> I} ⟧
⟹ reach T ⊆ I"
by (rule_tac I="I ∩ reach T" in inv_rule, auto)
text ‹Incremental proof rule for invariants using auxiliary invariant(s).
This rule might have become obsolete by addition of $INV\_rule$.›
lemma inv_rule_incr:
"⟦ init T ⊆ I; {I ∩ J} (trans T) {> I}; reach T ⊆ J ⟧
⟹ reach T ⊆ I"
by (rule INV_rule, auto)
subsection ‹Refinement›
text ‹Our notion of refinement is simulation. We first define a general
notion of relational Hoare tuple, which we then use to define the refinement
proof obligation. Finally, we show that observation-consistent refinement
of specifications implies the implementation relation between them.›
subsubsection ‹Relational Hoare tuples›
text ‹Relational Hoare tuples formalize the following generalized simulation
diagram:
\begin{verbatim}
o -- Ra --> o
| |
pre post
| |
v V
o -- Rc --> o
\end{verbatim}
Here, $Ra$ and $Rc$ are the abstract and concrete transition relations,
and $pre$ and $post$ are the pre- and post-relations.
(In the definiton below, the operator @{term "(O)"} stands for relational
composition, which is defined as follows: @{thm relcomp_def [no_vars]}.)›
definition
PO_rhoare ::
"[('s × 't) set, ('s × 's) set, ('t × 't) set, ('s × 't) set] ⇒ bool"
("(4{_} _, _ {> _})" [0, 0, 0] 90)
where
"{pre} Ra, Rc {> post} ≡ pre O Rc ⊆ Ra O post"
lemmas PO_rhoare_defs = PO_rhoare_def relcomp_unfold
text ‹Facts about relational Hoare tuples.›
lemma relhoare_conseq_left [intro]:
"⟦ {pre'} Ra, Rc {> post}; pre ⊆ pre' ⟧
⟹ {pre} Ra, Rc {> post}"
by (auto simp add: PO_rhoare_defs dest!: subsetD)
lemma relhoare_conseq_right:
"⟦ {pre} Ra, Rc {> post'}; post' ⊆ post ⟧
⟹ {pre} Ra, Rc {> post}"
by (auto simp add: PO_rhoare_defs)
lemma relhoare_false_left [simp]:
"{ {} } Ra, Rc {> post}"
by (auto simp add: PO_rhoare_defs)
lemma relhoare_true_right [simp]:
"{pre} Ra, Rc {> UNIV} = (Domain (pre O Rc) ⊆ Domain Ra)"
by (auto simp add: PO_rhoare_defs)
lemma Domain_rel_comp [intro]:
"Domain pre ⊆ R ⟹ Domain (pre O Rc) ⊆ R"
by (auto simp add: Domain_def)
lemma rel_hoare_skip [iff]: "{R} Id, Id {> R}"
by (auto simp add: PO_rhoare_def)
text ‹Reflexivity and transitivity.›
lemma relhoare_refl [simp]: "{Id} R, R {> Id}"
by (auto simp add: PO_rhoare_defs)
lemma rhoare_trans:
"⟦ {R1} T1, T2 {> R1}; {R2} T2, T3 {> R2} ⟧
⟹ {R1 O R2} T1, T3 {> R1 O R2}"
apply (auto simp add: PO_rhoare_def del: subsetI)
apply (drule subset_refl [THEN relcomp_mono, where r=R1])
apply (drule subset_refl [THEN [2] relcomp_mono, where s=R2])
apply (auto simp add: O_assoc del: subsetI)
done
text ‹Conjunction in the post-relation cannot be split in general. However,
here are two useful special cases. In the first case the abstract transtition
relation is deterministic and in the second case one conjunct is a cartesian
product of two state predicates.›
lemma relhoare_conj_right_det:
"⟦ {pre} Ra, Rc {> post1}; {pre} Ra, Rc {> post2};
single_valued Ra ⟧
⟹ {pre} Ra, Rc {> post1 ∩ post2}"
by (auto simp add: PO_rhoare_defs dest: single_valuedD dest!: subsetD)
lemma relhoare_conj_right_cartesian [intro]:
"⟦ {Domain pre} Ra {> I}; {Range pre} Rc {> J};
{pre} Ra, Rc {> post} ⟧
⟹ {pre} Ra, Rc {> post ∩ I × J}"
by (force simp add: PO_rhoare_defs PO_hoare_defs Domain_def Range_def)
text ‹Separate rule for cartesian products.›
corollary relhoare_cartesian:
"⟦ {Domain pre} Ra {> I}; {Range pre} Rc {> J};
{pre} Ra, Rc {> post} ⟧
⟹ {pre} Ra, Rc {> I × J}"
by (auto intro: relhoare_conseq_right)
text ‹Unions of transition relations.›
lemma relhoare_concrete_Un [simp]:
"{pre} Ra, Rc1 ∪ Rc2 {> post}
= ({pre} Ra, Rc1 {> post} ∧ {pre} Ra, Rc2 {> post})"
apply (auto simp add: PO_rhoare_defs)
apply (auto dest!: subsetD)
done
lemma relhoare_concrete_UN [simp]:
"{pre} Ra, ⋃x. Rc x {> post} = (∀x. {pre} Ra, Rc x {> post})"
apply (auto simp add: PO_rhoare_defs)
apply (auto dest!: subsetD)
done
lemma relhoare_abstract_Un_left [intro]:
"⟦ {pre} Ra1, Rc {> post} ⟧
⟹ {pre} Ra1 ∪ Ra2, Rc {> post}"
by (auto simp add: PO_rhoare_defs)
lemma relhoare_abstract_Un_right [intro]:
"⟦ {pre} Ra2, Rc {> post} ⟧
⟹ {pre} Ra1 ∪ Ra2, Rc {> post}"
by (auto simp add: PO_rhoare_defs)
lemma relhoare_abstract_UN [intro!]:
"⟦ {pre} Ra x, Rc {> post} ⟧
⟹ {pre} ⋃x. Ra x, Rc {> post}"
apply (auto simp add: PO_rhoare_defs)
apply (auto dest!: subsetD)
done
subsubsection ‹Refinement proof obligations›
text ‹A transition system refines another one if the initial states and the
transitions are refined.
Initial state refinement means that for each concrete initial state there is
a related abstract one. Transition refinement means that the simulation
relation is preserved (as expressed by a relational Hoare tuple).
›
definition
PO_refines ::
"[('s × 't) set, ('s, 'a) TS_scheme, ('t, 'b) TS_scheme] ⇒ bool"
where
"PO_refines R Ta Tc ≡ (
init Tc ⊆ R``(init Ta)
∧ {R} (trans Ta), (trans Tc) {> R}
)"
lemma PO_refinesI:
"⟦ init Tc ⊆ R``(init Ta); {R} (trans Ta), (trans Tc) {> R} ⟧ ⟹ PO_refines R Ta Tc"
by (simp add: PO_refines_def)
lemma PO_refinesE [elim]:
"⟦ PO_refines R Ta Tc; ⟦ init Tc ⊆ R``(init Ta); {R} (trans Ta), (trans Tc) {> R} ⟧ ⟹ P ⟧
⟹ P"
by (simp add: PO_refines_def)
text ‹Basic refinement rule. This is just an introduction rule for the
definition.›
lemma refine_basic:
"⟦ init Tc ⊆ R``(init Ta); {R} (trans Ta), (trans Tc) {> R} ⟧
⟹ PO_refines R Ta Tc"
by (simp add: PO_refines_def)
text ‹The following proof rule uses individual invariants @{term "I"}
and @{term "J"} of the concrete and abstract systems to strengthen the
simulation relation $R$.
The hypotheses state that these state predicates are indeed invariants.
Note that the pre-condition of the invariant preservation hypotheses for
@{term "I"} and @{term "J"} are strengthened by adding the predicates
@{term "Domain (R ∩ UNIV × J)"} and @{term "Range (R ∩ I × UNIV)"},
respectively. In particular, the latter predicate may be essential, if a
concrete invariant depends on the simulation relation and an abstract invariant,
i.e. to "transport" abstract invariants to the concrete system.›
lemma refine_init_using_invariants:
"⟦ init Tc ⊆ R``(init Ta); init Ta ⊆ I; init Tc ⊆ J ⟧
⟹ init Tc ⊆ (R ∩ I × J)``(init Ta)"
by (auto simp add: Image_def dest!: bspec subsetD)
lemma refine_trans_using_invariants:
"⟦ {R ∩ I × J} (trans Ta), (trans Tc) {> R};
{I ∩ Domain (R ∩ UNIV × J)} (trans Ta) {> I};
{J ∩ Range (R ∩ I × UNIV)} (trans Tc) {> J} ⟧
⟹ {R ∩ I × J} (trans Ta), (trans Tc) {> R ∩ I × J}"
by (rule relhoare_conj_right_cartesian) (auto)
text ‹This is our main rule for refinements.›
lemma refine_using_invariants:
"⟦ {R ∩ I × J} (trans Ta), (trans Tc) {> R};
{I ∩ Domain (R ∩ UNIV × J)} (trans Ta) {> I};
{J ∩ Range (R ∩ I × UNIV)} (trans Tc) {> J};
init Tc ⊆ R``(init Ta);
init Ta ⊆ I; init Tc ⊆ J ⟧
⟹ PO_refines (R ∩ I × J) Ta Tc"
by (unfold PO_refines_def)
(intro refine_init_using_invariants refine_trans_using_invariants conjI)
subsubsection ‹Deriving invariants from refinements›
text ‹Some invariants can only be proved after the simulation has been
established, because they depend on the simulation relation and some abstract
invariants. Here is a rule to derive invariant theorems from the refinement.›
lemma PO_refines_implies_Range_init:
"PO_refines R Ta Tc ⟹ init Tc ⊆ Range R"
by (auto simp add: PO_refines_def)
lemma PO_refines_implies_Range_trans:
"PO_refines R Ta Tc ⟹ {Range R} trans Tc {> Range R}"
by (auto simp add: PO_refines_def PO_rhoare_def PO_hoare_def)
lemma PO_refines_implies_Range_invariant:
"PO_refines R Ta Tc ⟹ reach Tc ⊆ Range R"
by (rule INV_rule)
(auto intro!: PO_refines_implies_Range_init
PO_refines_implies_Range_trans)
text ‹The following rules are more useful in proofs.›
corollary INV_init_from_refinement:
"⟦ PO_refines R Ta Tc; Range R ⊆ I ⟧
⟹ init Tc ⊆ I"
by (drule PO_refines_implies_Range_init, auto)
corollary INV_trans_from_refinement:
"⟦ PO_refines R Ta Tc; K ⊆ Range R; Range R ⊆ I ⟧
⟹ {K} trans Tc {> I}"
apply (drule PO_refines_implies_Range_trans)
apply (auto intro: hoare_conseq_right)
done
corollary INV_from_refinement:
"⟦ PO_refines R Ta Tc; Range R ⊆ I ⟧
⟹ reach Tc ⊆ I"
by (drule PO_refines_implies_Range_invariant, fast)
subsubsection ‹Refinement of specifications›
text ‹Lift relation membership to finite sequences›
inductive_set
seq_lift :: "('s × 't) set ⇒ ('s list × 't list) set"
for R :: "('s × 't) set"
where
sl_nil [iff]: "([], []) ∈ seq_lift R"
| sl_cons [intro]:
"⟦ (xs, ys) ∈ seq_lift R; (x, y) ∈ R ⟧ ⟹ (x#xs, y#ys) ∈ seq_lift R"
inductive_cases sl_cons_right_invert: "(ba', t # bc) ∈ seq_lift R"
text ‹For each concrete behaviour there is a related abstract one.›
lemma behaviour_refinement:
"⟦ PO_refines R Ta Tc; bc ∈ beh Tc⟧
⟹ ∃ba ∈ beh Ta. (ba, bc) ∈ seq_lift R"
apply (erule beh.induct, auto)
apply (clarsimp simp add: PO_refines_def Image_def)
apply (drule subsetD, auto)
apply (erule sl_cons_right_invert, clarsimp)
apply (rename_tac s bc s' ba t)
apply (auto simp add: PO_refines_def PO_rhoare_def)
apply (thin_tac "X ⊆ Y" for X Y)
apply (drule subsetD, auto)
done
text ‹Observation consistency of a relation is defined using a mediator
function @{term "pi"} to abstract the concrete observation. This allows us
to also refine the observables as we move down a refinement branch.
›
definition
obs_consistent ::
"[('s × 't) set, 'p ⇒ 'o, ('s, 'o) spec, ('t, 'p) spec] ⇒ bool"
where
"obs_consistent R pi Sa Sc ≡ (∀s t. (s, t) ∈ R ⟶ pi (obs Sc t) = obs Sa s)"
lemma obs_consistent_refl [iff]: "obs_consistent Id id S S"
by (simp add: obs_consistent_def)
lemma obs_consistent_trans [intro]:
"⟦ obs_consistent R1 pi1 S1 S2; obs_consistent R2 pi2 S2 S3 ⟧
⟹ obs_consistent (R1 O R2) (pi1 o pi2) S1 S3"
by (auto simp add: obs_consistent_def)
lemma obs_consistent_empty: "obs_consistent {} pi Sa Sc"
by (auto simp add: obs_consistent_def)
lemma obs_consistent_conj1 [intro]:
"obs_consistent R pi Sa Sc ⟹ obs_consistent (R ∩ R') pi Sa Sc"
by (auto simp add: obs_consistent_def)
lemma obs_consistent_conj2 [intro]:
"obs_consistent R pi Sa Sc ⟹ obs_consistent (R' ∩ R) pi Sa Sc"
by (auto simp add: obs_consistent_def)
lemma obs_consistent_behaviours:
"⟦ obs_consistent R pi Sa Sc; bc ∈ beh Sc; ba ∈ beh Sa; (ba, bc) ∈ seq_lift R⟧
⟹ map pi (map (obs Sc) bc) = map (obs Sa) ba"
by (erule seq_lift.induct) (auto simp add: obs_consistent_def)
text ‹Definition of refinement proof obligations.›
definition
refines ::
"[('s × 't) set, 'p ⇒ 'o, ('s, 'o) spec, ('t, 'p) spec] ⇒ bool"
where
"refines R pi Sa Sc ≡ obs_consistent R pi Sa Sc ∧ PO_refines R Sa Sc"
lemmas refines_defs =
refines_def PO_refines_def
lemma refinesI:
"⟦ PO_refines R Sa Sc; obs_consistent R pi Sa Sc ⟧
⟹ refines R pi Sa Sc"
by (simp add: refines_def)
lemma refinesE [elim]:
"⟦ refines R pi Sa Sc; ⟦ PO_refines R Sa Sc; obs_consistent R pi Sa Sc ⟧ ⟹ P ⟧
⟹ P"
by (simp add: refines_def)
text ‹Reflexivity and transitivity of refinement.›
lemma refinement_reflexive: "refines Id id S S"
by (auto simp add: refines_defs)
lemma refinement_transitive:
"⟦ refines R1 pi1 S1 S2; refines R2 pi2 S2 S3 ⟧
⟹ refines (R1 O R2) (pi1 o pi2) S1 S3"
apply (auto simp add: refines_defs del: subsetI
intro: rhoare_trans)
apply (fastforce dest: Image_mono)
done
text ‹Soundness of refinement for proving implementation›
lemma observable_behaviour_refinement:
"⟦ refines R pi Sa Sc; bc ∈ obeh Sc ⟧ ⟹ map pi bc ∈ obeh Sa"
by (auto simp add: refines_def obeh_def image_def
dest!: behaviour_refinement obs_consistent_behaviours)
theorem refinement_soundness:
"refines R pi Sa Sc ⟹ implements pi Sa Sc"
by (auto simp add: implements_def
elim!: observable_behaviour_refinement)
text ‹Extended versions of refinement proof rules including observations›
lemmas Refinement_basic = refine_basic [THEN refinesI]
lemmas Refinement_using_invariants = refine_using_invariants [THEN refinesI]
lemma refines_reachable_strengthening:
"refines R pi Sa Sc ⟹ refines (R ∩ reach Sa × reach Sc) pi Sa Sc"
by (auto intro!: Refinement_using_invariants)
text ‹Inhertitance of internal invariants through refinements›
lemma INV_init_from_Refinement:
"⟦refines R pi Sa Sc; Range R ⊆ I⟧ ⟹ init Sc ⊆ I"
by (blast intro: INV_init_from_refinement)
lemma INV_trans_from_Refinement:
" ⟦refines R pi Sa Sc; K ⊆ Range R; Range R ⊆ I⟧ ⟹ {K} TS.trans Sc {> I}"
by (blast intro: INV_trans_from_refinement)
lemma INV_from_Refinement_basic:
"⟦ refines R pi Sa Sc; Range R ⊆ I ⟧ ⟹ reach Sc ⊆ I"
by (rule INV_from_refinement) blast
lemma INV_from_Refinement_using_invariants:
assumes "refines R pi Sa Sc" "Range (R ∩ I × J) ⊆ K"
"reach Sa ⊆ I" "reach Sc ⊆ J"
shows "reach Sc ⊆ K"
proof (rule INV_from_Refinement_basic)
show "refines (R ∩ reach Sa × reach Sc) pi Sa Sc" using assms(1)
by (rule refines_reachable_strengthening)
next
show "Range (R ∩ reach Sa × reach Sc) ⊆ K" using assms(2-4) by blast
qed
end
Theory Agents
section ‹Atomic messages›
theory Agents imports Main
begin
text ‹The definitions below are moved here from the message theory, since
the higher levels of protocol abstraction do not know about cryptographic
messages.›
subsection ‹Agents›
datatype
agent = Server | Agent nat
consts
bad :: "agent set"
specification (bad)
Server_not_bad [iff]: "Server ∉ bad"
by (rule exI [of _ "{Agent 0}"], simp)
abbreviation
good :: "agent set"
where
"good ≡ -bad"
abbreviation
Sv :: "agent"
where
"Sv ≡ Server"
subsection ‹Nonces›
text ‹We have an unspecified type of freshness identifiers.
For executability, we may need to assume that this type is infinite.›
typedecl fid_t
datatype fresh_t =
mk_fresh "fid_t" "nat" (infixr "$" 65)
fun fid :: "fresh_t ⇒ fid_t" where
"fid (f $ n) = f"
fun num :: "fresh_t ⇒ nat" where
"num (f $ n) = n"
text ‹Nonces›
type_synonym
nonce = "fresh_t"
end
Theory Keys
section ‹Symmetric and Assymetric Keys›
theory Keys imports Agents begin
text ‹Divide keys into session and long-term keys. Define different kinds
of long-term keys in second step.›
datatype ltkey =
sharK "agent"
| publK "agent"
| privK "agent"
datatype key =
sesK "fresh_t"
| ltK "ltkey"
abbreviation
shrK :: "agent ⇒ key" where
"shrK A ≡ ltK (sharK A)"
abbreviation
pubK :: "agent ⇒ key" where
"pubK A ≡ ltK (publK A)"
abbreviation
priK :: "agent ⇒ key" where
"priK A ≡ ltK (privK A)"
text‹The inverse of a symmetric key is itself; that of a public key
is the private key and vice versa›
fun invKey :: "key ⇒ key" where
"invKey (ltK (publK A)) = priK A"
| "invKey (ltK (privK A)) = pubK A"
| "invKey K = K"
definition
symKeys :: "key set" where
"symKeys ≡ {K. invKey K = K}"
lemma invKey_K: "K ∈ symKeys ⟹ invKey K = K"
by (simp add: symKeys_def)
text ‹Most lemmas we need come for free with the inductive type definition:
injectiveness and distinctness.›
lemma invKey_invKey_id [simp]: "invKey (invKey K) = K"
by (cases K, auto)
(rename_tac ltk, case_tac ltk, auto)
lemma invKey_eq [simp]: "(invKey K = invKey K') = (K=K')"
apply (safe)
apply (drule_tac f=invKey in arg_cong, simp)
done
text ‹We get most lemmas below for free from the inductive definition
of type @{typ key}. Many of these are just proved as a reality check.›
subsection‹Asymmetric Keys›
text ‹No private key equals any public key (essential to ensure that private
keys are private!). A similar statement an axiom in Paulson's theory!›
lemma privateKey_neq_publicKey: "priK A ≠ pubK A'"
by auto
lemma publicKey_neq_privateKey: "pubK A ≠ priK A'"
by auto
subsection‹Basic properties of @{term pubK} and @{term priK}›
lemma publicKey_inject [iff]: "(pubK A = pubK A') = (A = A')"
by (auto)
lemma not_symKeys_pubK [iff]: "pubK A ∉ symKeys"
by (simp add: symKeys_def)
lemma not_symKeys_priK [iff]: "priK A ∉ symKeys"
by (simp add: symKeys_def)
lemma symKey_neq_priK: "K ∈ symKeys ⟹ K ≠ priK A"
by (auto simp add: symKeys_def)
lemma symKeys_neq_imp_neq: "(K ∈ symKeys) ≠ (K' ∈ symKeys) ⟹ K ≠ K'"
by blast
lemma symKeys_invKey_iff [iff]: "(invKey K ∈ symKeys) = (K ∈ symKeys)"
by (unfold symKeys_def, auto)
subsection‹"Image" equations that hold for injective functions›
lemma invKey_image_eq [simp]: "(invKey x ∈ invKey`A) = (x ∈ A)"
by auto
lemma invKey_pubK_image_priK_image [simp]: "invKey ` pubK ` AS = priK ` AS"
by (auto simp add: image_def)
lemma publicKey_notin_image_privateKey: "pubK A ∉ priK ` AS"
by auto
lemma privateKey_notin_image_publicKey: "priK x ∉ pubK ` AA"
by auto
lemma publicKey_image_eq [simp]: "(pubK x ∈ pubK ` AA) = (x ∈ AA)"
by auto
lemma privateKey_image_eq [simp]: "(priK A ∈ priK ` AS) = (A ∈ AS)"
by auto
subsection‹Symmetric Keys›
text ‹The following was stated as an axiom in Paulson's theory.›
lemma sym_sesK: "sesK f ∈ symKeys"
by (simp add: symKeys_def)
lemma sym_shrK: "shrK X ∈ symKeys"
by (simp add: symKeys_def)
text ‹Symmetric keys and inversion›
lemma symK_eq_invKey: "⟦ SK = invKey K; SK ∈ symKeys ⟧ ⟹ K = SK"
by (auto simp add: symKeys_def)
text ‹Image-related lemmas.›
lemma publicKey_notin_image_shrK: "pubK x ∉ shrK ` AA"
by auto
lemma privateKey_notin_image_shrK: "priK x ∉ shrK ` AA"
by auto
lemma shrK_notin_image_publicKey: "shrK x ∉ pubK ` AA"
by auto
lemma shrK_notin_image_privateKey: "shrK x ∉ priK ` AA"
by auto
lemma sesK_notin_image_shrK [simp]: "sesK K ∉ shrK`AA"
by (auto)
lemma shrK_notin_image_sesK [simp]: "shrK K ∉ sesK`AA"
by (auto)
lemma sesK_image_eq [simp]: "(sesK x ∈ sesK ` AA) = (x ∈ AA)"
by auto
lemma shrK_image_eq [simp]: "(shrK x ∈ shrK ` AA) = (x ∈ AA)"
by auto
end
Theory Atoms
section ‹Atomic messages›
theory Atoms imports Keys
begin
subsection ‹Atoms datatype›
datatype atom =
aAgt "agent"
| aNon "nonce"
| aKey "key"
| aNum "nat"
subsection ‹Long-term key setup (abstractly)›
text ‹Suppose an initial long-term key setup without looking into the
structure of long-term keys.
Remark: This setup is agnostic with respect to the structure of the
type @{typ "ltkey"}. Ideally, the type @{typ "ltkey"} should be a
parameter of the type @{typ "key"}, which is instantiated only at
Level 3.›
consts
ltkeySetup :: "(ltkey × agent) set"
text ‹The initial key setup contains static, long-term keys.›
definition
keySetup :: "(key × agent) set" where
"keySetup ≡ {(ltK K, A) | K A. (K, A) ∈ ltkeySetup}"
text ‹Corrupted keys are the long-term keys known by bad agents.›
definition
corrKey :: "key set" where
"corrKey ≡ keySetup¯ `` bad"
lemma corrKey_Dom_keySetup [simp, intro]: "K ∈ corrKey ⟹ K ∈ Domain keySetup"
by (auto simp add: corrKey_def)
lemma keySetup_noSessionKeys [simp]: "(sesK K, A) ∉ keySetup"
by (simp add: keySetup_def)
lemma corrKey_noSessionKeys [simp]: "sesK K ∉ corrKey"
by (auto simp add: keySetup_def corrKey_def)
end
Theory Runs
section ‹Protocol runs›
theory Runs imports Atoms
begin
subsection ‹Runs›
text ‹Define some typical roles.›
datatype role_t = Init | Resp | Serv
fun
roleIdx :: "role_t ⇒ nat"
where
"roleIdx Init = 0"
| "roleIdx Resp = 1"
| "roleIdx Serv = 2"
text ‹The type of runs is a partial function from run identifiers to
a triple consisting of a role, a list of agents, and a list of atomic messages
recorded during the run's execution.
The type of roles could be made a parameter for more flexibility.›
type_synonym
rid_t = "fid_t"
type_synonym
runs_t = "rid_t ⇀ role_t × agent list × atom list"
subsection ‹Run abstraction›
text ‹Define a function that lifts a function on roles and atom lists
to a function on runs.›
definition
map_runs :: "([role_t, atom list] ⇒ atom list) ⇒ runs_t ⇒ runs_t"
where
"map_runs h runz rid ≡ case runz rid of
None ⇒ None
| Some (rol, agts, al) ⇒ Some (rol, agts, h rol al)"
lemma map_runs_empty [simp]: "map_runs h Map.empty = Map.empty"
by (rule ext) (auto simp add: map_runs_def)
lemma map_runs_dom [simp]: "dom (map_runs h runz) = dom runz"
by (auto simp add: map_runs_def split: option.split_asm)
lemma map_runs_update [simp]:
"map_runs h (runz(R ↦ (rol, agts, al)))
= (map_runs h runz)(R ↦ (rol, agts, h rol al))"
by (auto simp add: map_runs_def)
end
Theory Channels
section ‹Channel Messages›
theory Channels imports Atoms
begin
subsection ‹Channel messages›
datatype secprop = auth | confid
type_synonym
chtyp = "secprop set"
abbreviation
secure :: chtyp where
"secure ≡ {auth, confid}"
datatype payload = Msg "atom list"
datatype chmsg =
StatCh "chtyp" "agent" "agent" "payload"
| DynCh "chtyp" "key" "payload"
text ‹Abbreviations for use in protocol defs›
abbreviation
Insec :: "[agent, agent, payload] ⇒ chmsg" where
"Insec ≡ StatCh {}"
abbreviation
Confid :: "[agent, agent, payload] ⇒ chmsg" where
"Confid ≡ StatCh {confid}"
abbreviation
Auth :: "[agent, agent, payload] ⇒ chmsg" where
"Auth ≡ StatCh {auth}"
abbreviation
Secure :: "[agent, agent, payload] ⇒ chmsg" where
"Secure ≡ StatCh {auth, confid}"
abbreviation
dConfid :: "[key, payload] ⇒ chmsg" where
"dConfid ≡ DynCh {confid}"
abbreviation
dAuth :: "[key, payload] ⇒ chmsg" where
"dAuth ≡ DynCh {auth}"
abbreviation
dSecure :: "[key, payload] ⇒ chmsg" where
"dSecure ≡ DynCh {auth, confid}"
subsection ‹Keys used in dynamic channel messages›
definition
keys_for :: "chmsg set ⇒ key set" where
"keys_for H ≡ {K. ∃c M. DynCh c K M ∈ H}"
lemma keys_forI [dest]: "DynCh c K M ∈ H ⟹ K ∈ keys_for H"
by (auto simp add: keys_for_def)
lemma keys_for_empty [simp]: "keys_for {} = {}"
by (simp add: keys_for_def)
lemma keys_for_monotone: "G ⊆ H ⟹ keys_for G ⊆ keys_for H"
by (auto simp add: keys_for_def)
lemmas keys_for_mono [elim] = keys_for_monotone [THEN [2] rev_subsetD]
lemma keys_for_insert_StatCh [simp]:
"keys_for (insert (StatCh c A B M) H) = keys_for H"
by (auto simp add: keys_for_def)
lemma keys_for_insert_DynCh [simp]:
"keys_for (insert (DynCh c K M) H) = insert K (keys_for H)"
by (auto simp add: keys_for_def)
subsection ‹Atoms in a set of channel messages›
text ‹The set of atoms contained in a set of channel messages. We also
include the public atoms, i.e., the agent names, numbers, and corrupted keys.
›
inductive_set
atoms :: "chmsg set ⇒ atom set"
for H :: "chmsg set"
where
at_StatCh: "⟦ StatCh c A B (Msg M) ∈ H; At ∈ set M ⟧ ⟹ At ∈ atoms H"
| at_DynCh: "⟦ DynCh c K (Msg M) ∈ H; At ∈ set M ⟧ ⟹ At ∈ atoms H"
declare atoms.intros [intro]
lemma atoms_empty [simp]: "atoms {} = {}"
by (auto elim!: atoms.cases)
lemma atoms_monotone: "G ⊆ H ⟹ atoms G ⊆ atoms H"
by (auto elim!: atoms.cases)
lemmas atoms_mono [elim] = atoms_monotone [THEN [2] rev_subsetD]
lemma atoms_insert_StatCh [simp]:
"atoms (insert (StatCh c A B (Msg M)) H) = set M ∪ atoms H"
by (auto elim!: atoms.cases)
lemma atoms_insert_DynCh [simp]:
"atoms (insert (DynCh c K (Msg M)) H) = set M ∪ atoms H"
by (auto elim!: atoms.cases)
subsection ‹Intruder knowledge (atoms)›
text ‹Atoms that the intruder can extract from a set of channel messages.›
inductive_set
extr :: "atom set ⇒ chmsg set ⇒ atom set"
for T :: "atom set"
and H :: "chmsg set"
where
extr_Inj: "At ∈ T ⟹ At ∈ extr T H"
| extr_StatCh:
"⟦ StatCh c A B (Msg M) ∈ H; At ∈ set M; confid ∉ c ∨ A ∈ bad ∨ B ∈ bad ⟧
⟹ At ∈ extr T H"
| extr_DynCh:
"⟦ DynCh c K (Msg M) ∈ H; At ∈ set M; confid ∉ c ∨ aKey K ∈ extr T H ⟧
⟹ At ∈ extr T H"
declare extr.intros [intro]
declare extr.cases [elim]
text‹Typical parameter describing initial intruder knowledge.›
definition
ik0 :: "atom set" where
"ik0 ≡ range aAgt ∪ range aNum ∪ aKey`corrKey"
lemma ik0_aAgt [iff]: "aAgt A ∈ ik0"
by (auto simp add: ik0_def)
lemma ik0_aNum [iff]: "aNum T ∈ ik0"
by (auto simp add: ik0_def)
lemma ik0_aNon [iff]: "aNon N ∉ ik0"
by (auto simp add: ik0_def)
lemma ik0_aKey_corr [simp]: "(aKey K ∈ ik0) = (K ∈ corrKey)"
by (auto simp add: ik0_def)
subsubsection ‹Basic lemmas›
lemma extr_empty [simp]: "extr T {} = T"
by (auto)
lemma extr_monotone [dest]: "G ⊆ H ⟹ extr T G ⊆ extr T H"
by (safe, erule extr.induct, auto)
lemmas extr_mono [elim] = extr_monotone [THEN [2] rev_subsetD]
lemma extr_monotone_param [dest]: "T ⊆ U ⟹ extr T H ⊆ extr U H"
by (safe, erule extr.induct, auto)
lemmas extr_mono_param [elim] = extr_monotone_param [THEN [2] rev_subsetD]
lemma extr_insert [intro]: "At ∈ extr T H ⟹ At ∈ extr T (insert C H)"
by (erule extr_mono) (auto)
lemma extr_into_atoms [dest]: "At ∈ extr T H ⟹ At ∈ T ∪ atoms H"
by (erule extr.induct, auto)
subsubsection ‹Insertion lemmas for atom parameters›
lemma extr_insert_non_key_param [simp]:
assumes "At ∈ range aNon ∪ range aAgt ∪ range aNum"
shows "extr (insert At T) H = insert At (extr T H)"
proof -
{ fix Bt
assume "Bt ∈ extr (insert At T) H"
hence "Bt ∈ insert At (extr T H)"
using assms by induct auto
}
thus ?thesis by auto
qed
lemma extr_insert_unused_key_param [simp]:
assumes "K ∉ keys_for H"
shows "extr (insert (aKey K) T) H = insert (aKey K) (extr T H)"
proof -
{ fix At
assume "At ∈ extr (insert (aKey K) T) H"
hence "At ∈ insert (aKey K) (extr T H)"
using assms by induct (auto simp add: keys_for_def)
}
thus ?thesis by auto
qed
subsubsection ‹Insertion lemmas for each type of channel message›
text ‹Note that the parameter accumulates the extracted atoms. In particular,
these may include keys that may open further dynamically confidential messages.
›
lemma extr_insert_StatCh [simp]:
"extr T (insert (StatCh c A B (Msg M)) H)
= (if confid ∉ c ∨ A ∈ bad ∨ B ∈ bad then extr (set M ∪ T) H else extr T H)"
proof (cases "confid ∉ c ∨ A ∈ bad ∨ B ∈ bad")
case True
moreover
{
fix At
assume "At ∈ extr T (insert (StatCh c A B (Msg M)) H)"
hence "At ∈ extr (set M ∪ T) H" by induct auto
}
moreover
{
fix At
assume "At ∈ extr (set M ∪ T) H"
and "confid ∉ c ∨ A ∈ bad ∨ B ∈ bad"
hence "At ∈ extr T (insert (StatCh c A B (Msg M)) H)" by induct auto
}
ultimately show ?thesis by auto
next
case False
moreover
{
fix At
assume "At ∈ extr T (insert (StatCh c A B (Msg M)) H)"
and "confid ∈ c" "A ∉ bad" "B ∉ bad"
hence "At ∈ extr T H" by induct auto
}
ultimately show ?thesis by auto
qed
lemma extr_insert_DynCh [simp]:
"extr T (insert (DynCh c K (Msg M)) H)
= (if confid ∉ c ∨ aKey K ∈ extr T H then extr (set M ∪ T) H else extr T H)"
proof (cases "confid ∉ c ∨ aKey K ∈ extr T H")
case True
moreover
{
fix At
assume "At ∈ extr T (insert (DynCh c K (Msg M)) H)"
hence "At ∈ extr (set M ∪ T) H" by induct auto
}
moreover
{
fix At
assume "At ∈ extr (set M ∪ T) H"
hence "At ∈ extr T (insert (DynCh c K (Msg M)) H)"
using True by induct auto
}
ultimately show ?thesis by auto
next
case False
moreover
hence "extr T (insert (DynCh c K (Msg M)) H) = extr T H"
by (intro equalityI subsetI) (erule extr.induct, auto)+
ultimately show ?thesis by auto
qed
declare extr.cases [rule del, elim]
subsection ‹Faking messages›
text ‹Channel messages that are fakeable from a given set of channel
messages. Parameters are a set of atoms and a set of freshness identifiers.
For faking messages on dynamic non-authentic channels, we cannot allow the
intruder to use arbitrary keys. Otherwise, we would lose the possibility to
generate fresh values in our model. Therefore, the chosen keys must correspond
to session keys associated with existing runs (i.e., from set
@{term "rkeys U"}).
›
abbreviation
rkeys :: "fid_t set ⇒ key set" where
"rkeys U ≡ sesK`(λ(x, y). x $ y)`(U × (UNIV::nat set))"
lemma rkeys_sesK [simp, dest]: "sesK (R$i) ∈ rkeys U ⟹ R ∈ U"
by (auto simp add: image_def)
inductive_set
fake :: "atom set ⇒ fid_t set ⇒ chmsg set ⇒ chmsg set"
for T :: "atom set"
and U :: "fid_t set"
and H :: "chmsg set"
where
fake_Inj:
"M ∈ H ⟹ M ∈ fake T U H"
| fake_StatCh:
"⟦ set M ⊆ extr T H; auth ∉ c ∨ A ∈ bad ∨ B ∈ bad ⟧
⟹ StatCh c A B (Msg M) ∈ fake T U H"
| fake_DynCh:
"⟦ set M ⊆ extr T H; auth ∉ c ∧ K ∈ rkeys U ∨ aKey K ∈ extr T H ⟧
⟹ DynCh c K (Msg M) ∈ fake T U H"
declare fake.cases [elim]
declare fake.intros [intro]
lemmas fake_intros = fake_StatCh fake_DynCh
lemma fake_expanding [intro]: "H ⊆ fake T U H"
by (auto)
lemma fake_monotone [intro]: "G ⊆ H ⟹ fake T U G ⊆ fake T U H"
by (safe, erule fake.cases, auto intro!: fake_intros)
lemma fake_monotone_param1 [intro]:
"T ⊆ T' ⟹ fake T U H ⊆ fake T' U H"
by (safe, erule fake.cases, auto intro!: fake_intros)
lemmas fake_mono [elim] = fake_monotone [THEN [2] rev_subsetD]
lemmas fake_mono_param1 [elim] = fake_monotone_param1 [THEN [2] rev_subsetD]
subsubsection ‹Atoms and extr together with fake›
lemma atoms_fake [simp]: "atoms (fake T U H) = T ∪ atoms H"
proof -
{
fix At
assume "At ∈ T"
hence "At ∈ atoms (fake T U H)"
proof -
{
fix A B
have "Insec A B (Msg [At]) ∈ fake T U H" using ‹At ∈ T›
by (intro fake_StatCh) (auto)
}
thus ?thesis by (intro at_StatCh) (auto)
qed
}
moreover
{
fix At
assume "At ∈ atoms (fake T U H) "
hence "At ∈ T ∪ atoms H" by cases blast+
}
ultimately show ?thesis by auto
qed
lemma extr_fake [simp]:
assumes "T' ⊆ T" shows "extr T (fake T' U H) = extr T H"
proof (intro equalityI subsetI)
fix At
assume "At ∈ extr T (fake T' U H)"
with assms have "At ∈ extr T (fake T U H)" by auto
thus "At ∈ extr T H" by induct auto
qed auto
end
Theory Message
section ‹Theory of Agents and Messages for Security Protocols›
theory Message imports Keys begin
lemma Un_idem_collapse [simp]: "A ∪ (B ∪ A) = B ∪ A"
by blast
datatype
msg = Agent agent
| Number nat
| Nonce nonce
| Key key
| Hash msg
| MPair msg msg
| Crypt key msg
text‹Concrete syntax: messages appear as ‹⦃A,B,NA⦄›, etc...›
syntax
"_MTuple" :: "['a, args] => 'a * 'b" ("(2⦃_,/ _⦄)")
translations
"⦃x, y, z⦄" == "⦃x, ⦃y, z⦄⦄"
"⦃x, y⦄" == "CONST MPair x y"
definition
HPair :: "[msg,msg] ⇒ msg" ("(4Hash[_] /_)" [0, 1000])
where
"Hash[X] Y ≡ ⦃Hash⦃X,Y⦄, Y⦄"
definition
keysFor :: "msg set ⇒ key set"
where
"keysFor H ≡ invKey ` {K. ∃X. Crypt K X ∈ H}"
subsubsection‹Inductive Definition of All Parts" of a Message›
inductive_set
parts :: "msg set => msg set"
for H :: "msg set"
where
Inj [intro]: "X ∈ H ==> X ∈ parts H"
| Fst: "⦃X,Y⦄ ∈ parts H ==> X ∈ parts H"
| Snd: "⦃X,Y⦄ ∈ parts H ==> Y ∈ parts H"
| Body: "Crypt K X ∈ parts H ==> X ∈ parts H"
text‹Monotonicity›
lemma parts_mono: "G ⊆ H ==> parts(G) ⊆ parts(H)"
apply auto
apply (erule parts.induct)
apply (blast dest: parts.Fst parts.Snd parts.Body)+
done
text‹Equations hold because constructors are injective.›
lemma Other_image_eq [simp]: "(Agent x ∈ Agent`A) = (x:A)"
by auto
lemma Key_image_eq [simp]: "(Key x ∈ Key`A) = (x∈A)"
by auto
lemma Nonce_Key_image_eq [simp]: "(Nonce x ∉ Key`A)"
by auto
subsection‹keysFor operator›
lemma keysFor_empty [simp]: "keysFor {} = {}"
by (unfold keysFor_def, blast)
lemma keysFor_Un [simp]: "keysFor (H ∪ H') = keysFor H ∪ keysFor H'"
by (unfold keysFor_def, blast)
lemma keysFor_UN [simp]: "keysFor (⋃i∈A. H i) = (⋃i∈A. keysFor (H i))"
by (unfold keysFor_def, blast)
text‹Monotonicity›
lemma keysFor_mono: "G ⊆ H ==> keysFor(G) ⊆ keysFor(H)"
by (unfold keysFor_def, blast)
lemma keysFor_insert_Agent [simp]: "keysFor (insert (Agent A) H) = keysFor H"
by (unfold keysFor_def, auto)
lemma keysFor_insert_Nonce [simp]: "keysFor (insert (Nonce N) H) = keysFor H"
by (unfold keysFor_def, auto)
lemma keysFor_insert_Number [simp]: "keysFor (insert (Number N) H) = keysFor H"
by (unfold keysFor_def, auto)
lemma keysFor_insert_Key [simp]: "keysFor (insert (Key K) H) = keysFor H"
by (unfold keysFor_def, auto)
lemma keysFor_insert_Hash [simp]: "keysFor (insert (Hash X) H) = keysFor H"
by (unfold keysFor_def, auto)
lemma keysFor_insert_MPair [simp]: "keysFor (insert ⦃X,Y⦄ H) = keysFor H"
by (unfold keysFor_def, auto)
lemma keysFor_insert_Crypt [simp]:
"keysFor (insert (Crypt K X) H) = insert (invKey K) (keysFor H)"
by (unfold keysFor_def, auto)
lemma keysFor_image_Key [simp]: "keysFor (Key`E) = {}"
by (unfold keysFor_def, auto)
lemma Crypt_imp_invKey_keysFor: "Crypt K X ∈ H ==> invKey K ∈ keysFor H"
by (unfold keysFor_def, blast)
subsection‹Inductive relation "parts"›
lemma MPair_parts:
"[| ⦃X,Y⦄ ∈ parts H;
[| X ∈ parts H; Y ∈ parts H |] ==> P |] ==> P"
by (blast dest: parts.Fst parts.Snd)
declare MPair_parts [elim!] parts.Body [dest!]
text‹NB These two rules are UNSAFE in the formal sense, as they discard the
compound message. They work well on THIS FILE.
‹MPair_parts› is left as SAFE because it speeds up proofs.
The Crypt rule is normally kept UNSAFE to avoid breaking up certificates.›
lemma parts_increasing: "H ⊆ parts(H)"
by blast
lemmas parts_insertI = subset_insertI [THEN parts_mono, THEN subsetD]
lemma parts_empty [simp]: "parts{} = {}"
apply safe
apply (erule parts.induct, blast+)
done
lemma parts_emptyE [elim!]: "X∈ parts{} ==> P"
by simp
text‹WARNING: loops if H = {Y}, therefore must not be repeated!›
lemma parts_singleton: "X∈ parts H ==> ∃Y∈H. X∈ parts {Y}"
by (erule parts.induct, fast+)
subsubsection‹Unions›
lemma parts_Un_subset1: "parts(G) ∪ parts(H) ⊆ parts(G ∪ H)"
by (intro Un_least parts_mono Un_upper1 Un_upper2)
lemma parts_Un_subset2: "parts(G ∪ H) ⊆ parts(G) ∪ parts(H)"
apply (rule subsetI)
apply (erule parts.induct, blast+)
done
lemma parts_Un [simp]: "parts(G ∪ H) = parts(G) ∪ parts(H)"
by (intro equalityI parts_Un_subset1 parts_Un_subset2)
lemma parts_insert: "parts (insert X H) = parts {X} ∪ parts H"
apply (subst insert_is_Un [of _ H])
apply (simp only: parts_Un)
done
text‹TWO inserts to avoid looping. This rewrite is better than nothing.
Not suitable for Addsimps: its behaviour can be strange.›
lemma parts_insert2:
"parts (insert X (insert Y H)) = parts {X} ∪ parts {Y} ∪ parts H"
apply (simp add: Un_assoc)
apply (simp add: parts_insert [symmetric])
done
lemma parts_UN_subset1: "(⋃x∈A. parts(H x)) ⊆ parts(⋃x∈A. H x)"
by (intro UN_least parts_mono UN_upper)
lemma parts_UN_subset2: "parts(⋃x∈A. H x) ⊆ (⋃x∈A. parts(H x))"
apply (rule subsetI)
apply (erule parts.induct, blast+)
done
lemma parts_UN [simp]: "parts(⋃x∈A. H x) = (⋃x∈A. parts(H x))"
by (intro equalityI parts_UN_subset1 parts_UN_subset2)
text‹Added to simplify arguments to parts, analz and synth.
NOTE: the UN versions are no longer used!›
text‹This allows ‹blast› to simplify occurrences of
@{term "parts(G∪H)"} in the assumption.›
lemmas in_parts_UnE = parts_Un [THEN equalityD1, THEN subsetD, THEN UnE]
declare in_parts_UnE [elim!]
lemma parts_insert_subset: "insert X (parts H) ⊆ parts(insert X H)"
by (blast intro: parts_mono [THEN [2] rev_subsetD])
subsubsection‹Idempotence and transitivity›
lemma parts_partsD [dest!]: "X∈ parts (parts H) ==> X∈ parts H"
by (erule parts.induct, blast+)
lemma parts_idem [simp]: "parts (parts H) = parts H"
by blast
lemma parts_subset_iff [simp]: "(parts G ⊆ parts H) = (G ⊆ parts H)"
apply (rule iffI)
apply (iprover intro: subset_trans parts_increasing)
apply (frule parts_mono, simp)
done
lemma parts_trans: "[| X∈ parts G; G ⊆ parts H |] ==> X∈ parts H"
by (drule parts_mono, blast)
text‹Cut›
lemma parts_cut:
"[| Y∈ parts (insert X G); X∈ parts H |] ==> Y∈ parts (G ∪ H)"
by (blast intro: parts_trans)
lemma parts_cut_eq [simp]: "X∈ parts H ==> parts (insert X H) = parts H"
by (force dest!: parts_cut intro: parts_insertI)
subsubsection‹Rewrite rules for pulling out atomic messages›
lemmas parts_insert_eq_I = equalityI [OF subsetI parts_insert_subset]
lemma parts_insert_Agent [simp]:
"parts (insert (Agent agt) H) = insert (Agent agt) (parts H)"
apply (rule parts_insert_eq_I)
apply (erule parts.induct, auto)
done
lemma parts_insert_Nonce [simp]:
"parts (insert (Nonce N) H) = insert (Nonce N) (parts H)"
apply (rule parts_insert_eq_I)
apply (erule parts.induct, auto)
done
lemma parts_insert_Number [simp]:
"parts (insert (Number N) H) = insert (Number N) (parts H)"
apply (rule parts_insert_eq_I)
apply (erule parts.induct, auto)
done
lemma parts_insert_Key [simp]:
"parts (insert (Key K) H) = insert (Key K) (parts H)"
apply (rule parts_insert_eq_I)
apply (erule parts.induct, auto)
done
lemma parts_insert_Hash [simp]:
"parts (insert (Hash X) H) = insert (Hash X) (parts H)"
apply (rule parts_insert_eq_I)
apply (erule parts.induct, auto)
done
lemma parts_insert_Crypt [simp]:
"parts (insert (Crypt K X) H) = insert (Crypt K X) (parts (insert X H))"
apply (rule equalityI)
apply (rule subsetI)
apply (erule parts.induct, auto)
apply (blast intro: parts.Body)
done
lemma parts_insert_MPair [simp]:
"parts (insert ⦃X,Y⦄ H) =
insert ⦃X,Y⦄ (parts (insert X (insert Y H)))"
apply (rule equalityI)
apply (rule subsetI)
apply (erule parts.induct, auto)
apply (blast intro: parts.Fst parts.Snd)+
done
lemma parts_image_Key [simp]: "parts (Key`N) = Key`N"
apply auto
apply (erule parts.induct, auto)
done
text‹In any message, there is an upper bound N on its greatest nonce.›
subsection‹Inductive relation "analz"›
text‹Inductive definition of "analz" -- what can be broken down from a set of
messages, including keys. A form of downward closure. Pairs can
be taken apart; messages decrypted with known keys.›
inductive_set
analz :: "msg set => msg set"
for H :: "msg set"
where
Inj [intro,simp] : "X ∈ H ==> X ∈ analz H"
| Fst: "⦃X,Y⦄ ∈ analz H ==> X ∈ analz H"
| Snd: "⦃X,Y⦄ ∈ analz H ==> Y ∈ analz H"
| Decrypt [dest]:
"[|Crypt K X ∈ analz H; Key(invKey K): analz H|] ==> X ∈ analz H"
text‹Monotonicity; Lemma 1 of Lowe's paper›
lemma analz_mono: "G⊆H ==> analz(G) ⊆ analz(H)"
apply auto
apply (erule analz.induct)
apply (auto dest: analz.Fst analz.Snd)
done
lemmas analz_monotonic = analz_mono [THEN [2] rev_subsetD]
text‹Making it safe speeds up proofs›
lemma MPair_analz [elim!]:
"[| ⦃X,Y⦄ ∈ analz H;
[| X ∈ analz H; Y ∈ analz H |] ==> P
|] ==> P"
by (blast dest: analz.Fst analz.Snd)
lemma analz_increasing: "H ⊆ analz(H)"
by blast
lemma analz_subset_parts: "analz H ⊆ parts H"
apply (rule subsetI)
apply (erule analz.induct, blast+)
done
lemmas analz_into_parts = analz_subset_parts [THEN subsetD]
lemmas not_parts_not_analz = analz_subset_parts [THEN contra_subsetD]
lemma parts_analz [simp]: "parts (analz H) = parts H"
apply (rule equalityI)
apply (rule analz_subset_parts [THEN parts_mono, THEN subset_trans], simp)
apply (blast intro: analz_increasing [THEN parts_mono, THEN subsetD])
done
lemma analz_parts [simp]: "analz (parts H) = parts H"
apply auto
apply (erule analz.induct, auto)
done
lemmas analz_insertI = subset_insertI [THEN analz_mono, THEN [2] rev_subsetD]
subsubsection‹General equational properties›
lemma analz_empty [simp]: "analz{} = {}"
apply safe
apply (erule analz.induct, blast+)
done
text‹Converse fails: we can analz more from the union than from the
separate parts, as a key in one might decrypt a message in the other›
lemma analz_Un: "analz(G) ∪ analz(H) ⊆ analz(G ∪ H)"
by (intro Un_least analz_mono Un_upper1 Un_upper2)
lemma analz_insert: "insert X (analz H) ⊆ analz(insert X H)"
by (blast intro: analz_mono [THEN [2] rev_subsetD])
subsubsection‹Rewrite rules for pulling out atomic messages›
lemmas analz_insert_eq_I = equalityI [OF subsetI analz_insert]
lemma analz_insert_Agent [simp]:
"analz (insert (Agent agt) H) = insert (Agent agt) (analz H)"
apply (rule analz_insert_eq_I)
apply (erule analz.induct, auto)
done
lemma analz_insert_Nonce [simp]:
"analz (insert (Nonce N) H) = insert (Nonce N) (analz H)"
apply (rule analz_insert_eq_I)
apply (erule analz.induct, auto)
done
lemma analz_insert_Number [simp]:
"analz (insert (Number N) H) = insert (Number N) (analz H)"
apply (rule analz_insert_eq_I)
apply (erule analz.induct, auto)
done
lemma analz_insert_Hash [simp]:
"analz (insert (Hash X) H) = insert (Hash X) (analz H)"
apply (rule analz_insert_eq_I)
apply (erule analz.induct, auto)
done
text‹Can only pull out Keys if they are not needed to decrypt the rest›
lemma analz_insert_Key [simp]:
"K ∉ keysFor (analz H) ==>
analz (insert (Key K) H) = insert (Key K) (analz H)"
apply (unfold keysFor_def)
apply (rule analz_insert_eq_I)
apply (erule analz.induct, auto)
done
lemma analz_insert_MPair [simp]:
"analz (insert ⦃X,Y⦄ H) =
insert ⦃X,Y⦄ (analz (insert X (insert Y H)))"
apply (rule equalityI)
apply (rule subsetI)
apply (erule analz.induct, auto)
apply (erule analz.induct)
apply (blast intro: analz.Fst analz.Snd)+
done
text‹Can pull out enCrypted message if the Key is not known›
lemma analz_insert_Crypt:
"Key (invKey K) ∉ analz H
==> analz (insert (Crypt K X) H) = insert (Crypt K X) (analz H)"
apply (rule analz_insert_eq_I)
apply (erule analz.induct, auto)
done
lemma lemma1: "Key (invKey K) ∈ analz H ==>
analz (insert (Crypt K X) H) ⊆
insert (Crypt K X) (analz (insert X H))"
apply (rule subsetI)
apply (erule_tac x = x in analz.induct, auto)
done
lemma lemma2: "Key (invKey K) ∈ analz H ==>
insert (Crypt K X) (analz (insert X H)) ⊆
analz (insert (Crypt K X) H)"
apply auto
apply (erule_tac x = x in analz.induct, auto)
apply (blast intro: analz_insertI analz.Decrypt)
done
lemma analz_insert_Decrypt:
"Key (invKey K) ∈ analz H ==>
analz (insert (Crypt K X) H) =
insert (Crypt K X) (analz (insert X H))"
by (intro equalityI lemma1 lemma2)
text‹Case analysis: either the message is secure, or it is not! Effective,
but can cause subgoals to blow up! Use with ‹split_if›; apparently
‹split_tac› does not cope with patterns such as @{term"analz (insert
(Crypt K X) H)"}›
lemma analz_Crypt_if [simp]:
"analz (insert (Crypt K X) H) =
(if (Key (invKey K) ∈ analz H)
then insert (Crypt K X) (analz (insert X H))
else insert (Crypt K X) (analz H))"
by (simp add: analz_insert_Crypt analz_insert_Decrypt)
text‹This rule supposes "for the sake of argument" that we have the key.›
lemma analz_insert_Crypt_subset:
"analz (insert (Crypt K X) H) ⊆
insert (Crypt K X) (analz (insert X H))"
apply (rule subsetI)
apply (erule analz.induct, auto)
done
lemma analz_image_Key [simp]: "analz (Key`N) = Key`N"
apply auto
apply (erule analz.induct, auto)
done
subsubsection‹Idempotence and transitivity›
lemma analz_analzD [dest!]: "X∈ analz (analz H) ==> X∈ analz H"
by (erule analz.induct, blast+)
lemma analz_idem [simp]: "analz (analz H) = analz H"
by blast
lemma analz_subset_iff [simp]: "(analz G ⊆ analz H) = (G ⊆ analz H)"
apply (rule iffI)
apply (iprover intro: subset_trans analz_increasing)
apply (frule analz_mono, simp)
done
lemma analz_trans: "[| X∈ analz G; G ⊆ analz H |] ==> X∈ analz H"
by (drule analz_mono, blast)
text‹Cut; Lemma 2 of Lowe›
lemma analz_cut: "[| Y∈ analz (insert X H); X∈ analz H |] ==> Y∈ analz H"
by (erule analz_trans, blast)
text‹This rewrite rule helps in the simplification of messages that involve
the forwarding of unknown components (X). Without it, removing occurrences
of X can be very complicated.›
lemma analz_insert_eq: "X∈ analz H ==> analz (insert X H) = analz H"
by (blast intro: analz_cut analz_insertI)
text‹A congruence rule for "analz"›
lemma analz_subset_cong:
"[| analz G ⊆ analz G'; analz H ⊆ analz H' |]
==> analz (G ∪ H) ⊆ analz (G' ∪ H')"
apply simp
apply (iprover intro: conjI subset_trans analz_mono Un_upper1 Un_upper2)
done
lemma analz_cong:
"[| analz G = analz G'; analz H = analz H' |]
==> analz (G ∪ H) = analz (G' ∪ H')"
by (intro equalityI analz_subset_cong, simp_all)
lemma analz_insert_cong:
"analz H = analz H' ==> analz(insert X H) = analz(insert X H')"
by (force simp only: insert_def intro!: analz_cong)
text‹If there are no pairs or encryptions then analz does nothing›
lemma analz_trivial:
"[| ∀X Y. ⦃X,Y⦄ ∉ H; ∀X K. Crypt K X ∉ H |] ==> analz H = H"
apply safe
apply (erule analz.induct, blast+)
done
text‹These two are obsolete (with a single Spy) but cost little to prove...›
lemma analz_UN_analz_lemma:
"X∈ analz (⋃i∈A. analz (H i)) ==> X∈ analz (⋃i∈A. H i)"
apply (erule analz.induct)
apply (blast intro: analz_mono [THEN [2] rev_subsetD])+
done
lemma analz_UN_analz [simp]: "analz (⋃i∈A. analz (H i)) = analz (⋃i∈A. H i)"
by (blast intro: analz_UN_analz_lemma analz_mono [THEN [2] rev_subsetD])
subsection‹Inductive relation "synth"›
text‹Inductive definition of "synth" -- what can be built up from a set of
messages. A form of upward closure. Pairs can be built, messages
encrypted with known keys. Agent names are public domain.
Numbers can be guessed, but Nonces cannot be.›
inductive_set
synth :: "msg set => msg set"
for H :: "msg set"
where
Inj [intro]: "X ∈ H ==> X ∈ synth H"
| Agent [intro]: "Agent agt ∈ synth H"
| Number [intro]: "Number n ∈ synth H"
| Hash [intro]: "X ∈ synth H ==> Hash X ∈ synth H"
| MPair [intro]: "[|X ∈ synth H; Y ∈ synth H|] ==> ⦃X,Y⦄ ∈ synth H"
| Crypt [intro]: "[|X ∈ synth H; Key(K) ∈ H|] ==> Crypt K X ∈ synth H"
text‹Monotonicity›
lemma synth_mono: "G⊆H ==> synth(G) ⊆ synth(H)"
by (auto, erule synth.induct, auto)
text‹NO ‹Agent_synth›, as any Agent name can be synthesized.
The same holds for @{term Number}›
inductive_cases Nonce_synth [elim!]: "Nonce n ∈ synth H"
inductive_cases Key_synth [elim!]: "Key K ∈ synth H"
inductive_cases Hash_synth [elim!]: "Hash X ∈ synth H"
inductive_cases MPair_synth [elim!]: "⦃X,Y⦄ ∈ synth H"
inductive_cases Crypt_synth [elim!]: "Crypt K X ∈ synth H"
lemma synth_increasing: "H ⊆ synth(H)"
by blast
subsubsection‹Unions›
text‹Converse fails: we can synth more from the union than from the
separate parts, building a compound message using elements of each.›
lemma synth_Un: "synth(G) ∪ synth(H) ⊆ synth(G ∪ H)"
by (intro Un_least synth_mono Un_upper1 Un_upper2)
lemma synth_insert: "insert X (synth H) ⊆ synth(insert X H)"
by (blast intro: synth_mono [THEN [2] rev_subsetD])
subsubsection‹Idempotence and transitivity›
lemma synth_synthD [dest!]: "X∈ synth (synth H) ==> X∈ synth H"
by (erule synth.induct, blast+)
lemma synth_idem: "synth (synth H) = synth H"
by blast
lemma synth_subset_iff [simp]: "(synth G ⊆ synth H) = (G ⊆ synth H)"
apply (rule iffI)
apply (iprover intro: subset_trans synth_increasing)
apply (frule synth_mono, simp add: synth_idem)
done
lemma synth_trans: "[| X∈ synth G; G ⊆ synth H |] ==> X∈ synth H"
by (drule synth_mono, blast)
text‹Cut; Lemma 2 of Lowe›
lemma synth_cut: "[| Y∈ synth (insert X H); X∈ synth H |] ==> Y∈ synth H"
by (erule synth_trans, blast)
lemma Agent_synth [simp]: "Agent A ∈ synth H"
by blast
lemma Number_synth [simp]: "Number n ∈ synth H"
by blast
lemma Nonce_synth_eq [simp]: "(Nonce N ∈ synth H) = (Nonce N ∈ H)"
by blast
lemma Key_synth_eq [simp]: "(Key K ∈ synth H) = (Key K ∈ H)"
by blast
lemma Crypt_synth_eq [simp]:
"Key K ∉ H ==> (Crypt K X ∈ synth H) = (Crypt K X ∈ H)"
by blast
lemma keysFor_synth [simp]:
"keysFor (synth H) = keysFor H ∪ invKey`{K. Key K ∈ H}"
by (unfold keysFor_def, blast)
subsubsection‹Combinations of parts, analz and synth›
lemma parts_synth [simp]: "parts (synth H) = parts H ∪ synth H"
apply (rule equalityI)
apply (rule subsetI)
apply (erule parts.induct)
apply (blast intro: synth_increasing [THEN parts_mono, THEN subsetD]
parts.Fst parts.Snd parts.Body)+
done
lemma analz_analz_Un [simp]: "analz (analz G ∪ H) = analz (G ∪ H)"
apply (intro equalityI analz_subset_cong)+
apply simp_all
done
lemma analz_synth_Un [simp]: "analz (synth G ∪ H) = analz (G ∪ H) ∪ synth G"
apply (rule equalityI)
apply (rule subsetI)
apply (erule analz.induct)
prefer 5 apply (blast intro: analz_mono [THEN [2] rev_subsetD])
apply (blast intro: analz.Fst analz.Snd analz.Decrypt)+
done
lemma analz_synth [simp]: "analz (synth H) = analz H ∪ synth H"
apply (cut_tac H = "{}" in analz_synth_Un)
apply (simp (no_asm_use))
done
text ‹chsp: added›
lemma analz_Un_analz [simp]: "analz (G ∪ analz H) = analz (G ∪ H)"
by (subst Un_commute, auto)+
lemma analz_synth_Un2 [simp]: "analz (G ∪ synth H) = analz (G ∪ H) ∪ synth H"
by (subst Un_commute, auto)+
subsubsection‹For reasoning about the Fake rule in traces›
lemma parts_insert_subset_Un: "X∈ G ==> parts(insert X H) ⊆ parts G ∪ parts H"
by (rule subset_trans [OF parts_mono parts_Un_subset2], blast)
text‹More specifically for Fake. Very occasionally we could do with a version
of the form @{term"parts{X} ⊆ synth (analz H) ∪ parts H"}›
lemma Fake_parts_insert:
"X ∈ synth (analz H) ==>
parts (insert X H) ⊆ synth (analz H) ∪ parts H"
apply (drule parts_insert_subset_Un)
apply (simp (no_asm_use))
apply blast
done
lemma Fake_parts_insert_in_Un:
"[|Z ∈ parts (insert X H); X ∈ synth (analz H)|]
==> Z ∈ synth (analz H) ∪ parts H"
by (blast dest: Fake_parts_insert [THEN subsetD, dest])
text‹@{term H} is sometimes @{term"Key ` KK ∪ spies evs"}, so can't put
@{term "G=H"}.›
lemma Fake_analz_insert:
"X∈ synth (analz G) ==>
analz (insert X H) ⊆ synth (analz G) ∪ analz (G ∪ H)"
apply (rule subsetI)
apply (subgoal_tac "x ∈ analz (synth (analz G) ∪ H) ")
prefer 2
apply (blast intro: analz_mono [THEN [2] rev_subsetD]
analz_mono [THEN synth_mono, THEN [2] rev_subsetD])
apply (simp (no_asm_use))
apply blast
done
lemma analz_conj_parts [simp]:
"(X ∈ analz H & X ∈ parts H) = (X ∈ analz H)"
by (blast intro: analz_subset_parts [THEN subsetD])
lemma analz_disj_parts [simp]:
"(X ∈ analz H | X ∈ parts H) = (X ∈ parts H)"
by (blast intro: analz_subset_parts [THEN subsetD])
text‹Without this equation, other rules for synth and analz would yield
redundant cases›
lemma MPair_synth_analz [iff]:
"(⦃X,Y⦄ ∈ synth (analz H)) =
(X ∈ synth (analz H) & Y ∈ synth (analz H))"
by blast
lemma Crypt_synth_analz:
"[| Key K ∈ analz H; Key (invKey K) ∈ analz H |]
==> (Crypt K X ∈ synth (analz H)) = (X ∈ synth (analz H))"
by blast
lemma Hash_synth_analz [simp]:
"X ∉ synth (analz H)
==> (Hash⦃X,Y⦄ ∈ synth (analz H)) = (Hash⦃X,Y⦄ ∈ analz H)"
by blast
subsection‹HPair: a combination of Hash and MPair›
subsubsection‹Freeness›
lemma Agent_neq_HPair: "Agent A ~= Hash[X] Y"
by (unfold HPair_def, simp)
lemma Nonce_neq_HPair: "Nonce N ~= Hash[X] Y"
by (unfold HPair_def, simp)
lemma Number_neq_HPair: "Number N ~= Hash[X] Y"
by (unfold HPair_def, simp)
lemma Key_neq_HPair: "Key K ~= Hash[X] Y"
by (unfold HPair_def, simp)
lemma Hash_neq_HPair: "Hash Z ~= Hash[X] Y"
by (unfold HPair_def, simp)
lemma Crypt_neq_HPair: "Crypt K X' ~= Hash[X] Y"
by (unfold HPair_def, simp)
lemmas HPair_neqs = Agent_neq_HPair Nonce_neq_HPair Number_neq_HPair
Key_neq_HPair Hash_neq_HPair Crypt_neq_HPair
declare HPair_neqs [iff]
declare HPair_neqs [symmetric, iff]
lemma HPair_eq [iff]: "(Hash[X'] Y' = Hash[X] Y) = (X' = X & Y'=Y)"
by (simp add: HPair_def)
lemma MPair_eq_HPair [iff]:
"(⦃X',Y'⦄ = Hash[X] Y) = (X' = Hash⦃X,Y⦄ & Y'=Y)"
by (simp add: HPair_def)
lemma HPair_eq_MPair [iff]:
"(Hash[X] Y = ⦃X',Y'⦄) = (X' = Hash⦃X,Y⦄ & Y'=Y)"
by (auto simp add: HPair_def)
subsubsection‹Specialized laws, proved in terms of those for Hash and MPair›
lemma keysFor_insert_HPair [simp]: "keysFor (insert (Hash[X] Y) H) = keysFor H"
by (simp add: HPair_def)
lemma parts_insert_HPair [simp]:
"parts (insert (Hash[X] Y) H) =
insert (Hash[X] Y) (insert (Hash⦃X,Y⦄) (parts (insert Y H)))"
by (simp add: HPair_def)
lemma analz_insert_HPair [simp]:
"analz (insert (Hash[X] Y) H) =
insert (Hash[X] Y) (insert (Hash⦃X,Y⦄) (analz (insert Y H)))"
by (simp add: HPair_def)
lemma HPair_synth_analz [simp]:
"X ∉ synth (analz H)
==> (Hash[X] Y ∈ synth (analz H)) =
(Hash⦃X, Y⦄ ∈ analz H & Y ∈ synth (analz H))"
by (simp add: HPair_def)
text‹We do NOT want Crypt... messages broken up in protocols!!›
declare parts.Body [rule del]
text‹Rewrites to push in Key and Crypt messages, so that other messages can
be pulled out using the ‹analz_insert› rules›
lemmas pushKeys =
insert_commute [of "Key K" "Agent C" for K C]
insert_commute [of "Key K" "Nonce N" for K N]
insert_commute [of "Key K" "Number N" for K N]
insert_commute [of "Key K" "Hash X" for K X]
insert_commute [of "Key K" "MPair X Y" for K X Y]
insert_commute [of "Key K" "Crypt X K'" for K K' X]
lemmas pushCrypts =
insert_commute [of "Crypt X K" "Agent C" for X K C]
insert_commute [of "Crypt X K" "Agent C" for X K C]
insert_commute [of "Crypt X K" "Nonce N" for X K N]
insert_commute [of "Crypt X K" "Number N" for X K N]
insert_commute [of "Crypt X K" "Hash X'" for X K X']
insert_commute [of "Crypt X K" "MPair X' Y" for X K X' Y]
text‹Cannot be added with ‹[simp]› -- messages should not always be
re-ordered.›
lemmas pushes = pushKeys pushCrypts
text‹By default only ‹o_apply› is built-in. But in the presence of
eta-expansion this means that some terms displayed as @{term "f o g"} will be
rewritten, and others will not!›
declare o_def [simp]
lemma Crypt_notin_image_Key [simp]: "Crypt K X ∉ Key ` A"
by auto
lemma Hash_notin_image_Key [simp] :"Hash X ∉ Key ` A"
by auto
lemma synth_analz_mono: "G⊆H ==> synth (analz(G)) ⊆ synth (analz(H))"
by (iprover intro: synth_mono analz_mono)
lemma Fake_analz_eq [simp]:
"X ∈ synth(analz H) ==> synth (analz (insert X H)) = synth (analz H)"
apply (drule Fake_analz_insert[of _ _ "H"])
apply (simp add: synth_increasing[THEN Un_absorb2])
apply (drule synth_mono)
apply (simp add: synth_idem)
apply (rule equalityI)
apply (simp add: )
apply (rule synth_analz_mono, blast)
done
text‹Two generalizations of ‹analz_insert_eq››
lemma gen_analz_insert_eq [rule_format]:
"X ∈ analz H ==> ALL G. H ⊆ G --> analz (insert X G) = analz G"
by (blast intro: analz_cut analz_insertI analz_mono [THEN [2] rev_subsetD])
lemma synth_analz_insert_eq [rule_format]:
"X ∈ synth (analz H)
==> ALL G. H ⊆ G --> (Key K ∈ analz (insert X G)) = (Key K ∈ analz G)"
apply (erule synth.induct)
apply (simp_all add: gen_analz_insert_eq subset_trans [OF _ subset_insertI])
done
lemma Fake_parts_sing:
"X ∈ synth (analz H) ==> parts{X} ⊆ synth (analz H) ∪ parts H"
apply (rule subset_trans)
apply (erule_tac [2] Fake_parts_insert)
apply (rule parts_mono, blast)
done
lemmas Fake_parts_sing_imp_Un = Fake_parts_sing [THEN [2] rev_subsetD]
text‹For some reason, moving this up can make some proofs loop!›
declare invKey_K [simp]
end
Theory s0g_secrecy
section ‹Secrecy with Leaking (global version)›
theory s0g_secrecy imports Refinement Agents
begin
text ‹This model extends the global secrecy model by adding a ‹leak›
event, which models that the adversary can learn messages through leaks of
some (unspecified) kind.›
text ‹Proof tool configuration. Avoid annoying automatic unfolding of
‹dom›.›
declare domIff [simp, iff del]
subsection ‹State›
text ‹The only state variable is a knowledge relation, an authorization
relation, and a leakage relation.
@{term "(d, A) ∈ kn s"} means that the agent @{term "A"} knows data @{term "d"}.
@{term "(d, A) ∈ az s"} means that the agent @{term "A"} is authorized to
know data @{term "d"}.
@{term "(d, A) ∈ lk s"} means that data @{term "d"} has leaked to agent
@{term "A"}. Leakage models potential unauthorized knowledge.
›
record 'd s0g_state =
kn :: "('d × agent) set"
az :: "('d × agent) set"
lk :: "'d set"
type_synonym
'd s0g_obs = "'d s0g_state"
abbreviation
"lkr s ≡ lk s × UNIV"
subsection ‹Invariant definitions›
text ‹Global secrecy is stated as an invariant.›
definition
s0g_secrecy :: "'d s0g_state set"
where
"s0g_secrecy ≡ {s. kn s ⊆ az s ∪ lkr s}"
lemmas s0g_secrecyI = s0g_secrecy_def [THEN setc_def_to_intro, rule_format]
lemmas s0g_secrecyE [elim] =
s0g_secrecy_def [THEN setc_def_to_elim, rule_format]
text ‹Data that someone is authorized to know and leaked data is known
by someone.›
definition
s0g_dom :: "'d s0g_state set"
where
"s0g_dom ≡ {s. Domain (az s ∪ lkr s) ⊆ Domain (kn s)}"
lemmas s0g_domI = s0g_dom_def [THEN setc_def_to_intro, rule_format]
lemmas s0g_domE [elim] = s0g_dom_def [THEN setc_def_to_elim, rule_format]
subsection ‹Events›
text ‹New secrets may be generated anytime.›
definition
s0g_gen :: "['d, agent, agent set] ⇒ ('d s0g_state × 'd s0g_state) set"
where
"s0g_gen d A G ≡ {(s, s1).
A ∈ G ∧
d ∉ Domain (kn s) ∧
s1 = s⦇
kn := insert (d, A) (kn s),
az := az s ∪ {d} × (if G ∩ bad = {} then G else UNIV)
⦈
}"
text ‹Learning secrets.›
definition
s0g_learn ::
"['d, agent] ⇒ ('d s0g_state × 'd s0g_state) set"
where
"s0g_learn d B ≡ {(s, s1).
(d, B) ∈ az s ∪ lkr s ∧
s1 = s⦇ kn := insert (d, B) (kn s) ⦈
}"
text ‹Leaking secrets.›
definition
s0g_leak ::
"'d ⇒ ('d s0g_state × 'd s0g_state) set"
where
"s0g_leak d ≡ {(s, s1).
d ∈ Domain (kn s) ∧
s1 = s⦇ lk := insert d (lk s) ⦈
}"
subsection ‹Specification›
definition
s0g_init :: "'d s0g_state set"
where
"s0g_init ≡ s0g_secrecy ∩ s0g_dom"
definition
s0g_trans :: "('d s0g_state × 'd s0g_state) set" where
"s0g_trans ≡ (⋃d A B G.
s0g_gen d A G ∪
s0g_learn d B ∪
s0g_leak d ∪
Id
)"
definition
s0g :: "('d s0g_state, 'd s0g_obs) spec" where
"s0g ≡ ⦇
init = s0g_init,
trans = s0g_trans,
obs = id
⦈"
lemmas s0g_defs =
s0g_def s0g_init_def s0g_trans_def
s0g_gen_def s0g_learn_def s0g_leak_def
lemma s0g_obs_id [simp]: "obs s0g = id"
by (simp add: s0g_def)
text ‹All state predicates are trivially observable.›
lemma s0g_anyP_observable [iff]: "observable (obs s0g) P"
by (auto)
subsection ‹Invariant proofs›
subsection ‹inv1: Secrecy›
lemma PO_s0g_secrecy_init [iff]:
"init s0g ⊆ s0g_secrecy"
by (auto simp add: s0g_defs intro!: s0g_secrecyI)
lemma PO_s0g_secrecy_trans [iff]:
"{s0g_secrecy} trans s0g {> s0g_secrecy}"
apply (auto simp add: s0g_defs PO_hoare_defs intro!: s0g_secrecyI)
apply (auto)
done
lemma PO_s0g_secrecy [iff]:"reach s0g ⊆ s0g_secrecy"
by (rule inv_rule_basic, auto)
text ‹As en external invariant.›
lemma PO_s0g_obs_secrecy [iff]:"oreach s0g ⊆ s0g_secrecy"
by (rule external_from_internal_invariant) (auto del: subsetI)
subsection ‹inv2: Authorized and leaked data is known to someone›
lemma PO_s0g_dom_init [iff]:
"init s0g ⊆ s0g_dom"
by (auto simp add: s0g_defs intro!: s0g_domI)
lemma PO_s0g_dom_trans [iff]:
"{s0g_dom} trans s0g {> s0g_dom}"
apply (auto simp add: s0g_defs PO_hoare_defs intro!: s0g_domI)
apply (blast)+
done
lemma PO_s0g_dom [iff]: "reach s0g ⊆ s0g_dom"
by (rule inv_rule_basic, auto)
text ‹As en external invariant.›
lemma PO_s0g_obs_dom [iff]: "oreach s0g ⊆ s0g_dom"
by (rule external_from_internal_invariant) (auto del: subsetI)
end
Theory a0n_agree
section ‹Non-injective Agreement›
theory a0n_agree imports Refinement Agents
begin
text ‹The initial model abstractly specifies entity authentication, where
one agent/role authenticates another. More precisely, this property corresponds
to non-injective agreement on a data set ‹ds›. We use Running and Commit
signals to obtain a protocol-independent extensional specification.›
text ‹Proof tool configuration. Avoid annoying automatic unfolding of
‹dom›.›
declare domIff [simp, iff del]
subsection ‹State›
text ‹Signals. At this stage there are no protocol runs yet. All we model
are the signals that indicate a certain progress of a protocol run by one
agent/role (Commit signal) and the other role (Running signal). The signals
contain a list of agents that are assumed to be honest and a polymorphic data
set to be agreed upon, which is instantiated later.
Usually, the agent list will contain the names of the two agents who want to
agree on the data, but sometimes one of the agents is honest by assumption
(e.g., the server) or the honesty of additional agents needs to be assumed
for the agreement to hold.›
datatype 'ds signal =
Running "agent list" "'ds"
| Commit "agent list" "'ds"
record 'ds a0n_state =
signals :: "'ds signal ⇒ nat"
corrupted :: "'ds set"
type_synonym
'ds a0n_obs = "'ds a0n_state"
subsection ‹Events›
definition
a0n_init :: "'ds a0n_state set"
where
"a0n_init ≡ {s. ∃ds. s = ⦇
signals = λs. 0,
corrupted = ds
⦈ }"
text ‹Running signal, indicating end of responder run.›
definition
a0n_running :: "[agent list, 'ds] ⇒ ('ds a0n_state × 'ds a0n_state) set"
where
"a0n_running h d ≡ {(s, s').
s' = s⦇
signals := (signals s)(Running h d := signals s (Running h d) + 1)
⦈
}"
text ‹Commit signal, marking end of initiator run.›
definition
a0n_commit :: "[agent list, 'ds] ⇒ ('ds a0n_state × 'ds a0n_state) set"
where
"a0n_commit h d ≡ {(s, s').
(set h ⊆ good ⟶ d ∉ corrupted s ⟶ signals s (Running h d) > 0) ∧
s' = s⦇
signals := (signals s)(Commit h d := signals s (Commit h d) + 1)
⦈
}"
text ‹Data corruption.›
definition
a0n_corrupt :: "'ds set ⇒ ('ds a0n_state × 'ds a0n_state) set"
where
"a0n_corrupt ds ≡ {(s, s').
s' = s⦇
corrupted := corrupted s ∪ ds
⦈
}"
text ‹Transition system.›
definition
a0n_trans :: "('ds a0n_state × 'ds a0n_state) set" where
"a0n_trans ≡ (⋃h d ds.
a0n_running h d ∪
a0n_commit h d ∪
a0n_corrupt ds ∪
Id
)"
definition
a0n :: "('ds a0n_state, 'ds a0n_obs) spec" where
"a0n ≡ ⦇
init = a0n_init,
trans = a0n_trans,
obs = id
⦈"
lemmas a0n_defs =
a0n_def a0n_init_def a0n_trans_def
a0n_running_def a0n_commit_def a0n_corrupt_def
text ‹Any property is trivially observable.›
lemma a0n_obs [simp]: "obs a0n= id"
by (simp add: a0n_def)
lemma a0n_anyP_observable [iff]: "observable (obs a0n) P"
by (auto)
subsection ‹Invariants›
subsection ‹inv1: non-injective agreement›
text ‹This is an extensional variant of Lowe's \emph{non-injective agreement}
of the first with the second agent (by convention) in ‹h› on data
‹d› [Lowe97].
›
definition
a0n_inv1_niagree :: "'ds a0n_state set"
where
"a0n_inv1_niagree ≡ {s. ∀h d.
set h ⊆ good ⟶ d ∉ corrupted s ⟶
signals s (Commit h d) > 0 ⟶ signals s (Running h d) > 0
}"
lemmas a0n_inv1_niagreeI =
a0n_inv1_niagree_def [THEN setc_def_to_intro, rule_format]
lemmas a0n_inv1_niagreeE [elim] =
a0n_inv1_niagree_def [THEN setc_def_to_elim, rule_format]
lemmas a0n_inv1_niagreeD =
a0n_inv1_niagree_def [THEN setc_def_to_dest, rule_format, rotated 2]
text ‹Invariance proof.›
lemma PO_a0n_inv1_niagree_init [iff]:
"init a0n ⊆ a0n_inv1_niagree"
by (auto simp add: a0n_defs intro!: a0n_inv1_niagreeI)
lemma PO_a0n_inv1_niagree_trans [iff]:
"{a0n_inv1_niagree} trans a0n {> a0n_inv1_niagree}"
apply (auto simp add: PO_hoare_defs a0n_defs intro!: a0n_inv1_niagreeI)
apply (auto dest!: a0n_inv1_niagreeD dest: dom_lemmas)
done
lemma PO_a0n_inv1_niagree [iff]: "reach a0n ⊆ a0n_inv1_niagree"
by (rule inv_rule_basic) (auto)
text ‹This is also an external invariant.›
lemma a0n_obs_inv1_niagree [iff]:
"oreach a0n ⊆ a0n_inv1_niagree"
apply (rule external_from_internal_invariant, fast)
apply (subst a0n_def, auto)
done
end
Theory a0i_agree
section ‹Injective Agreement›
theory a0i_agree imports a0n_agree
begin
text ‹This refinement adds injectiveness to the agreement property.›
subsection ‹State›
text ‹The state and observations are the same as in the previous model.›
type_synonym
'd a0i_state = "'d a0n_state"
type_synonym
'd a0i_obs = "'d a0n_obs"
subsection ‹Events›
text ‹We just refine the commit event. Everything else remains the same.›
abbreviation
a0i_init :: "'ds a0n_state set"
where
"a0i_init ≡ a0n_init"
abbreviation
a0i_running :: "[agent list, 'ds] ⇒ ('ds a0i_state × 'ds a0i_state) set"
where
"a0i_running ≡ a0n_running"
definition
a0i_commit ::
"[agent list, 'ds] ⇒ ('ds a0i_state × 'ds a0i_state) set"
where
"a0i_commit h d ≡ {(s, s').
(set h ⊆ good ⟶ d ∉ corrupted s ⟶
signals s (Commit h d) < signals s (Running h d)) ∧
s' = s⦇
signals := (signals s)(Commit h d := signals s (Commit h d) + 1)
⦈
}"
abbreviation
a0i_corrupt :: "'ds set ⇒ ('ds a0i_state × 'ds a0i_state) set"
where
"a0i_corrupt ≡ a0n_corrupt"
text ‹Transition system.›
definition
a0i_trans :: "('ds a0i_state × 'ds a0i_state) set" where
"a0i_trans ≡ (⋃ h d ds.
a0i_running h d ∪
a0i_commit h d ∪
a0i_corrupt ds ∪
Id
)"
definition
a0i :: "('ds a0i_state, 'ds a0i_obs) spec" where
"a0i ≡ ⦇
init = a0i_init,
trans = a0i_trans,
obs = id
⦈"
lemmas a0i_defs =
a0n_defs a0i_def a0i_trans_def a0i_commit_def
text ‹Any property is trivially observable.›
lemma a0i_obs [simp]: "obs a0i = id"
by (simp add: a0i_def)
lemma a0i_anyP_observable [iff]: "observable (obs a0i) P"
by (auto)
subsection ‹Invariants›
subsubsection ‹Injective agreement.›
definition
a0i_inv1_iagree :: "'ds a0i_state set"
where
"a0i_inv1_iagree ≡ {s. ∀h d.
set h ⊆ good ⟶ d ∉ corrupted s ⟶
signals s (Commit h d) ≤ signals s (Running h d)
}"
lemmas a0i_inv1_iagreeI =
a0i_inv1_iagree_def [THEN setc_def_to_intro, rule_format]
lemmas a0i_inv1_iagreeE [elim] =
a0i_inv1_iagree_def [THEN setc_def_to_elim, rule_format]
lemmas a0i_inv1_iagreeD =
a0i_inv1_iagree_def [THEN setc_def_to_dest, rule_format, rotated 1]
lemma PO_a0i_inv1_iagree_init [iff]:
"init a0i ⊆ a0i_inv1_iagree"
by (auto simp add: a0i_defs intro!: a0i_inv1_iagreeI)
lemma PO_a0i_inv1_iagree_trans [iff]:
"{a0i_inv1_iagree} trans a0i {> a0i_inv1_iagree}"
apply (auto simp add: PO_hoare_defs a0i_defs intro!: a0i_inv1_iagreeI)
apply (auto dest: a0i_inv1_iagreeD intro: le_SucI)
done
lemma PO_a0i_inv1_iagree [iff]: "reach a0i ⊆ a0i_inv1_iagree"
by (rule inv_rule_basic) (auto)
text ‹As an external invariant.›
lemma PO_a0i_obs_inv1_iagree [iff]: "oreach a0i ⊆ a0i_inv1_iagree"
apply (rule external_from_internal_invariant, fast)
apply (subst a0i_def, auto)
done
subsection ‹Refinement›
definition
med0n0i :: "'d a0i_obs ⇒ 'd a0i_obs"
where
"med0n0i ≡ id"
definition
R0n0i :: "('d a0n_state × 'd a0i_state) set"
where
"R0n0i ≡ Id"
lemma PO_a0i_running_refines_a0n_running:
"{R0n0i}
(a0n_running h d), (a0i_running h d)
{> R0n0i}"
by (unfold R0n0i_def) (rule relhoare_refl)
lemma PO_a0i_commit_refines_a0n_commit:
"{R0n0i}
(a0n_commit h d), (a0i_commit h d)
{> R0n0i}"
by (auto simp add: PO_rhoare_defs R0n0i_def a0i_defs)
lemma PO_a0i_corrupt_refines_a0n_corrupt:
"{R0n0i}
(a0n_corrupt d), (a0i_corrupt d)
{> R0n0i}"
by (unfold R0n0i_def) (rule relhoare_refl)
lemmas PO_a0i_trans_refines_a0n_trans =
PO_a0i_running_refines_a0n_running
PO_a0i_commit_refines_a0n_commit
PO_a0i_corrupt_refines_a0n_corrupt
text ‹All together now...›
lemma PO_m1_refines_init_a0n [iff]:
"init a0i ⊆ R0n0i``(init a0n)"
by (auto simp add: R0n0i_def a0i_defs)
lemma PO_m1_refines_trans_a0n [iff]:
"{R0n0i}
(trans a0n), (trans a0i)
{> R0n0i}"
by (auto simp add: a0n_def a0n_trans_def a0i_def a0i_trans_def
intro!: PO_a0i_trans_refines_a0n_trans)
lemma PO_obs_consistent [iff]:
"obs_consistent R0n0i med0n0i a0n a0i"
by (auto simp add: obs_consistent_def R0n0i_def med0n0i_def a0i_def a0n_def)
lemma PO_a0i_refines_a0n:
"refines R0n0i med0n0i a0n a0i"
by (rule Refinement_basic) (auto)
subsection ‹Derived invariants›
lemma iagree_implies_niagree [iff]: "a0i_inv1_iagree ⊆ a0n_inv1_niagree"
apply (auto intro!: a0n_inv1_niagreeI)
apply (drule_tac d=d in a0i_inv1_iagreeD, auto)
done
text ‹Non-injective agreeement as internal and external invariants.›
lemma PO_a0i_a0n_inv1_niagree [iff]: "reach a0i ⊆ a0n_inv1_niagree"
by (rule subset_trans, rule, rule)
lemma PO_a0i_obs_a0n_inv1_niagree [iff]: "oreach a0i ⊆ a0n_inv1_niagree"
by (rule subset_trans, rule, rule)
end
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
Theory m2_auth_chan
section ‹Refinement 2a: Authentic Channel Protocol›
theory m2_auth_chan imports m1_auth "../Refinement/Channels"
begin
text ‹We refine the abstract authentication protocol to a version of the
ISO/IEC 9798-3 protocol using abstract channels. In standard protocol notation,
the original protocol is specified as follows.
\[
\begin{array}{llll}
\mathrm{M1.} & A \rightarrow B & : & A, B, N_A \\
\mathrm{M2.} & B \rightarrow A & : & \{N_B, N_A, A\}_{K^{-1}(B)}
\end{array}
\]
We introduce insecure channels between pairs of agents for the first message and
authentic channels for the second.›
declare domIff [simp, iff del]
subsection ‹State›
text ‹State: we extend the state with insecure and authentic channels
defined above.›
record m2_state = m1_state +
chan :: "chmsg set"
text ‹Observations.›
type_synonym
m2_obs = m1_state
definition
m2_obs :: "m2_state ⇒ m2_obs" where
"m2_obs s ≡ ⦇
runs = runs s
⦈"
subsection ‹Events›
definition
m2_step1 :: "[rid_t, agent, agent, nonce] ⇒ (m2_state × m2_state) set"
where
"m2_step1 Ra A B Na ≡ {(s, s1).
Ra ∉ dom (runs s) ∧
Na = Ra$0 ∧
s1 = s⦇
runs := (runs s)(Ra ↦ (Init, [A, B], [])),
chan := insert (Insec A B (Msg [aNon Na])) (chan s)
⦈
}"
definition
m2_step2 :: "[rid_t, agent, agent, nonce, nonce] ⇒ (m2_state × m2_state) set"
where
"m2_step2 Rb A B Na Nb ≡ {(s, s1).
Rb ∉ dom (runs s) ∧
Nb = Rb$0 ∧
Insec A B (Msg [aNon Na]) ∈ chan s ∧
s1 = s⦇
runs := (runs s)(Rb ↦ (Resp, [A, B], [aNon Na])),
chan := insert (Auth B A (Msg [aNon Nb, aNon Na])) (chan s)
⦈
}"
definition
m2_step3 :: "[rid_t, agent, agent, nonce, nonce] ⇒ (m2_state × m2_state) set"
where
"m2_step3 Ra A B Na Nb ≡ {(s, s1).
runs s Ra = Some (Init, [A, B], []) ∧
Na = Ra$0 ∧
Auth B A (Msg [aNon Nb, aNon Na]) ∈ chan s ∧
s1 = s⦇
runs := (runs s)(Ra ↦ (Init, [A, B], [aNon Nb]))
⦈
}"
text ‹Intruder fake event.›
definition
m2_fake :: "(m2_state × m2_state) set"
where
"m2_fake ≡ {(s, s1).
s1 = s⦇ chan := fake ik0 (dom (runs s)) (chan s) ⦈
}"
text ‹Transition system.›
definition
m2_init :: "m2_state set"
where
"m2_init ≡ { ⦇
runs = Map.empty,
chan = {}
⦈ }"
definition
m2_trans :: "(m2_state × m2_state) set" where
"m2_trans ≡ (⋃A B Ra Rb Na Nb.
(m2_step1 Ra A B Na) ∪
(m2_step2 Rb A B Na Nb) ∪
(m2_step3 Ra A B Na Nb) ∪
m2_fake ∪
Id
)"
definition
m2 :: "(m2_state, m2_obs) spec" where
"m2 ≡ ⦇
init = m2_init,
trans = m2_trans,
obs = m2_obs
⦈"
lemmas m2_defs =
m2_def m2_init_def m2_trans_def m2_obs_def
m2_step1_def m2_step2_def m2_step3_def m2_fake_def
subsection ‹Invariants›
subsubsection ‹Authentic channel and responder›
text ‹This property relates the messages in the authentic channel to the
responder run frame.›
definition
m2_inv1_auth :: "m2_state set" where
"m2_inv1_auth ≡ {s. ∀A B Na Nb.
Auth B A (Msg [aNon Nb, aNon Na]) ∈ chan s ⟶ B ∉ bad ⟶ A ∉ bad ⟶
(∃Rb. runs s Rb = Some (Resp, [A, B], [aNon Na]) ∧ Nb = Rb$0)
}"
lemmas m2_inv1_authI =
m2_inv1_auth_def [THEN setc_def_to_intro, rule_format]
lemmas m2_inv1_authE [elim] =
m2_inv1_auth_def [THEN setc_def_to_elim, rule_format]
lemmas m2_inv1_authD [dest] =
m2_inv1_auth_def [THEN setc_def_to_dest, rule_format, rotated 1]
text ‹Invariance proof.›
lemma PO_m2_inv2_init [iff]:
"init m2 ⊆ m2_inv1_auth"
by (auto simp add: PO_hoare_def m2_defs intro!: m2_inv1_authI)
lemma PO_m2_inv2_trans [iff]:
"{m2_inv1_auth} trans m2 {> m2_inv1_auth}"
apply (auto simp add: PO_hoare_def m2_defs intro!: m2_inv1_authI)
apply (auto dest: dom_lemmas)
apply (force)
done
lemma PO_m2_inv2 [iff]: "reach m2 ⊆ m2_inv1_auth"
by (rule_tac inv_rule_incr) (auto)
subsection ‹Refinement›
text ‹Simulation relation and mediator function. This is a pure superposition
refinement.›
definition
R12 :: "(m1_state × m2_state) set" where
"R12 ≡ {(s, t). runs s = runs t}"
definition
med21 :: "m2_obs ⇒ m1_obs" where
"med21 ≡ id"
text ‹Refinement proof›
lemma PO_m2_step1_refines_m1_step1:
"{R12}
(m1_step1 Ra A B Na), (m2_step1 Ra A B Na)
{> R12}"
by (auto simp add: PO_rhoare_defs R12_def m1_defs m2_defs)
lemma PO_m2_step2_refines_m1_step2:
"{R12}
(m1_step2 Ra A B Na Nb), (m2_step2 Ra A B Na Nb)
{> R12}"
by (auto simp add: PO_rhoare_defs R12_def m1_defs m2_defs)
lemma PO_m2_step3_refines_m1_step3:
"{R12 ∩ UNIV × m2_inv1_auth}
(m1_step3 Ra A B Na Nb), (m2_step3 Ra A B Na Nb)
{> R12}"
by (auto simp add: PO_rhoare_defs R12_def m1_defs m2_defs)
text ‹New fake event refines skip.›
lemma PO_m2_fake_refines_m1_skip:
"{R12} Id, m2_fake {> R12}"
by (auto simp add: PO_rhoare_defs R12_def m1_defs m2_defs)
lemmas PO_m2_trans_refines_m1_trans =
PO_m2_step1_refines_m1_step1 PO_m2_step2_refines_m1_step2
PO_m2_step3_refines_m1_step3 PO_m2_fake_refines_m1_skip
text ‹All together now...›
lemma PO_m2_refines_init_m1 [iff]:
"init m2 ⊆ R12``(init m1)"
by (auto simp add: R12_def m1_defs m2_defs)
lemma PO_m2_refines_trans_m1 [iff]:
"{R12 ∩ UNIV × m2_inv1_auth}
(trans m1), (trans m2)
{> R12}"
apply (auto simp add: m2_def m2_trans_def m1_def m1_trans_def)
apply (blast intro!: PO_m2_trans_refines_m1_trans)+
done
lemma PO_obs_consistent [iff]:
"obs_consistent R12 med21 m1 m2"
by (auto simp add: obs_consistent_def R12_def med21_def m1_defs m2_defs)
lemma m2_refines_m1:
"refines
(R12 ∩ UNIV × m2_inv1_auth)
med21 m1 m2"
by (rule Refinement_using_invariants) (auto)
end
Theory m2_confid_chan
section ‹Refinement 2b: Confidential Channel Protocol›
theory m2_confid_chan imports m1_auth "../Refinement/Channels"
begin
text ‹We refine the abstract authentication protocol to the first two
steps of the Needham-Schroeder-Lowe protocol, which we call NSL/2.
In standard protocol notation, the original protocol is specified as follows.
\[
\begin{array}{llll}
\mathrm{M1.} & A \rightarrow B & : & \{N_A, A\}_{K(B)} \\
\mathrm{M2.} & B \rightarrow A & : & \{N_A, N_B, B\}_{K(A)}
\end{array}
\]
At this refinement level, we abstract the encrypted messages to
non-cryptographic messages transmitted on confidential channels.›
declare domIff [simp, iff del]
subsection ‹State and observations›
record m2_state = m1_state +
chan :: "chmsg set"
type_synonym
m2_obs = m1_state
definition
m2_obs :: "m2_state ⇒ m2_obs" where
"m2_obs s ≡ ⦇
runs = runs s
⦈"
subsection ‹Events›
definition
m2_init :: "m2_state set"
where
"m2_init ≡ { ⦇
runs = Map.empty,
chan = {}
⦈ }"
definition
m2_step1 :: "[rid_t, agent, agent, nonce] ⇒ (m2_state × m2_state) set"
where
"m2_step1 Ra A B Na ≡ {(s, s1).
Ra ∉ dom (runs s) ∧
Na = Ra$0 ∧
s1 = s⦇
runs := (runs s)(Ra ↦ (Init, [A, B], [])),
chan := insert (Confid A B (Msg [aNon Na])) (chan s)
⦈
}"
definition
m2_step2 :: "[rid_t, agent, agent, nonce, nonce] ⇒ (m2_state × m2_state) set"
where
"m2_step2 Rb A B Na Nb ≡ {(s, s1).
Rb ∉ dom (runs s) ∧
Nb = Rb$0 ∧
Confid A B (Msg [aNon Na]) ∈ chan s ∧
s1 = s⦇
runs := (runs s)(Rb ↦ (Resp, [A, B], [aNon Na])),
chan := insert (Confid B A (Msg [aNon Na, aNon Nb])) (chan s)
⦈
}"
definition
m2_step3 :: "[rid_t, agent, agent, nonce, nonce] ⇒ (m2_state × m2_state) set"
where
"m2_step3 Ra A B Na Nb ≡ {(s, s1).
runs s Ra = Some (Init, [A, B], []) ∧
Na = Ra$0 ∧
Confid B A (Msg [aNon Na, aNon Nb]) ∈ chan s ∧
s1 = s⦇
runs := (runs s)(Ra ↦ (Init, [A, B], [aNon Nb]))
⦈
}"
text ‹Intruder fake event.›
definition
m2_fake :: "(m2_state × m2_state) set"
where
"m2_fake ≡ {(s, s1).
s1 = s⦇ chan := fake ik0 (dom (runs s)) (chan s) ⦈
}"
text ‹Transition system.›
definition
m2_trans :: "(m2_state × m2_state) set" where
"m2_trans ≡ (⋃ A B Ra Rb Na Nb.
m2_step1 Ra A B Na ∪
m2_step2 Rb A B Na Nb ∪
m2_step3 Ra A B Na Nb ∪
m2_fake ∪
Id
)"
definition
m2 :: "(m2_state, m2_obs) spec" where
"m2 ≡ ⦇
init = m2_init,
trans = m2_trans,
obs = m2_obs
⦈"
lemmas m2_defs =
m2_def m2_init_def m2_trans_def m2_obs_def
m2_step1_def m2_step2_def m2_step3_def m2_fake_def
subsection ‹Invariants›
subsubsection ‹Invariant 1: Messages only contains generated nonces.›
definition
m2_inv1_nonces :: "m2_state set" where
"m2_inv1_nonces ≡ {s. ∀R.
aNon (R$0) ∈ atoms (chan s) ⟶ R ∈ dom (runs s)
}"
lemmas m2_inv1_noncesI =
m2_inv1_nonces_def [THEN setc_def_to_intro, rule_format]
lemmas m2_inv1_noncesE [elim] =
m2_inv1_nonces_def [THEN setc_def_to_elim, rule_format]
lemmas m2_inv1_noncesD =
m2_inv1_nonces_def [THEN setc_def_to_dest, rule_format, rotated 1]
lemma PO_m2_inv1_init [iff]: "init m2 ⊆ m2_inv1_nonces"
by (auto simp add: PO_hoare_def m2_defs intro!: m2_inv1_noncesI)
lemma PO_m2_inv1_trans [iff]:
"{m2_inv1_nonces} trans m2 {> m2_inv1_nonces}"
apply (auto simp add: PO_hoare_def m2_defs intro!: m2_inv1_noncesI)
apply (auto dest: m2_inv1_noncesD)
apply (subgoal_tac "aNon (R$0) ∈ atoms (chan xa)", auto)
done
lemma PO_m2_inv012 [iff]:
"reach m2 ⊆ m2_inv1_nonces"
by (rule inv_rule_basic) (auto)
subsubsection ‹Invariant 3: relates message 2 with the responder run›
text ‹It is needed, together with initiator nonce secrecy, in proof
obligation REF/@{term m2_step2}.›
definition
m2_inv3_msg2 :: "m2_state set" where
"m2_inv3_msg2 ≡ {s. ∀A B Na Nb.
Confid B A (Msg [aNon Na, aNon Nb]) ∈ chan s ⟶
aNon Na ∉ extr ik0 (chan s) ⟶
(∃Rb. Nb = Rb$0 ∧ runs s Rb = Some (Resp, [A, B], [aNon Na]))
}"
lemmas m2_inv3_msg2I = m2_inv3_msg2_def [THEN setc_def_to_intro, rule_format]
lemmas m2_inv3_msg2E [elim] = m2_inv3_msg2_def [THEN setc_def_to_elim, rule_format]
lemmas m2_inv3_msg2D = m2_inv3_msg2_def [THEN setc_def_to_dest, rule_format, rotated 1]
lemma PO_m2_inv4_init [iff]:
"init m2 ⊆ m2_inv3_msg2"
by (auto simp add: PO_hoare_def m2_defs intro!: m2_inv3_msg2I)
lemma PO_m2_inv4_trans [iff]:
"{m2_inv3_msg2} trans m2 {> m2_inv3_msg2}"
apply (auto simp add: PO_hoare_def m2_defs intro!: m2_inv3_msg2I)
apply (auto dest: m2_inv3_msg2D dom_lemmas)
apply (drule m2_inv3_msg2D, auto dest: dom_lemmas)
apply (drule m2_inv3_msg2D, auto, force)
done
lemma PO_m2_inv4 [iff]: "reach m2 ⊆ m2_inv3_msg2"
by (rule inv_rule_incr) (auto del: subsetI)
subsubsection ‹Invariant 4: Initiator nonce secrecy.›
text ‹It is needed in the proof
obligation REF/@{term m2_step2}. It would be sufficient to prove the invariant
for the case @{term "x=None"}, but we have generalized it here.›
definition
m2_inv4_inon_secret :: "m2_state set" where
"m2_inv4_inon_secret ≡ {s. ∀A B Ra al.
runs s Ra = Some (Init, [A, B], al) ⟶
A ∉ bad ⟶ B ∉ bad ⟶
aNon (Ra$0) ∉ extr ik0 (chan s)
}"
lemmas m2_inv4_inon_secretI =
m2_inv4_inon_secret_def [THEN setc_def_to_intro, rule_format]
lemmas m2_inv4_inon_secretE [elim] =
m2_inv4_inon_secret_def [THEN setc_def_to_elim, rule_format]
lemmas m2_inv4_inon_secretD =
m2_inv4_inon_secret_def [THEN setc_def_to_dest, rule_format, rotated 1]
lemma PO_m2_inv3_init [iff]:
"init m2 ⊆ m2_inv4_inon_secret"
by (auto simp add: PO_hoare_def m2_defs intro!: m2_inv4_inon_secretI)
lemma PO_m2_inv3_trans [iff]:
"{m2_inv4_inon_secret ∩ m2_inv1_nonces}
trans m2
{> m2_inv4_inon_secret}"
apply (auto simp add: PO_hoare_def m2_defs intro!: m2_inv4_inon_secretI)
apply (auto dest: m2_inv4_inon_secretD)
apply (fastforce)
apply (fastforce)
apply (fastforce)
done
lemma PO_m2_inv3 [iff]: "reach m2 ⊆ m2_inv4_inon_secret"
by (rule inv_rule_incr [where J="m2_inv1_nonces"]) (auto)
subsection ‹Refinement›
definition
R12 :: "(m1_state × m2_state) set" where
"R12 ≡ {(s, t). runs s = runs t}"
abbreviation
med21 :: "m2_obs ⇒ m1_obs" where
"med21 ≡ id"
text ‹Proof obligations.›
lemma PO_m2_step1_refines_m1_step1:
"{R12}
(m1_step1 Ra A B Na), (m2_step1 Ra A B Na)
{> R12}"
by (auto simp add: PO_rhoare_defs R12_def m1_defs m2_defs)
lemma PO_m2_step2_refines_m1_step2:
"{R12}
(m1_step2 Rb A B Na Nb), (m2_step2 Rb A B Na Nb)
{> R12}"
by (auto simp add: PO_rhoare_defs R12_def m1_defs m2_defs)
lemma PO_m2_step3_refines_m1_step3:
"{R12 ∩ UNIV × (m2_inv4_inon_secret ∩ m2_inv3_msg2)}
(m1_step3 Ra A B Na Nb), (m2_step3 Ra A B Na Nb)
{> R12}"
by (auto simp add: PO_rhoare_defs R12_def m1_defs m2_defs)
(blast)
text ‹New fake events refine skip.›
lemma PO_m2_fake_refines_skip:
"{R12} Id, m2_fake {> R12}"
by (auto simp add: PO_rhoare_def R12_def m1_defs m2_defs)
lemmas PO_m2_trans_refines_m1_trans =
PO_m2_step1_refines_m1_step1 PO_m2_step2_refines_m1_step2
PO_m2_step3_refines_m1_step3 PO_m2_fake_refines_skip
text ‹All together now...›
lemma PO_m2_refines_init_m1 [iff]:
"init m2 ⊆ R12``(init m1)"
by (auto simp add: R12_def m1_defs m2_defs)
lemma PO_m2_refines_trans_m1 [iff]:
"{R12 ∩
UNIV × (m2_inv4_inon_secret ∩ m2_inv3_msg2)}
(trans m1), (trans m2)
{> R12}"
apply (auto simp add: m2_def m2_trans_def m1_def m1_trans_def)
apply (blast intro!: PO_m2_trans_refines_m1_trans)+
done
lemma PO_R12_obs_consistent [iff]:
"obs_consistent R12 med21 m1 m2"
by (auto simp add: obs_consistent_def R12_def m1_defs m2_defs)
lemma PO_m3_refines_m2:
"refines
(R12 ∩
UNIV × (m2_inv4_inon_secret ∩ m2_inv3_msg2 ∩ m2_inv1_nonces))
med21 m1 m2"
by (rule Refinement_using_invariants) (auto)
end
Theory m3_sig
section ‹Refinement 3a: Signature-based Dolev-Yao Protocol (Variant A)›
theory m3_sig imports m2_auth_chan "../Refinement/Message"
begin
text ‹We implement the channel protocol of the previous refinement with
signatures and add a full-fledged Dolev-Yao adversary. In this variant, the
adversary is realized using Paulson's closure operators for message derivation
(as opposed to a collection of one-step derivation events a la Strand spaces).
›
text ‹Proof tool configuration. Avoid annoying automatic unfolding of
‹dom› (again).›
declare domIff [simp, iff del]
declare analz_into_parts [dest]
subsection ‹State›
text ‹We extend the state of @{term m1} with insecure and authentic
channels between each pair of agents.›
record m3_state = m1_state +
IK :: "msg set"
type_synonym
m3_obs = m1_state
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 ⦃Agent A, Agent B, Nonce Na⦄ (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 ∧
⦃Agent A, Agent B, Nonce Na⦄ ∈ IK s ∧
s1 = s⦇
runs := (runs s)(Rb ↦ (Resp, [A, B], [aNon Na])),
IK := insert (Crypt (priK B) ⦃Nonce Nb, Nonce Na, Agent A⦄) (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 (priK B) ⦃Nonce Nb, Nonce Na, Agent A⦄ ∈ IK s ∧
s1 = s⦇
runs := (runs s)(Ra ↦ (Init, [A, B], [aNon Nb]))
⦈
}"
text ‹The intruder messages are now generated by a full-fledged 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 ‹Specialize injectiveness of parts 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]
text ‹The following invariants do not depend on the protocol messages.
We want to keep this compilation refinement from channel protocols to
full-fledged Dolev-Yao protocols as generic as possible.›
subsubsection ‹inv1: Long-term key secrecy›
text ‹Private signing keys are secret, that is, the intruder only knows
private keys of corrupted agents.
The invariant uses the weaker @{term parts} operator instead of the perhaps
more intuitive @{term analz} in its premise. This strengthens the invariant
and potentially simplifies its proof.
›
definition
m3_inv1_lkeysec :: "m3_state set" where
"m3_inv1_lkeysec ≡ {s. ∀ A.
Key (priK A) ∈ analz (IK s) ⟶ A ∈ bad
}"
lemmas m3_inv1_lkeysecI =
m3_inv1_lkeysec_def [THEN setc_def_to_intro, rule_format]
lemmas m3_inv1_lkeysecE [elim] =
m3_inv1_lkeysec_def [THEN setc_def_to_elim, rule_format]
lemmas m3_inv1_lkeysecD =
m3_inv1_lkeysec_def [THEN setc_def_to_dest, rule_format, rotated 1]
lemma PO_m3_inv1_lkeysec_init [iff]:
"init m3 ⊆ m3_inv1_lkeysec"
by (auto simp add: PO_hoare_def m3_defs intro!: m3_inv1_lkeysecI)
lemma PO_m3_inv1_lkeysec_trans [iff]:
"{m3_inv1_lkeysec} trans m3 {> m3_inv1_lkeysec}"
by (auto simp add: PO_hoare_def m3_defs intro!: m3_inv1_lkeysecI)
lemma PO_m3_inv1_lkeysec [iff]: "reach m3 ⊆ m3_inv1_lkeysec"
by (rule inv_rule_basic) (auto)
subsubsection ‹inv2: Intruder knows long-term keys of bad guys›
definition
m3_inv2_badkeys :: "m3_state set"
where
"m3_inv2_badkeys ≡ {s. ∀C.
C ∈ bad ⟶ Key (priK C) ∈ analz (IK s)
}"
lemmas m3_inv2_badkeysI =
m3_inv2_badkeys_def [THEN setc_def_to_intro, rule_format]
lemmas m3_inv2_badkeysE [elim] =
m3_inv2_badkeys_def [THEN setc_def_to_elim, rule_format]
lemmas m3_inv2_badkeysD [dest] =
m3_inv2_badkeys_def [THEN setc_def_to_dest, rule_format, rotated 1]
text ‹Invariance proof.›
lemma PO_m3_inv2_badkeys_init [iff]:
"init m3 ⊆ m3_inv2_badkeys"
by (auto simp add: m3_defs m3_inv2_badkeys_def)
lemma PO_m3_inv2_badkeys_trans [iff]:
"{m3_inv2_badkeys} trans m3 {> m3_inv2_badkeys}"
by (auto simp add: PO_hoare_defs m3_defs intro!: m3_inv2_badkeysI)
lemma PO_m3_inv2_badkeys [iff]: "reach m3 ⊆ m3_inv2_badkeys"
by (rule inv_rule_basic) (auto)
subsubsection ‹inv3: Intruder knows all public keys (NOT USED)›
text ‹This invariant is only needed with equality in ‹R23_msgs›.›
definition
m3_inv3_pubkeys :: "m3_state set"
where
"m3_inv3_pubkeys ≡ {s. ∀C.
Key (pubK C) ∈ analz (IK s)
}"
lemmas m3_inv3_pubkeysI =
m3_inv3_pubkeys_def [THEN setc_def_to_intro, rule_format]
lemmas m3_inv3_pubkeysE [elim] =
m3_inv3_pubkeys_def [THEN setc_def_to_elim, rule_format]
lemmas m3_inv3_pubkeysD [dest] =
m3_inv3_pubkeys_def [THEN setc_def_to_dest, rule_format, rotated 1]
text ‹Invariance proof.›
lemma PO_m3_inv3_pubkeys_init [iff]:
"init m3 ⊆ m3_inv3_pubkeys"
by (auto simp add: m3_defs m3_inv3_pubkeys_def)
lemma PO_m3_inv3_pubkeys_trans [iff]:
"{m3_inv3_pubkeys} trans m3 {> m3_inv3_pubkeys}"
by (auto simp add: PO_hoare_defs m3_defs intro!: m3_inv3_pubkeysI)
lemma PO_m3_inv3_pubkeys [iff]: "reach m3 ⊆ m3_inv3_pubkeys"
by (rule inv_rule_basic) (auto)
subsection ‹Refinement›
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]
subsubsection ‹Simulation relation›
abbreviation
nonces :: "msg set ⇒ nonce set"
where
"nonces H ≡ {N. Nonce N ∈ analz H}"
abbreviation
ink :: "chmsg set ⇒ nonce set"
where
"ink H ≡ {N. aNon N ∈ extr ik0 H}"
text ‹Abstraction function on sets of messages.›
inductive_set
abs_msg :: "msg set ⇒ chmsg set"
for H :: "msg set"
where
am_M1:
"⦃Agent A, Agent B, Nonce Na⦄ ∈ H
⟹ Insec A B (Msg [aNon Na]) ∈ abs_msg H"
| am_M2:
"Crypt (priK B) ⦃Nonce Nb, Nonce Na, Agent A⦄ ∈ H
⟹ Auth B A (Msg [aNon Nb, aNon Na]) ∈ abs_msg H"
text ‹The simulation relation is canonical. It states that the protocol
messages in the intruder knowledge refine the abstract messages appearing in
the channels @{term Insec} and @{term Auth}.›
definition
R23_msgs :: "(m2_state × m3_state) set" where
"R23_msgs ≡ {(s, t). abs_msg (parts (IK t)) ⊆ chan s}"
definition
R23_ink :: "(m2_state × m3_state) set" where
"R23_ink ≡ {(s, t). nonces (IK t) ⊆ ink (chan s)}"
definition
R23_preserved :: "(m2_state × m3_state) set" where
"R23_preserved ≡ {(s, t). runs s = runs t}"
definition
R23 :: "(m2_state × m3_state) set" where
"R23 ≡ R23_msgs ∩ R23_ink ∩ R23_preserved"
lemmas R23_defs = R23_def R23_msgs_def R23_ink_def R23_preserved_def
text ‹Mediator function: nothing new.›
definition
med32 :: "m3_obs ⇒ m2_obs" where
"med32 ≡ id"
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_inkI =
R23_ink_def [THEN rel_def_to_intro, simplified, rule_format]
lemmas R23_inkE [elim] =
R23_ink_def [THEN rel_def_to_elim, simplified, rule_format]
lemmas R23_preservedI =
R23_preserved_def [THEN rel_def_to_intro, simplified, rule_format]
lemmas R23_preservedE [elim] =
R23_preserved_def [THEN rel_def_to_elim, simplified, rule_format]
lemmas R23_intros = R23_msgsI R23_inkI R23_preservedI
subsubsection ‹Facts about the abstraction function›
declare abs_msg.intros [intro!]
declare abs_msg.cases [elim!]
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_fakeable:
"⟦ (s, t) ∈ R23_msgs; (s, t) ∈ R23_ink; t ∈ m3_inv1_lkeysec ⟧
⟹ abs_msg (synth (analz (IK t))) ⊆ fake ik0 (dom (runs s)) (chan s)"
apply (auto)
apply (rule fake_intros, auto)
apply (rule fake_Inj, auto)
apply (rule fake_intros, auto)
done
lemma absmsg_parts_subset_fakeable:
"⟦ (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_fakeable [simp, intro!]
declare absmsg_parts_subset_fakeable [simp, intro!]
subsubsection ‹Refinement proof›
lemma PO_m3_step1_refines_m2_step1:
"{R23}
(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 }
(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)
(auto)
text ‹The Dolev-Yao fake event refines the abstract fake event.›
lemma PO_m3_DY_fake_refines_m2_fake:
"{R23 ∩ UNIV × (m3_inv1_lkeysec ∩ m3_inv2_badkeys)}
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_inv2_badkeys ∩ m3_inv1_lkeysec)}
(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_obs_consistent [iff]:
"obs_consistent R23 med32 m2 m3"
by (auto simp add: obs_consistent_def R23_def med32_def m2_defs m3_defs)
lemma PO_m3_refines_m2:
"refines
(R23 ∩ UNIV × (m3_inv2_badkeys ∩ m3_inv1_lkeysec))
med32 m2 m3"
by (rule Refinement_using_invariants) (auto)
end
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
Theory m1_keydist
chapter ‹Key Establishment Protocols›
text ‹In this chapter, we develop several key establishment protocols:
\begin{itemize}
\item Needham-Schroeder Shared Key (NSSK)
\item core Kerberos IV and V, and
\item Denning-Sacco.
\end{itemize}
›
section ‹Basic abstract key distribution (L1)›
theory m1_keydist imports "../Refinement/Runs" "../Refinement/s0g_secrecy"
begin
text ‹The first refinement introduces the protocol roles, local memory of the
agents and the communication structure of the protocol. For actual
communication, the "receiver" directly reads the memory of the "sender".
It captures the core of essentials of server-based key distribution protocols:
The server generates a key that the clients read from his memory. At this
stage we are only interested in secrecy preservation, not in authentication.
›
declare option.split_asm [split]
declare domIff [simp, iff del]
consts
sk :: "nat"
subsection ‹State›
text ‹Runs record the protocol participants (initiator, responder) and the
keys learned during the execution. In later refinements, we will also add
nonces and timestamps to the run record.
The variables ‹kn› and ‹az› from ‹s0g_secrecy_leak›
are replaced by runs using a data refinement. Variable ‹lk› is
concretized into variable ‹leak›.
We define the state in two separate record definitions. The first one has
just a runs field and the second extends this with a leak field. Later
refinements may define different state for leaks (e.g. to record more context).
›
record m1r_state =
runs :: runs_t
record m1x_state = m1r_state +
leak :: "key set"
type_synonym m1x_obs = "m1x_state"
text ‹Predicate types for invariants and transition relation types. Use the
r-version for invariants and transitions if there is no reference to the leak
variable. This improves reusability in later refinements.
›
type_synonym 'x m1r_pred = "'x m1r_state_scheme set"
type_synonym 'x m1x_pred = "'x m1x_state_scheme set"
type_synonym 'x m1r_trans = "('x m1r_state_scheme × 'x m1r_state_scheme) set"
type_synonym 'x m1x_trans = "('x m1x_state_scheme × 'x m1x_state_scheme) set"
subsubsection ‹Key knowledge and authorization (reconstruction)›
text ‹Key knowledge and authorization relations, reconstructed from the runs
and an unspecified initial key setup. These auxiliary definitions are used in
some event guards and in the simulation relation (see below).›
text ‹Knowledge relation (reconstructed)›
inductive_set
knC :: "runs_t ⇒ (key × agent) set" for runz :: "runs_t"
where
knC_init:
"runz Ra = Some (Init, [A, B], aKey K # al) ⟹ (K, A) ∈ knC runz"
| knC_resp:
"runz Rb = Some (Resp, [A, B], aKey K # al) ⟹ (K, B) ∈ knC runz"
| knC_serv:
"⟦ Rs ∈ dom runz; fst (the (runz Rs)) = Serv ⟧ ⟹ (sesK (Rs$sk), Sv) ∈ knC runz"
| knC_0:
"(K, A) ∈ keySetup ⟹ (K, A) ∈ knC runz"
text ‹Authorization relation (reconstructed)›
inductive_set
azC :: "runs_t ⇒ (key × agent) set" for runz :: "runs_t"
where
azC_good:
"⟦ runz Rs = Some (Serv, [A, B], al); C ∈ {A, B, Sv} ⟧
⟹ (sesK (Rs$sk), C) ∈ azC runz"
| azC_bad:
"⟦ runz Rs = Some (Serv, [A, B], al); A ∈ bad ∨ B ∈ bad ⟧
⟹ (sesK (Rs$sk), C) ∈ azC runz"
| azC_0:
"⟦ (K, C) ∈ keySetup ⟧ ⟹ (K, C) ∈ azC runz"
declare knC.intros [intro]
declare azC.intros [intro]
text ‹Misc lemmas: empty state, projections, ...›
lemma knC_empty [simp]: "knC Map.empty = keySetup"
by (auto elim: knC.cases)
lemma azC_empty [simp]: "azC Map.empty = keySetup"
by (auto elim: azC.cases)
text ‹‹azC› and run abstraction›
lemma azC_map_runs [simp]: "azC (map_runs h runz) = azC runz"
by (auto simp add: map_runs_def elim!: azC.cases)
text ‹Update lemmas for @{term "knC"}›
lemma knC_upd_Init_Resp_None:
"⟦ R ∉ dom runz; rol ∈ {Init, Resp} ⟧
⟹ knC (runz(R ↦ (rol, [A, B], []))) = knC runz"
by (fastforce simp add: domIff elim!: knC.cases)
lemma knC_upd_Init_Some:
"⟦ runz Ra = Some (Init, [A, B], []) ⟧
⟹ knC (runz(Ra ↦ (Init, [A, B], [aKey Kab]))) = insert (Kab, A) (knC runz)"
apply (auto elim!: knC.cases)
apply (rename_tac Raa Aa Ba K al, rule_tac A=Aa and B=Ba and al=al in knC_init, auto)
apply (rename_tac Rb Aa Ba K al, rule_tac A=Aa and B=Ba and al=al in knC_resp, auto)
apply (rule_tac knC_serv, auto)
done
lemma knC_upd_Resp_Some:
"⟦ runz Ra = Some (Resp, [A, B], []) ⟧
⟹ knC (runz(Ra ↦ (Resp, [A, B], [aKey Kab]))) = insert (Kab, B) (knC runz)"
apply (auto elim!: knC.cases)
apply (rename_tac Raa Aa Ba K al, rule_tac A=Aa and B=Ba and al=al in knC_init, auto)
apply (rename_tac Raa Aa Ba K al, rule_tac A=Aa and B=Ba and al=al in knC_resp, auto)
apply (rule_tac knC_serv, auto)
done
lemma knC_upd_Server:
"⟦ Rs ∉ dom runz ⟧
⟹ knC (runz(Rs ↦ (Serv, [A, B], []))) = insert (sesK (Rs$sk), Sv) (knC runz)"
apply (auto elim!: knC.cases)
apply (rename_tac Raa Aa Ba K al, rule_tac A=Aa and B=Ba in knC_init, auto dest: dom_lemmas)
apply (rename_tac Raa Aa Ba K al, rule_tac A=Aa and B=Ba in knC_resp, auto dest: dom_lemmas)
done
lemmas knC_upd_lemmas [simp] =
knC_upd_Init_Resp_None knC_upd_Init_Some knC_upd_Resp_Some
knC_upd_Server
text ‹Update lemmas for @{term "azC"}›
lemma azC_upd_Init_None:
"⟦ Ra ∉ dom runz ⟧
⟹ azC (runz(Ra ↦ (Init, [A, B], []))) = azC runz"
by (auto simp add: azC.simps elim!: azC.cases dest: dom_lemmas)
lemma azC_upd_Resp_None:
"⟦ Rb ∉ dom runz ⟧
⟹ azC (runz(Rb ↦ (Resp, [A, B], []))) = azC runz"
by (auto simp add: azC.simps elim!: azC.cases dest: dom_lemmas)
lemma azC_upd_Init_Some:
"⟦ runz Ra = Some (Init, [A, B], []) ⟧
⟹ azC (runz(Ra ↦ (Init, [A, B], al))) = azC runz"
apply (auto elim!: azC.cases)
apply (rule_tac azC_good, auto)
apply (rule_tac azC_good, auto)
apply (rule_tac azC_good, auto)
apply (rule_tac azC_bad, auto)+
done
lemma azC_upd_Resp_Some:
"⟦ runz Rb = Some (Resp, [A, B], []) ⟧
⟹ azC (runz(Rb ↦ (Resp, [A, B], al))) = azC runz"
apply (auto elim!: azC.cases)
apply (rule_tac azC_good, auto)
apply (rule_tac azC_good, auto)
apply (rule_tac azC_good, auto)
apply (rule_tac azC_bad, auto)+
done
lemma azC_upd_Serv_bad:
"⟦ Rs ∉ dom runz; A ∈ bad ∨ B ∈ bad ⟧
⟹ azC (runz(Rs ↦ (Serv, [A, B], al))) = azC runz ∪ {sesK (Rs$sk)} × UNIV"
apply (auto elim!: azC.cases)
apply (
rename_tac Rsa Aa Ba ala, rule_tac A=Aa and B=Ba and al=ala in azC_good, auto dest: dom_lemmas,
rename_tac Rsa Aa Ba ala, rule_tac A=Aa and B=Ba and al=ala in azC_good, auto dest: dom_lemmas,
rename_tac Rsa Aa Ba ala, rule_tac A=Aa and B=Ba and al=ala in azC_good, auto dest: dom_lemmas,
rename_tac Rsa Aa Ba ala C, rule_tac A=Aa and B=Ba and al=ala in azC_bad, auto dest: dom_lemmas,
rename_tac Rsa Aa Ba ala C, rule_tac A=Aa and B=Ba and al=ala in azC_bad, auto dest: dom_lemmas
)+
done
lemma azC_upd_Serv_good:
"⟦ Rs ∉ dom runz; K = sesK (Rs$sk); A ∉ bad; B ∉ bad ⟧
⟹ azC (runz(Rs ↦ (Serv, [A, B], al)))
= azC runz ∪ {(K, A), (K, B), (K, Sv)}"
apply (auto elim!: azC.cases)
apply (
rename_tac Rsa Aa Ba ala, rule_tac A=Aa and B=Ba and al=ala in azC_good, auto dest: dom_lemmas,
rename_tac Rsa Aa Ba ala, rule_tac A=Aa and B=Ba and al=ala in azC_good, auto dest: dom_lemmas,
rename_tac Rsa Aa Ba ala, rule_tac A=Aa and B=Ba and al=ala in azC_good, auto dest: dom_lemmas,
rename_tac Rsa Aa Ba ala C, rule_tac A=Aa and B=Ba and al=ala in azC_bad, auto dest: dom_lemmas,
rename_tac Rsa Aa Ba ala C, rule_tac A=Aa and B=Ba and al=ala in azC_bad, auto dest: dom_lemmas
)+
done
lemma azC_upd_Serv:
"⟦ Rs ∉ dom runz; K = sesK (Rs$sk) ⟧
⟹ azC (runz(Rs ↦ (Serv, [A, B], al))) =
azC runz ∪ {K} × (if A ∉ bad ∧ B ∉ bad then {A, B, Sv} else UNIV)"
by (simp add: azC_upd_Serv_bad azC_upd_Serv_good)
lemmas azC_upd_lemmas [simp] =
azC_upd_Init_None azC_upd_Resp_None
azC_upd_Init_Some azC_upd_Resp_Some azC_upd_Serv
subsection ‹Events›
definition
m1x_step1 :: "[rid_t, agent, agent] ⇒ 'x m1r_trans"
where
"m1x_step1 Ra A B ≡ {(s, s1).
Ra ∉ dom (runs s) ∧
s1 = s⦇ runs := (runs s)(Ra ↦ (Init, [A, B], [])) ⦈
}"
definition
m1x_step2 :: "[rid_t, agent, agent] ⇒ 'x m1r_trans"
where
"m1x_step2 Rb A B ≡ {(s, s1).
Rb ∉ dom (runs s) ∧
s1 = s⦇ runs := (runs s)(Rb ↦ (Resp, [A, B], [])) ⦈
}"
definition
m1x_step3 :: "[rid_t, agent, agent, key] ⇒ 'x m1r_trans"
where
"m1x_step3 Rs A B Kab ≡ {(s, s1).
Rs ∉ dom (runs s) ∧
Kab = sesK (Rs$sk) ∧
s1 = s⦇ runs := (runs s)(Rs ↦ (Serv, [A, B], [])) ⦈
}"
definition
m1x_step4 :: "[rid_t, agent, agent, key] ⇒ 'x m1x_trans"
where
"m1x_step4 Ra A B Kab ≡ {(s, s1).
runs s Ra = Some (Init, [A, B], []) ∧
(Kab ∉ leak s ⟶ (Kab, A) ∈ azC (runs s)) ∧
s1 = s⦇ runs := (runs s)(Ra ↦ (Init, [A, B], [aKey Kab])) ⦈
}"
definition
m1x_step5 :: "[rid_t, agent, agent, key] ⇒ 'x m1x_trans"
where
"m1x_step5 Rb A B Kab ≡ {(s, s1).
runs s Rb = Some (Resp, [A, B], []) ∧
(Kab ∉ leak s ⟶ (Kab, B) ∈ azC (runs s)) ∧
s1 = s⦇ runs := (runs s)(Rb ↦ (Resp, [A, B], [aKey Kab])) ⦈
}"
definition
m1x_leak :: "rid_t ⇒ 'x m1x_trans"
where
"m1x_leak Rs ≡ {(s, s1).
Rs ∈ dom (runs s) ∧
fst (the (runs s Rs)) = Serv ∧
s1 = s⦇ leak := insert (sesK (Rs$sk)) (leak s) ⦈
}"
subsection ‹Specification›
definition
m1x_init :: "m1x_state set"
where
"m1x_init ≡ { ⦇
runs = Map.empty,
leak = corrKey
⦈ }"
definition
m1x_trans :: "'x m1x_trans" where
"m1x_trans ≡ (⋃A B Ra Rb Rs Kab.
m1x_step1 Ra A B ∪
m1x_step2 Rb A B ∪
m1x_step3 Rs A B Kab ∪
m1x_step4 Ra A B Kab ∪
m1x_step5 Rb A B Kab ∪
m1x_leak Rs ∪
Id
)"
definition
m1x :: "(m1x_state, m1x_obs) spec" where
"m1x ≡ ⦇
init = m1x_init,
trans = m1x_trans,
obs = id
⦈"
lemmas m1x_defs =
m1x_def m1x_init_def m1x_trans_def
m1x_step1_def m1x_step2_def m1x_step3_def m1x_step4_def m1x_step5_def
m1x_leak_def
lemma m1x_obs_id [simp]: "obs m1x = id"
by (simp add: m1x_def)
subsection ‹Invariants›
subsubsection ‹inv1: Key definedness›
text ‹Only run identifiers or static keys can be (concretely) known or
authorized keys. (This reading corresponds to the contraposition of the
property expressed below.)›
definition
m1x_inv1_key :: "m1x_state set"
where
"m1x_inv1_key ≡ {s. ∀Rs A.
Rs ∉ dom (runs s) ⟶
(sesK (Rs$sk), A) ∉ knC (runs s) ∧
(sesK (Rs$sk), A) ∉ azC (runs s) ∧
sesK (Rs$sk) ∉ leak s
}"
lemmas m1x_inv1_keyI = m1x_inv1_key_def [THEN setc_def_to_intro, rule_format]
lemmas m1x_inv1_keyE [elim] =
m1x_inv1_key_def [THEN setc_def_to_elim, rule_format]
lemmas m1x_inv1_keyD [dest] =
m1x_inv1_key_def [THEN setc_def_to_dest, rule_format, rotated 1]
text ‹Invariance proof.›
lemma PO_m1x_inv1_key_init [iff]:
"init m1x ⊆ m1x_inv1_key"
by (auto simp add: m1x_defs m1x_inv1_key_def)
lemma PO_m1x_inv1_key_trans [iff]:
"{m1x_inv1_key} trans m1x {> m1x_inv1_key}"
by (auto simp add: PO_hoare_defs m1x_defs intro!: m1x_inv1_keyI)
lemma PO_m1x_inv1_key [iff]: "reach m1x ⊆ m1x_inv1_key"
by (rule inv_rule_basic) (auto)
subsection ‹Refinement of s0g›
text ‹med10: The mediator function maps a concrete observation to an
abstract one.›
definition
med01x :: "m1x_obs ⇒ key s0g_obs"
where
"med01x t ≡ ⦇ kn = knC (runs t), az = azC (runs t), lk = leak t ⦈"
text ‹R01: The simulation relation expreses key knowledge and authorization
in terms of the client and server run information.›
definition
R01x :: "(key s0g_state × m1x_state) set" where
"R01x ≡ {(s, t). s = med01x t}"
lemmas R01x_defs = R01x_def med01x_def
text ‹Refinement proof.›
lemma PO_m1x_step1_refines_skip:
"{R01x}
Id, (m1x_step1 Ra A B)
{> R01x}"
by (auto simp add: PO_rhoare_defs R01x_defs s0g_defs m1x_defs)
lemma PO_m1x_step2_refines_skip:
"{R01x}
Id, (m1x_step2 Rb A B)
{> R01x}"
by (auto simp add: PO_rhoare_defs R01x_defs s0g_defs m1x_defs)
lemma PO_m1x_step3_refines_s0g_gen:
"{R01x ∩ UNIV × m1x_inv1_key}
(s0g_gen Kab Sv {Sv, A, B}), (m1x_step3 Rs A B Kab)
{> R01x}"
by (auto simp add: PO_rhoare_defs R01x_defs s0g_defs m1x_defs)
lemma PO_m1x_step4_refines_s0g_learn:
"{R01x}
(s0g_learn Kab A), (m1x_step4 Ra A B Kab)
{> R01x}"
by (auto simp add: PO_rhoare_defs R01x_defs s0g_defs m1x_defs)
lemma PO_m1x_step5_refines_s0g_learn:
"{R01x}
(s0g_learn Kab B), (m1x_step5 Rb A B Kab)
{> R01x}"
by (auto simp add: PO_rhoare_defs R01x_defs s0g_defs m1x_defs)
lemma PO_m1x_leak_refines_s0g_leak:
"{R01x}
(s0g_leak (sesK (Rs$sk))), (m1x_leak Rs)
{> R01x}"
by (fastforce simp add: PO_rhoare_defs R01x_defs s0g_defs m1x_defs)
text ‹All together now...›
lemmas PO_m1x_trans_refines_s0g_trans =
PO_m1x_step1_refines_skip PO_m1x_step2_refines_skip
PO_m1x_step3_refines_s0g_gen PO_m1x_step4_refines_s0g_learn
PO_m1x_step5_refines_s0g_learn PO_m1x_leak_refines_s0g_leak
lemma PO_m1x_refines_init_s0g [iff]:
"init m1x ⊆ R01x``(init s0g)"
by (auto simp add: R01x_defs s0g_defs m1x_defs intro!: s0g_secrecyI s0g_domI)
lemma PO_m1x_refines_trans_s0g [iff]:
"{R01x ∩ UNIV × m1x_inv1_key}
(trans s0g), (trans m1x)
{> R01x}"
by (auto simp add: m1x_def m1x_trans_def s0g_def s0g_trans_def
intro!: PO_m1x_trans_refines_s0g_trans)
text ‹Observation consistency.›
lemma obs_consistent_med01x [iff]:
"obs_consistent R01x med01x s0g m1x"
by (auto simp add: obs_consistent_def R01x_defs s0g_def m1x_def)
text ‹Refinement result.›
lemma PO_m1x_refines_s0g [iff]:
"refines
(R01x ∩ UNIV × m1x_inv1_key)
med01x s0g m1x"
by (rule Refinement_using_invariants) (auto del: subsetI)
lemma m1x_implements_s0g [iff]: "implements med01x s0g m1x"
by (rule refinement_soundness) (fast)
subsection ‹Derived invariants›
subsubsection ‹inv2: Secrecy›
text ‹Secrecy, expressed in terms of runs.›
definition
m1x_secrecy :: "'x m1x_pred"
where
"m1x_secrecy ≡ {s. knC (runs s) ⊆ azC (runs s) ∪ leak s × UNIV}"
lemmas m1x_secrecyI = m1x_secrecy_def [THEN setc_def_to_intro, rule_format]
lemmas m1x_secrecyE [elim] = m1x_secrecy_def [THEN setc_def_to_elim, rule_format]
text ‹Invariance proof.›
lemma PO_m1x_obs_secrecy [iff]: "oreach m1x ⊆ m1x_secrecy"
apply (rule external_invariant_translation [OF PO_s0g_obs_secrecy _ m1x_implements_s0g])
apply (auto simp add: med01x_def m1x_secrecy_def s0g_secrecy_def)
done
lemma PO_m1x_secrecy [iff]: "reach m1x ⊆ m1x_secrecy"
by (rule external_to_internal_invariant [OF PO_m1x_obs_secrecy], auto)
end
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››