Session Security_Protocol_Refinement

Theory Infra

(*******************************************************************************

  Project: Development of Security Protocols by Refinement

  Module:  Refinement/Infra.thy (Isabelle/HOL 2016-1)
  ID:      $Id: Infra.thy 134925 2017-05-24 17:53:14Z csprenge $
  Author:  Christoph Sprenger, ETH Zurich <sprenger@inf.ethz.ch>
  
  Infrastructure for refinement proofs (attributes, prover tuning etc)

  Copyright (c) 2009-2016 Christoph Sprenger 
  Licence: LGPL

*******************************************************************************)

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"      (* already in simpset *)
by (simp)

― ‹Do NOT add the following equation to the simpset! (looping)›
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

(*******************************************************************************

  Project: Development of Security Protocols by Refinement

  Module:  Refinement/Refinement.thy (Isabelle/HOL 2016-1)
  ID:      $Id: Refinement.thy 132773 2016-12-09 15:30:22Z csprenge $
  Author:  Christoph Sprenger, ETH Zurich <sprenger@inf.ethz.ch>
  
  Minimal infrastructure for invariants and refinements

  Copyright (c) 2009-2016 Christoph Sprenger
  Licence: LGPL

*******************************************************************************)

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"

(* inductive_cases reach_invert: "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"    ― ‹other direction holds trivially›

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)              ― ‹strengthen goal›
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:                    ― ‹do NOT declare [intro]›
  " {pre} Ra, Rc {> post'}; post'  post  
   {pre} Ra, Rc {> post}"
by (auto simp add: PO_rhoare_defs)

lemma relhoare_false_left [simp]:               ― ‹do NOT declare [intro]›
  "{ {} } Ra, Rc {> post}"
by (auto simp add: PO_rhoare_defs)

lemma relhoare_true_right [simp]:                ― ‹not true in general›
  "{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                            ― ‹only for deterministic 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}                       ― ‹any post, including UNIV›!›
   {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!]:   ― ‹might be too aggressive?›
  " {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)
  ― ‹case: singleton›
  apply (clarsimp simp add: PO_refines_def Image_def)
  apply (drule subsetD, auto)

  ― ‹case: cons; first construct related abstract state›
  apply (erule sl_cons_right_invert, clarsimp)
  apply (rename_tac s bc s' ba t)
  ― ‹now construct abstract transition›
  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"   ― ‹EQUIV: R``I ∩ J›
          "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

(*******************************************************************************

  Project: Development of Security Protocols by Refinement

  Module:  Refinement/Agents.thy (Isabelle/HOL 2016-1)
  ID:      $Id: Agents.thy 133854 2017-03-20 17:53:50Z csprenge $
  Author:  Christoph Sprenger, ETH Zurich <sprenger@inf.ethz.ch>

  Agents and nonces (partly based on Paulson's Message.thy)

  Copyright (c) 2009-2016 Christoph Sprenger 
  Licence: LGPL

*******************************************************************************)

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  ― ‹We allow any number of agents plus an honest server.›
  agent = Server | Agent nat

consts 
  bad :: "agent set"			      ― ‹compromised agents›

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

(*******************************************************************************  

  Project: Development of Security Protocols by Refinement

  Module:  Refinement/Keys.thy (Isabelle/HOL 2016-1)
  ID:      $Id: Keys.thy 132773 2016-12-09 15:30:22Z csprenge $
  Author:  Christoph Sprenger, ETH Zurich <sprenger@inf.ethz.ch>
  
  Symmetric (shared) and asymmetric (public/private) keys.
  (based on Larry Paulson's theory Public.thy)

  Copyright (c) 2012-2016 Christoph Sprenger 
  Licence: LGPL

*******************************************************************************)

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 =    ― ‹long-term keys›
  sharK "agent"     ― ‹key shared with server›
| publK "agent"     ― ‹agent's public key›
| privK "agent"     ― ‹agent's private key›

datatype key = 
  sesK "fresh_t"   ― ‹session key›
| ltK "ltkey"      ― ‹long-term key›

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

(*holds because invKey is injective*)

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"   ― ‹All session keys are symmetric›
by (simp add: symKeys_def)

lemma sym_shrK: "shrK X  symKeys"   ― ‹All shared keys are symmetric›
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

(*******************************************************************************

  Project: Development of Security Protocols by Refinement

  Module:  Refinement/Atoms.thy (Isabelle/HOL 2016-1)
  ID:      $Id: Atoms.thy 132773 2016-12-09 15:30:22Z csprenge $
  Author:  Christoph Sprenger, ETH Zurich <sprenger@inf.ethz.ch>
  
  Atomic messages for L1-L2 protocols

  Copyright (c) 2009-2016 Christoph Sprenger 
  Licence: LGPL

*******************************************************************************)

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"  ― ‹LT key setup, for now unspecified›

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

(*******************************************************************************

  Project: Development of Security Protocols by Refinement

  Module:  Refinement/Runs.thy (Isabelle/HOL 2016-1)
  ID:      $Id: Runs.thy 132773 2016-12-09 15:30:22Z csprenge $
  Author:  Christoph Sprenger, ETH Zurich <sprenger@inf.ethz.ch>
  
  Protocol runs: local state of executing protocol roles

  Copyright (c) 2010-2016 Christoph Sprenger 
  Licence: LGPL

*******************************************************************************)

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

(*******************************************************************************

  Project: Development of Security Protocols by Refinement

  Module:  Refinement/Channels.thy (Isabelle/HOL 2016-1)
  ID:      $Id: Channels.thy 132773 2016-12-09 15:30:22Z csprenge $
  Author:  Christoph Sprenger, ETH Zurich <sprenger@inf.ethz.ch>
  
  Channel messages for Level 2 protocols

  Copyright (c) 2009-2016 Christoph Sprenger 
  Licence: LGPL

*******************************************************************************)

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

(*
lemma extr_fake [simp]: "extr T (fake T U H) = extr T H"
proof -
  {
    fix At
    assume "At ∈ extr T (fake T U H)"
    hence "At ∈ extr T H" by induct auto
  }
  thus ?thesis by auto
qed
*)

end

Theory Message

(*******************************************************************************

  Title:      HOL/Auth/Message
  Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
  Copyright   1996  University of Cambridge

  Datatypes of agents and messages;
  Inductive relations "parts", "analz" and "synth"

********************************************************************************

  Module:  Refinement/Message.thy (Isabelle/HOL 2016-1)
  ID:      $Id: Message.thy 133856 2017-03-20 18:05:54Z csprenge $
  Edited:  Christoph Sprenger <sprenger@inf.ethz.ch>, ETH Zurich

  Integrated and adapted for security protocol refinement

*******************************************************************************)

section ‹Theory of Agents and Messages for Security Protocols›

theory Message imports Keys begin

(*Needed occasionally with spy_analz_tac, e.g. in analz_insert_Key_newK*)
lemma Un_idem_collapse [simp]: "A  (B  A) = B  A"
by blast

datatype
     msg = Agent  agent     ― ‹Agent names›
         | Number nat       ― ‹Ordinary integers, timestamps, ...›
         | Nonce  nonce     ― ‹Unguessable nonces›
         | Key    key       ― ‹Crypto keys›
         | Hash   msg       ― ‹Hashing›
         | MPair  msg msg   ― ‹Compound messages›
         | Crypt  key msg   ― ‹Encryption, public- or shared-key›


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
  ― ‹Message Y paired with a MAC computed with the help of X›
  "Hash[X] Y  HashX,Y, Y"

definition
  keysFor :: "msg set  key set"
where
    ― ‹Keys useful to decrypt elements of a message set›
  "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) = (xA)"
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 (iA. H i) = (iA. 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 ==> YH. 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: "(xA. parts(H x))  parts(xA. H x)"
by (intro UN_least parts_mono UN_upper)

lemma parts_UN_subset2: "parts(xA. H x)  (xA. parts(H x))"
apply (rule subsetI)
apply (erule parts.induct, blast+)
done

lemma parts_UN [simp]: "parts(xA. H x) = (xA. 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(GH)"} 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.›
(*
lemma msg_Nonce_supply: "∃N. ∀n. N≤n --> Nonce n ∉ parts {msg}"
apply (induct msg)
apply (simp_all (no_asm_simp) add: exI parts_insert2)
 txt{*MPair case: blast works out the necessary sum itself!*}
 prefer 2 apply auto apply (blast elim!: add_leE)
txt{*Nonce case*}
apply (rule_tac x = "N + Suc nat" in exI, auto)
done
*)


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: "GH ==> 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)

(*Cut can be proved easily by induction on
   "Y: analz (insert X H) ==> X: analz H --> Y: analz H"
*)

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 (iA. analz (H i)) ==> X analz (iA. H i)"
apply (erule analz.induct)
apply (blast intro: analz_mono [THEN [2] rev_subsetD])+
done

lemma analz_UN_analz [simp]: "analz (iA. analz (H i)) = analz (iA. 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: "GH ==> 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)
      ==> (HashX,Y  synth (analz H)) = (HashX,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' = HashX,Y & Y'=Y)"
by (simp add: HPair_def)

lemma HPair_eq_MPair [iff]:
     "(Hash[X] Y = X',Y') = (X' = HashX,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 (HashX,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 (HashX,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)) =
        (HashX, 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: "GH ==> 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

(*******************************************************************************

  Project: Development of Security Protocols by Refinement

  Module:  Refinement/s0g_secrecy.thy (Isabelle/HOL 2016-1)
  ID:      $Id: s0g_secrecy.thy 134924 2017-05-24 17:23:15Z csprenge $
  Author:  Christoph Sprenger, ETH Zurich <sprenger@inf.ethz.ch>
  
  Key distribution protocols
  Initial Model: Secrecy (global version)

  Copyright (c) 2009-2016 Christoph Sprenger
  Licence: LGPL

*******************************************************************************)

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"                         ― ‹leaked data›

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).
    ― ‹guards:›
    A  G     
    d  Domain (kn s)                       ― ‹fresh item›
 
    ― ‹actions:›
    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).
    ― ‹guards:›
    ― ‹d ∈ Domain (kn s) ∧› someone knows d› (follows from authorization)›

    ― ‹check authorization or leakage to preserve secrecy›
    (d, B)  az s  lkr s 

    ― ‹actions:›
    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).
    ― ‹guards:›
    d  Domain (kn s)        ― ‹someone knows d›

    ― ‹actions:›
    s1 = s lk := insert d (lk s) 
  }"


(******************************************************************************)
subsection ‹Specification›
(******************************************************************************)

definition 
  s0g_init :: "'d s0g_state set"
where
  "s0g_init  s0g_secrecy  s0g_dom"   ― ‹any state satisfying invariants›

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

(*******************************************************************************

  Project: Development of Security Protocols by Refinement

  Module:  Refinement/a0n_agree.thy (Isabelle/HOL 2016-1)
  ID:      $Id: a0n_agree.thy 134924 2017-05-24 17:23:15Z csprenge $
  Author:  Christoph Sprenger, ETH Zurich <sprenger@inf.ethz.ch>
  
  One-Way authentication protocols
  Initial Model: Non-injective agreement 

  Copyright (c) 2009-2016 Christoph Sprenger
  Licence: LGPL

*******************************************************************************)

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"    ― ‹multi-set of signals›
  corrupted :: "'ds set"            ― ‹set of corrupted data›

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').
    ― ‹actions:›
    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').
    ― ‹guards:›
    (set h  good  d  corrupted s  signals s (Running h d) > 0) 

    ― ‹actions:›
    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').
    ― ‹actions:›
    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

(*******************************************************************************

  Project: Development of Security Protocols by Refinement

  Module:  Refinement/a0i_agree.thy (Isabelle/HOL 2016-1)
  ID:      $Id: a0i_agree.thy 134924 2017-05-24 17:23:15Z csprenge $
  Author:  Christoph Sprenger, ETH Zurich <sprenger@inf.ethz.ch>
  
  One-Way authentication protocols
  Initial Model: Injective agreement

  Copyright (c) 2009-2016 Christoph Sprenger
  Licence: LGPL

*******************************************************************************)

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').
    ― ‹guards:›
    (set h  good  d  corrupted s 
       signals s (Commit h d) < signals s (Running h d)) 

    ― ‹actions:›
    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

(*******************************************************************************

  Project: Development of Security Protocols by Refinement

  Module:  Auth_simple/m1_auth.thy (Isabelle/HOL 2016-1)
  ID:      $Id: m1_auth.thy 134925 2017-05-24 17:53:14Z csprenge $
  Author:  Christoph Sprenger, ETH Zurich <sprenger@inf.ethz.ch>
  
  One-Way authentication protocols
  Refinement 1: Direct memory access protocol 

  Copyright (c) 2009-2016 Christoph Sprenger
  Licence: LGPL

*******************************************************************************)

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 option.split_asm [split] *)
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   ― ‹refines @{term skip}
  m1_step1 :: "[rid_t, agent, agent, nonce]  (m1_state × m1_state) set" 
where  
  "m1_step1 Ra A B Na  {(s, s1).  

     ― ‹guards›
     Ra  dom (runs s)               ― ‹new initiator run›
     Na = Ra$0                       ― ‹generated nonce›

     ― ‹actions›
     s1 = s 
       runs := (runs s)(
         Ra  (Init, [A, B], [])
       )  
     
  }"

definition   ― ‹refines @{term a0i_running}
  m1_step2 :: "[rid_t, agent, agent, nonce, nonce]  (m1_state × m1_state) set" 
where
  "m1_step2 Rb A B Na Nb  {(s, s1).  ― ‹Ni› is completely arbitrary›

     ― ‹guards›
     Rb  dom (runs s)               ― ‹new responder run›
     Nb = Rb$0                       ― ‹generated nonce›

     ― ‹actions›
     s1 = s
       runs := (runs s)(Rb  (Resp, [A, B], [aNon Na]))
     
  }"

definition   ― ‹refines @{term a0i_commit}
  m1_step3 :: 
    "[rid_t, agent, agent, nonce, nonce]  (m1_state × m1_state) set" 
where
  "m1_step3 Ra A B Na Nb  {(s, s1).

     ― ‹guards›
     runs s Ra = Some (Init, [A, B], []) 
     Na = Ra$0 

     ― ‹authentication guard:›
     (A  bad  B  bad  (Rb. 
        Nb = Rb$0  runs s Rb = Some (Resp, [A, B], [aNon Na]))) 

     ― ‹actions›
     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

(*******************************************************************************

  Project: Development of Security Protocols by Refinement

  Module:  Auth_simple/m2_auth_chan.thy (Isabelle/HOL 2016-1)
  ID:      $Id: m2_auth_chan.thy 133854 2017-03-20 17:53:50Z csprenge $
  Author:  Christoph Sprenger, ETH Zurich <sprenger@inf.ethz.ch>
  
  One-Way authentication protocols
  Refinement 2: protocol using authentic channels

  Copyright (c) 2009-2016 Christoph Sprenger 
  Licence: LGPL

*******************************************************************************)

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).
     ― ‹guards›
     Ra  dom (runs s) 
     Na = Ra$0 

     ― ‹actions›
     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).
     ― ‹guards›
     Rb  dom (runs s) 
     Nb = Rb$0 

     Insec A B (Msg [aNon Na])  chan s                           ― ‹rcv M1›

     ― ‹actions›
     s1 = s 
       runs := (runs s)(Rb  (Resp, [A, B], [aNon Na])), 
       chan := insert (Auth B A (Msg [aNon Nb, aNon Na])) (chan s)  ― ‹snd M2›
       
  }"

definition
  m2_step3 :: "[rid_t, agent, agent, nonce, nonce]  (m2_state × m2_state) set"
where
  "m2_step3 Ra A B Na Nb  {(s, s1).
     ― ‹guards›
     runs s Ra = Some (Init, [A, B], []) 
     Na = Ra$0 

     Auth B A (Msg [aNon Nb, aNon Na])  chan s             ― ‹recv M2›

     ― ‹actions›
     s1 = s 
       runs := (runs s)(Ra  (Init, [A, B], [aNon Nb]))
       
  }"


text ‹Intruder fake event.›

definition     ― ‹refines @{term Id} 
  m2_fake :: "(m2_state × m2_state) set"
where
  "m2_fake  {(s, s1). 

    ― ‹actions:›
    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)
― ‹1 subgoal›
apply (force)                            (* SLOW *)
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}"           ― ‹That's it!›
 
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

(*******************************************************************************

  Project: Development of Security Protocols by Refinement

  Module:  Auth_simple/m2_confid_chan.thy (Isabelle/HOL 2016-1)
  ID:      $Id: m2_confid_chan.thy 133854 2017-03-20 17:53:50Z csprenge $
  Author:  Christoph Sprenger, ETH Zurich <sprenger@inf.ethz.ch>
  
  One-Way authentication protocols
  Refinement 2: protocol using confidential channels

  Copyright (c) 2009-2016 Christoph Sprenger 
  Licence: LGPL

*******************************************************************************)

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"                     ― ‹channels›

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).

     ― ‹guards:›
     Ra  dom (runs s) 
     Na = Ra$0 

     ― ‹actions:›
     s1 = s
       runs := (runs s)(Ra  (Init, [A, B], [])), 
       ― ‹send Na› on confidential channel 1›
       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).

     ― ‹guards›
     Rb  dom (runs s) 
     Nb = Rb$0 

     Confid A B (Msg [aNon Na])  chan s            ― ‹receive M1›

     ― ‹actions›
     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).

     ― ‹guards›
     runs s Ra = Some (Init, [A, B], []) 
     Na = Ra$0 

     Confid B A (Msg [aNon Na, aNon Nb])  chan s   ― ‹receive M2›

     ― ‹actions›
     s1 = s 
       runs := (runs s)(Ra  (Init, [A, B], [aNon Nb]))
       
  }"


text ‹Intruder fake event.›

definition     ― ‹refines @{term Id} 
  m2_fake :: "(m2_state × m2_state) set"
where
  "m2_fake  {(s, s1). 
    ― ‹actions:›
    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)
― ‹1 subgoal›
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›
(******************************************************************************)
(*
 1. ⋀a y. ⟦runs a = runs y; runs y Ra = Some (Init, [A, B], []);
           Confid A B (Msg [aNon (Ra$0), aNon Nb]) ∈ chan y; A ∉ bad; B ∉ bad⟧
          ⟹ ∃Rb. Nb = Rb $ 0 ∧ runs y Rb = Some (Resp, [A, B], [aNon (Ra $ 0)])
*)
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)
― ‹2 subgoals›
  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) 
― ‹3 subgoals›
  apply (fastforce)                ― ‹requires @{text "m2_inv1_nonces"}
  apply (fastforce)                ― ‹requires ind hyp›
  apply (fastforce)                ― ‹requires ind hyp›
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

(*******************************************************************************

  Project: Development of Security Protocols by Refinement

  Module:  Auth_simple/m3_sig.thy (Isabelle/HOL 2016-1)
  ID:      $Id: m3_sig.thy 133852 2017-03-20 15:59:33Z csprenge $
  Author:  Christoph Sprenger, ETH Zurich <sprenger@inf.ethz.ch>

  One-Way authentication protocols
  Refinement 3: protocol using signatures

  Copyright (c) 2009-2016 Christoph Sprenger
  Licence: LGPL

*******************************************************************************)

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"                             ― ‹intruder knowledge›

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).

     ― ‹guards›
     Ra  dom (runs s) 
     Na = Ra$0 

     ― ‹actions›
     s1 = s
       runs := (runs s)(Ra  (Init, [A, B], [])),
       IK := insert Agent A, Agent B, Nonce Na (IK s)    ― ‹send msg 1›
     
  }"

definition
  m3_step2 :: "[rid_t, agent, agent, nonce, nonce]  (m3_state × m3_state) set"
where
  "m3_step2 Rb A B Na Nb  {(s, s1).

     ― ‹guards›
     Rb  dom (runs s) 
     Nb = Rb$0 

     Agent A, Agent B, Nonce Na  IK s             ― ‹receive msg 1›

     ― ‹actions›
     s1 = s
       runs := (runs s)(Rb  (Resp, [A, B], [aNon Na])),
                                                        ― ‹send msg 2›
       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).

     ― ‹guards›
     runs s Ra = Some (Init, [A, B], []) 
     Na = Ra$0 

     Crypt (priK B) Nonce Nb, Nonce Na, Agent A  IK s  ― ‹recv msg 2›

     ― ‹actions›
     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).

     ― ‹actions:›
     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}"   ― ‹with parts›!›

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 ⌦‹∩ UNIV × m3_inv3_pubkeys›}
     (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

(*******************************************************************************

  Project: Development of Security Protocols by Refinement

  Module:  Auth_simple/m3_enc.thy (Isabelle/HOL 2016-1)
  ID:      $Id: m3_enc.thy 133852 2017-03-20 15:59:33Z csprenge $
  Author:  Christoph Sprenger, ETH Zurich <sprenger@inf.ethz.ch>
  
  One-Way authentication protocols
  Refinement 3: protocol using public-key encryption and Dolev-Yao intruder

  Copyright (c) 2009-2016 Christoph Sprenger 
  Licence: LGPL

*******************************************************************************)

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"                                 ― ‹intruder knowledge›


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).

     ― ‹guards:›
     Ra  dom (runs s) 
     Na = Ra$0 

     ― ‹actions:›
     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).

     ― ‹guards›
     Rb  dom (runs s) 
     Nb = Rb$0 

     Crypt (pubK B) Nonce Na, Agent A  IK s       ― ‹receive msg 1›

     ― ‹actions›
     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).

     ― ‹guards›
     runs s Ra = Some (Init, [A, B], []) 
     Na = Ra$0 

     Crypt (pubK A) Nonce Na, Nonce Nb, Agent B  IK s    ― ‹recv msg2›

     ― ‹actions›
     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).

     ― ‹actions:›
     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}"   ― ‹with parts›!›

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

(*******************************************************************************

  Project: Development of Security Protocols by Refinement

  Module:  Key_establish/m1b_keydist.thy (Isabelle/HOL 2016-1)
  ID:      $Id: m1_keydist.thy 134925 2017-05-24 17:53:14Z csprenge $
  Author:  Christoph Sprenger, ETH Zurich <sprenger@inf.ethz.ch>
  
  Key distribution protocols
  First refinement: abstract server-based key transport protocol with 
  initiator and responder roles.

  Copyright (c) 2009-2016 Christoph Sprenger
  Licence: LGPL

*******************************************************************************)

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"             ― ‹identifier used for session keys›


(******************************************************************************)
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"             ― ‹keys leaked to attacker›

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) 
― ‹3 subgoals›
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)
― ‹3 subgoals›
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)
― ‹2 subgoals›
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)
― ‹5 subgoals›
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)
― ‹5 subgoals›
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)
― ‹10 subgoals›
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)
― ‹5 subgoals›
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     ― ‹by @{term "A"}, refines skip›
  m1x_step1 :: "[rid_t, agent, agent]  'x m1r_trans"
where
  "m1x_step1 Ra A B  {(s, s1).

    ― ‹guards:›
    Ra  dom (runs s)                 ― ‹Ra› is fresh›

    ― ‹actions:›
    ― ‹create initiator thread›
    s1 = s runs := (runs s)(Ra  (Init, [A, B], [])) 
  }"

definition     ― ‹by @{term "B"}, refines skip›
  m1x_step2 :: "[rid_t, agent, agent]  'x m1r_trans"
where
  "m1x_step2 Rb A B  {(s, s1).

    ― ‹guards:›
    Rb  dom (runs s)                ― ‹Rb› is fresh›

    ― ‹actions:›
    ― ‹create responder thread›
    s1 = s runs := (runs s)(Rb  (Resp, [A, B], [])) 
  }"

definition     ― ‹by @{term "Server"}, refines @{term s0g_gen}
  m1x_step3 :: "[rid_t, agent, agent, key]  'x m1r_trans"
where
  "m1x_step3 Rs A B Kab  {(s, s1).

    ― ‹guards:›
    Rs  dom (runs s)                         ― ‹Rs› is fresh›
    Kab = sesK (Rs$sk)                        ― ‹generate session key›

    ― ‹actions:›
    s1 = s runs := (runs s)(Rs  (Serv, [A, B], [])) 
  }"

definition     ― ‹by @{term "A"}, refines @{term s0g_learn}
  m1x_step4 :: "[rid_t, agent, agent, key]  'x m1x_trans"
where
  "m1x_step4 Ra A B Kab  {(s, s1).
    ― ‹guards:›
    runs s Ra = Some (Init, [A, B], []) 
    (Kab  leak s  (Kab, A)  azC (runs s))    ― ‹authorization guard›

    ― ‹actions:›
    s1 = s runs := (runs s)(Ra  (Init, [A, B], [aKey Kab])) 
  }"

definition     ― ‹by @{text "B"}, refines @{term s0g_learn}
  m1x_step5 :: "[rid_t, agent, agent, key]  'x m1x_trans"
where
  "m1x_step5 Rb A B Kab  {(s, s1).
    ― ‹guards:›
    runs s Rb = Some (Resp, [A, B], [])  
    (Kab  leak s  (Kab, B)  azC (runs s))     ― ‹authorization guard›

    ― ‹actions:›
    s1 = s runs := (runs s)(Rb  (Resp, [A, B], [aKey Kab])) 
  }"

definition     ― ‹by attacker, refines @{term s0g_leak}
  m1x_leak :: "rid_t  'x m1x_trans"
where
  "m1x_leak Rs  {(s, s1).           
    ― ‹guards:›
    Rs  dom (runs s) 
    fst (the (runs s Rs)) = Serv          ― ‹compromise server run Rs›

    ― ‹actions:›
    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         ― ‹statically corrupted keys initially leaked›
   }"

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›
(*inv**************************************************************************)

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›
(*invh*************************************************************************)

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

(*******************************************************************************

  Project: Development of Security Protocols by Refinement

  Module:   Key_establish/m1_keydist_iirn.thy (Isabelle/HOL 2016-1)
  ID:       $Id: m1_keydist_iirn.thy 133854 2017-03-20 17:53:50Z csprenge $
  Author:   Christoph Sprenger, ETH Zurich <sprenger@inf.ethz.ch>

  Key distribution protocols
  Level 1, 1st refinement: Abstract server-based key transport protocol with 
  initiator and responder roles. Provides injective server authentication to 
  the initiator and non-injective server authenticaiton to the responder.

  Copyright (c) 2009-2016 Christoph Sprenger
  Licence: LGPL

*******************************************************************************)

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]
(* declare option.split_asm [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"   ― ‹num of agreeing list elements for initiator-server›  
  rs_len :: "nat"   ― ‹num of agreeing list elements for responder-server›


(******************************************************************************)
subsection ‹Events›
(******************************************************************************)

definition         ― ‹by @{term "A"}, refines @{term "m1x_step1"}
  m1a_step1 :: "[rid_t, agent, agent, nonce]  'x m1r_trans"
where
  "m1a_step1 Ra A B Na  {(s, s1).
    ― ‹guards:›
    Ra  dom (runs s)                 ― ‹Ra› is fresh›
    Na = Ra$na                        ― ‹NEW: generate a nonce›

    ― ‹actions:›
    ― ‹create initiator thread›
    s1 = s runs := (runs s)(Ra  (Init, [A, B], [])) 
  }"

definition       ― ‹by @{term "B"}, refines @{term "m1x_step2"}
  m1a_step2 :: "[rid_t, agent, agent]  'x m1r_trans"
where
  "m1a_step2  m1x_step2"

definition       ― ‹by @{term "Server"}, refines @{term m1x_step3}
  m1a_step3 :: "[rid_t, agent, agent, key, nonce, atom list]  'x m1r_trans"
where
  "m1a_step3 Rs A B Kab Na al  {(s, s1).
     ― ‹guards:›
     Rs  dom (runs s)                  ― ‹fresh run id›
     Kab = sesK (Rs$sk)                 ― ‹generate session key›

     ― ‹actions:›
     s1 = s runs := (runs s)(Rs  (Serv, [A, B], aNon Na # al)) 
  }"

definition         ― ‹by @{text "A"}, refines @{term m1x_step4}
  m1a_step4 :: "[rid_t, agent, agent, nonce, key, atom list]  'x m1a_trans"
where
  "m1a_step4 Ra A B Na Kab nla  {(s, s').
     ― ‹guards:›
     runs s Ra = Some (Init, [A, B], []) 
     (Kab  leak s  (Kab, A)  azC (runs s))   ― ‹authorization guard›
     Na = Ra$na                                    ― ‹fix parameter›

     ― ‹new guard for agreement with server on (Kab, B, Na, isl)›,›
     ― ‹where isl = take is_len nla›; injectiveness by including Na›
     (A  bad  (Rs. Kab = sesK (Rs$sk) 
        runs s Rs = Some (Serv, [A, B], aNon Na # take is_len nla))) 

     ― ‹actions:›
     s' = s runs := (runs s)(Ra  (Init, [A, B], aKey Kab # nla)) 
  }" 

definition         ― ‹by @{term "B"}, refines @{term m1x_step5}
  m1a_step5 :: "[rid_t, agent, agent, key, atom list]  'x m1a_trans"
where
  "m1a_step5 Rb A B Kab nlb  {(s, s1). 
     ― ‹guards:›
     runs s Rb = Some (Resp, [A, B], [])  
     (Kab  leak s  (Kab, B)  azC (runs s))          ― ‹authorization guard›

     ― ‹guard for showing agreement with server on (Kab, A, rsl)›,›
     ― ‹where rsl = take rs_len nlb›; this agreement is non-injective›

     (B  bad  (Rs Na. Kab = sesK (Rs$sk) 
        runs s Rs = Some (Serv, [A, B], aNon Na # take rs_len nlb))) 

     ― ‹actions:›
     s1 = s runs := (runs s)(Rb  (Resp, [A, B], aKey Kab # nlb)) 
  }"

definition     ― ‹by attacker, refines @{term m1x_leak}
  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›
(*inv**************************************************************************)

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›