# Theory Message

Up to index of Isabelle/HOL/Auth

theory Message
imports Main
begin

    (*  Title:      HOL/Auth/Message
        ID:         $Id: Message.thy,v 1.40 2005/09/30 07:52:46 paulson Exp $
        Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
        Copyright   1996  University of Cambridge

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

    header{*Theory of Agents and Messages for Security Protocols*}

    theory Message imports Main begin

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

    types
      key = nat

    consts
      all_symmetric :: bool        --{*true if all keys are symmetric*}
      invKey        :: "key=>key"  --{*inverse of a symmetric key*}

    specification (invKey)
      invKey [simp]: "invKey (invKey K) = K"
      invKey_symmetric: "all_symmetric --> invKey = id"
        by (rule exI [of _ id], auto)

    text{*The inverse of a symmetric key is itself; that of a public key
          is the private key and vice versa*}

    constdefs
      symKeys :: "key set"
      "symKeys == {K. invKey K = K}"

    datatype  --{*We allow any number of friendly agents*}
      agent = Server | Friend nat | Spy

    datatype
         msg = Agent  agent     --{*Agent names*}
             | Number nat       --{*Ordinary integers, timestamps, ...*}
             | Nonce  nat       --{*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{|_,/ _|})")

    syntax (xsymbols)
      "@MTuple"      :: "['a, args] => 'a * 'b"       ("(2\<lbrace>_,/ _\<rbrace>)")

    translations
      "{|x, y, z|}"   == "{|x, {|y, z|}|}"
      "{|x, y|}"      == "MPair x y"

    constdefs
      HPair :: "[msg,msg] => msg"                       ("(4Hash[_] /_)" [0, 1000])
        --{*Message Y paired with a MAC computed with the help of X*}
        "Hash[X] Y == {| Hash{|X,Y|}, Y|}"

      keysFor :: "msg set => key set"
        --{*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*}

    consts  parts   :: "msg set => msg set"
    inductive "parts H"
      intros
        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 Friend_image_eq [simp]: "(Friend x ∈ Friend`A) = (x:A)"
    by auto

    lemma Key_image_eq [simp]: "(Key x ∈ Key`A) = (x∈A)"
    by auto

    lemma Nonce_Key_image_eq [simp]: "(Nonce x ∉ Key`A)"
    by auto

    subsubsection{*Inverse of keys *}

    lemma invKey_eq [simp]: "(invKey K = invKey K') = (K=K')"
    apply safe
    apply (drule_tac f = invKey in arg_cong, simp)
    done

    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 (\<Union>i∈A. H i) = (\<Union>i∈A. keysFor (H i))"
    by (unfold keysFor_def, blast)

    text{*Monotonicity*}
    lemma keysFor_mono: "G ⊆ H ==> keysFor(G) ⊆ keysFor(H)"
    by (unfold keysFor_def, blast)

    lemma keysFor_insert_Agent [simp]: "keysFor (insert (Agent A) H) = keysFor H"
    by (unfold keysFor_def, auto)

    lemma keysFor_insert_Nonce [simp]: "keysFor (insert (Nonce N) H) = keysFor H"
    by (unfold keysFor_def, auto)

    lemma keysFor_insert_Number [simp]: "keysFor (insert (Number N) H) = keysFor H"
    by (unfold keysFor_def, auto)

    lemma keysFor_insert_Key [simp]: "keysFor (insert (Key K) H) = keysFor H"
    by (unfold keysFor_def, auto)

    lemma keysFor_insert_Hash [simp]: "keysFor (insert (Hash X) H) = keysFor H"
    by (unfold keysFor_def, auto)

    lemma keysFor_insert_MPair [simp]: "keysFor (insert {|X,Y|} H) = keysFor H"
    by (unfold keysFor_def, auto)

    lemma keysFor_insert_Crypt [simp]:
        "keysFor (insert (Crypt K X) H) = insert (invKey K) (keysFor H)"
    by (unfold keysFor_def, auto)

    lemma keysFor_image_Key [simp]: "keysFor (Key`E) = {}"
    by (unfold keysFor_def, auto)

    lemma Crypt_imp_invKey_keysFor: "Crypt K X ∈ H ==> invKey K ∈ keysFor H"
    by (unfold keysFor_def, blast)

    subsection{*Inductive relation "parts"*}

    lemma MPair_parts:
         "[| {|X,Y|} ∈ parts H;
             [| X ∈ parts H; Y ∈ parts H |] ==> P |] ==> P"
    by (blast dest: parts.Fst parts.Snd)

    declare MPair_parts [elim!]  parts.Body [dest!]
    text{*NB These two rules are UNSAFE in the formal sense, as they discard the
         compound message.  They work well on THIS FILE.
      @{text 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, standard]

    lemma parts_empty [simp]: "parts{} = {}"
    apply safe
    apply (erule parts.induct, blast+)
    done

    lemma parts_emptyE [elim!]: "X∈ parts{} ==> P"
    by simp

    text{*WARNING: loops if H = {Y}, therefore must not be repeated!*}
    lemma parts_singleton: "X∈ parts H ==> ∃Y∈H. X∈ parts {Y}"
    by (erule parts.induct, blast+)

    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: "(\<Union>x∈A. parts(H x)) ⊆ parts(\<Union>x∈A. H x)"
    by (intro UN_least parts_mono UN_upper)

    lemma parts_UN_subset2: "parts(\<Union>x∈A. H x) ⊆ (\<Union>x∈A. parts(H x))"
    apply (rule subsetI)
    apply (erule parts.induct, blast+)
    done

    lemma parts_UN [simp]: "parts(\<Union>x∈A. H x) = (\<Union>x∈A. parts(H x))"
    by (intro equalityI parts_UN_subset1 parts_UN_subset2)

    text{*Added to simplify arguments to parts, analz and synth.
      NOTE: the UN versions are no longer used!*}

    text{*This allows @{text blast} to simplify occurrences of
      @{term "parts(G∪H)"} in the assumption.*}
    lemmas in_parts_UnE = parts_Un [THEN equalityD1, THEN subsetD, THEN UnE]
    declare in_parts_UnE [elim!]

    lemma parts_insert_subset: "insert X (parts H) ⊆ parts(insert X H)"
    by (blast intro: parts_mono [THEN [2] rev_subsetD])

    subsubsection{*Idempotence and transitivity *}

    lemma parts_partsD [dest!]: "X∈ parts (parts H) ==> X∈ parts H"
    by (erule parts.induct, blast+)

    lemma parts_idem [simp]: "parts (parts H) = parts H"
    by blast

    lemma parts_subset_iff [simp]: "(parts G ⊆ parts H) = (G ⊆ parts H)"
    apply (rule iffI)
    apply (iprover intro: subset_trans parts_increasing)
    apply (frule parts_mono, simp)
    done

    lemma parts_trans: "[| X∈ parts G;  G ⊆ parts H |] ==> X∈ parts H"
    by (drule parts_mono, blast)

    text{*Cut*}
    lemma parts_cut:
         "[| Y∈ parts (insert X G);  X∈ parts H |] ==> Y∈ parts (G ∪ H)"
    by (erule parts_trans, auto)

    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_tac "msg")
    apply (simp_all (no_asm_simp) add: exI parts_insert2)
     txt{*MPair case: blast works out the necessary sum itself!*}
     prefer 2 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.  *}

    consts  analz   :: "msg set => msg set"
    inductive "analz H"
      intros
        Inj [intro,simp] :    "X ∈ H ==> X ∈ analz H"
        Fst:     "{|X,Y|} ∈ analz H ==> X ∈ analz H"
        Snd:     "{|X,Y|} ∈ analz H ==> Y ∈ analz H"
        Decrypt [dest]:
                 "[|Crypt K X ∈ analz H; Key(invKey K): analz H|] ==> X ∈ analz H"

    text{*Monotonicity; Lemma 1 of Lowe's paper*}
    lemma analz_mono: "G⊆H ==> analz(G) ⊆ analz(H)"
    apply auto
    apply (erule analz.induct)
    apply (auto dest: analz.Fst analz.Snd)
    done

    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, standard]

    lemmas not_parts_not_analz = analz_subset_parts [THEN contra_subsetD, standard]

    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, standard]

    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 xa = 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 xa = 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 @{text "split_if"}; apparently
    @{text "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 (\<Union>i∈A. analz (H i)) ==> X∈ analz (\<Union>i∈A. H i)"
    apply (erule analz.induct)
    apply (blast intro: analz_mono [THEN [2] rev_subsetD])+
    done

    lemma analz_UN_analz [simp]: "analz (\<Union>i∈A. analz (H i)) = analz (\<Union>i∈A. H i)"
    by (blast intro: analz_UN_analz_lemma analz_mono [THEN [2] rev_subsetD])

    subsection{*Inductive relation "synth"*}

    text{*Inductive definition of "synth" -- what can be built up from a set of
        messages.  A form of upward closure.  Pairs can be built, messages
        encrypted with known keys.  Agent names are public domain.
        Numbers can be guessed, but Nonces cannot be.  *}

    consts  synth   :: "msg set => msg set"
    inductive "synth H"
      intros
        Inj    [intro]:   "X ∈ H ==> X ∈ synth H"
        Agent  [intro]:   "Agent agt ∈ synth H"
        Number [intro]:   "Number n  ∈ synth H"
        Hash   [intro]:   "X ∈ synth H ==> Hash X ∈ synth H"
        MPair  [intro]:   "[|X ∈ synth H;  Y ∈ synth H|] ==> {|X,Y|} ∈ synth H"
        Crypt  [intro]:   "[|X ∈ synth H;  Key(K) ∈ H|] ==> Crypt K X ∈ synth H"

    text{*Monotonicity*}
    lemma synth_mono: "G⊆H ==> synth(G) ⊆ synth(H)"
      by (auto, erule synth.induct, auto)

    text{*NO @{text 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

    subsubsection{*For reasoning about the Fake rule in traces *}

    lemma parts_insert_subset_Un: "X∈ G ==> parts(insert X H) ⊆ parts G ∪ parts H"
    by (rule subset_trans [OF parts_mono parts_Un_subset2], blast)

    text{*More specifically for Fake.  Very occasionally we could do with a version
      of the form  @{term"parts{X} ⊆ synth (analz H) ∪ parts H"} *}
    lemma Fake_parts_insert:
         "X ∈ synth (analz H) ==>
          parts (insert X H) ⊆ synth (analz H) ∪ parts H"
    apply (drule parts_insert_subset_Un)
    apply (simp (no_asm_use))
    apply blast
    done

    lemma Fake_parts_insert_in_Un:
         "[|Z ∈ parts (insert X H);  X: synth (analz H)|]
          ==> Z ∈  synth (analz H) ∪ parts H";
    by (blast dest: Fake_parts_insert  [THEN subsetD, dest])

    text{*@{term H} is sometimes @{term"Key ` KK ∪ spies evs"}, so can't put
      @{term "G=H"}.*}
    lemma Fake_analz_insert:
         "X∈ synth (analz G) ==>
          analz (insert X H) ⊆ synth (analz G) ∪ analz (G ∪ H)"
    apply (rule subsetI)
    apply (subgoal_tac "x ∈ analz (synth (analz G) ∪ H) ")
    prefer 2 apply (blast intro: analz_mono [THEN [2] rev_subsetD] analz_mono [THEN synth_mono, THEN [2] rev_subsetD])
    apply (simp (no_asm_use))
    apply blast
    done

    lemma analz_conj_parts [simp]:
         "(X ∈ analz H & X ∈ parts H) = (X ∈ analz H)"
    by (blast intro: analz_subset_parts [THEN subsetD])

    lemma analz_disj_parts [simp]:
         "(X ∈ analz H | X ∈ parts H) = (X ∈ parts H)"
    by (blast intro: analz_subset_parts [THEN subsetD])

    text{*Without this equation, other rules for synth and analz would yield
      redundant cases*}
    lemma MPair_synth_analz [iff]:
         "({|X,Y|} ∈ synth (analz H)) =
          (X ∈ synth (analz H) & Y ∈ synth (analz H))"
    by blast

    lemma Crypt_synth_analz:
         "[| Key K ∈ analz H;  Key (invKey K) ∈ analz H |]
           ==> (Crypt K X ∈ synth (analz H)) = (X ∈ synth (analz H))"
    by blast

    lemma Hash_synth_analz [simp]:
         "X ∉ synth (analz H)
          ==> (Hash{|X,Y|} ∈ synth (analz H)) = (Hash{|X,Y|} ∈ analz H)"
    by blast

    subsection{*HPair: a combination of Hash and MPair*}

    subsubsection{*Freeness *}

    lemma Agent_neq_HPair: "Agent A ~= Hash[X] Y"
    by (unfold HPair_def, simp)

    lemma Nonce_neq_HPair: "Nonce N ~= Hash[X] Y"
    by (unfold HPair_def, simp)

    lemma Number_neq_HPair: "Number N ~= Hash[X] Y"
    by (unfold HPair_def, simp)

    lemma Key_neq_HPair: "Key K ~= Hash[X] Y"
    by (unfold HPair_def, simp)

    lemma Hash_neq_HPair: "Hash Z ~= Hash[X] Y"
    by (unfold HPair_def, simp)

    lemma Crypt_neq_HPair: "Crypt K X' ~= Hash[X] Y"
    by (unfold HPair_def, simp)

    lemmas HPair_neqs = Agent_neq_HPair Nonce_neq_HPair Number_neq_HPair
                        Key_neq_HPair Hash_neq_HPair Crypt_neq_HPair

    declare HPair_neqs [iff]
    declare HPair_neqs [symmetric, iff]

    lemma HPair_eq [iff]: "(Hash[X'] Y' = Hash[X] Y) = (X' = X & Y'=Y)"
    by (simp add: HPair_def)

    lemma MPair_eq_HPair [iff]:
         "({|X',Y'|} = Hash[X] Y) = (X' = Hash{|X,Y|} & Y'=Y)"
    by (simp add: HPair_def)

    lemma HPair_eq_MPair [iff]:
         "(Hash[X] Y = {|X',Y'|}) = (X' = Hash{|X,Y|} & Y'=Y)"
    by (auto simp add: HPair_def)

    subsubsection{*Specialized laws, proved in terms of those for Hash and MPair *}

    lemma keysFor_insert_HPair [simp]: "keysFor (insert (Hash[X] Y) H) = keysFor H"
    by (simp add: HPair_def)

    lemma parts_insert_HPair [simp]:
        "parts (insert (Hash[X] Y) H) =
         insert (Hash[X] Y) (insert (Hash{|X,Y|}) (parts (insert Y H)))"
    by (simp add: HPair_def)

    lemma analz_insert_HPair [simp]:
        "analz (insert (Hash[X] Y) H) =
         insert (Hash[X] Y) (insert (Hash{|X,Y|}) (analz (insert Y H)))"
    by (simp add: HPair_def)

    lemma HPair_synth_analz [simp]:
         "X ∉ synth (analz H)
        ==> (Hash[X] Y ∈ synth (analz H)) =
            (Hash {|X, Y|} ∈ analz H & Y ∈ synth (analz H))"
    by (simp add: HPair_def)

    text{*We do NOT want Crypt... messages broken up in protocols!!*}
    declare parts.Body [rule del]

    text{*Rewrites to push in Key and Crypt messages, so that other messages can
        be pulled out using the @{text analz_insert} rules*}
    ML
    {*
    fun insComm x y = inst "x" x (inst "y" y insert_commute);

    bind_thms ("pushKeys",
               map (insComm "Key ?K")
                       ["Agent ?C", "Nonce ?N", "Number ?N",
                        "Hash ?X", "MPair ?X ?Y", "Crypt ?X ?K'"]);

    bind_thms ("pushCrypts",
               map (insComm "Crypt ?X ?K")
                         ["Agent ?C", "Nonce ?N", "Number ?N",
                          "Hash ?X'", "MPair ?X' ?Y"]);
    *}

    text{*Cannot be added with @{text "[simp]"} -- messages should not always be
      re-ordered. *}
    lemmas pushes = pushKeys pushCrypts

    subsection{*Tactics useful for many protocol proofs*}
    ML
    {*
    val invKey = thm "invKey"
    val keysFor_def = thm "keysFor_def"
    val HPair_def = thm "HPair_def"
    val symKeys_def = thm "symKeys_def"
    val parts_mono = thm "parts_mono";
    val analz_mono = thm "analz_mono";
    val synth_mono = thm "synth_mono";
    val analz_increasing = thm "analz_increasing";

    val analz_insertI = thm "analz_insertI";
    val analz_subset_parts = thm "analz_subset_parts";
    val Fake_parts_insert = thm "Fake_parts_insert";
    val Fake_analz_insert = thm "Fake_analz_insert";
    val pushes = thms "pushes";

    (*Prove base case (subgoal i) and simplify others.  A typical base case
      concerns  Crypt K X ∉ Key`shrK`bad  and cannot be proved by rewriting
      alone.*)
    fun prove_simple_subgoals_tac i =
        force_tac (claset(), simpset() addsimps [image_eq_UN]) i THEN
        ALLGOALS Asm_simp_tac

    (*Analysis of Fake cases.  Also works for messages that forward unknown parts,
      but this application is no longer necessary if analz_insert_eq is used.
      Abstraction over i is ESSENTIAL: it delays the dereferencing of claset
      DEPENDS UPON "X" REFERRING TO THE FRADULENT MESSAGE *)

    (*Apply rules to break down assumptions of the form
      Y ∈ parts(insert X H)  and  Y ∈ analz(insert X H)
    *)
    val Fake_insert_tac =
        dresolve_tac [impOfSubs Fake_analz_insert,
                      impOfSubs Fake_parts_insert] THEN'
        eresolve_tac [asm_rl, thm"synth.Inj"];

    fun Fake_insert_simp_tac ss i =
        REPEAT (Fake_insert_tac i) THEN asm_full_simp_tac ss i;

    fun atomic_spy_analz_tac (cs,ss) = SELECT_GOAL
        (Fake_insert_simp_tac ss 1
         THEN
         IF_UNSOLVED (Blast.depth_tac
                      (cs addIs [analz_insertI,
                                       impOfSubs analz_subset_parts]) 4 1))

    (*The explicit claset and simpset arguments help it work with Isar*)
    fun gen_spy_analz_tac (cs,ss) i =
      DETERM
       (SELECT_GOAL
         (EVERY
          [  (*push in occurrences of X...*)
           (REPEAT o CHANGED)
               (res_inst_tac [("x1","X")] (insert_commute RS ssubst) 1),
           (*...allowing further simplifications*)
           simp_tac ss 1,
           REPEAT (FIRSTGOAL (resolve_tac [allI,impI,notI,conjI,iffI])),
           DEPTH_SOLVE (atomic_spy_analz_tac (cs,ss) 1)]) i)

    fun spy_analz_tac i = gen_spy_analz_tac (claset(), simpset()) i
    *}

    text{*By default only @{text o_apply} is built-in.  But in the presence of
    eta-expansion this means that some terms displayed as @{term "f o g"} will be
    rewritten, and others will not!*}
    declare o_def [simp]

    lemma Crypt_notin_image_Key [simp]: "Crypt K X ∉ Key ` A"
    by auto

    lemma Hash_notin_image_Key [simp] :"Hash X ∉ Key ` A"
    by auto

    lemma synth_analz_mono: "G⊆H ==> synth (analz(G)) ⊆ synth (analz(H))"
    by (iprover intro: synth_mono analz_mono)

    lemma Fake_analz_eq [simp]:
         "X ∈ synth(analz H) ==> synth (analz (insert X H)) = synth (analz H)"
    apply (drule Fake_analz_insert[of _ _ "H"])
    apply (simp add: synth_increasing[THEN Un_absorb2])
    apply (drule synth_mono)
    apply (simp add: synth_idem)
    apply (rule equalityI)
    apply (simp add: );
    apply (rule synth_analz_mono, blast)
    done

    text{*Two generalizations of @{text 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)
    apply (blast intro: elim:);
    done

    lemmas Fake_parts_sing_imp_Un = Fake_parts_sing [THEN [2] rev_subsetD]

    method_setup spy_analz = {*
        Method.ctxt_args (fn ctxt =>
            Method.METHOD (fn facts =>
                gen_spy_analz_tac (local_clasimpset_of ctxt) 1)) *}
        "for proving the Fake case when analz is involved"

    method_setup atomic_spy_analz = {*
        Method.ctxt_args (fn ctxt =>
            Method.METHOD (fn facts =>
                atomic_spy_analz_tac (local_clasimpset_of ctxt) 1)) *}
        "for debugging spy_analz"

    method_setup Fake_insert_simp = {*
        Method.ctxt_args (fn ctxt =>
            Method.METHOD (fn facts =>
                Fake_insert_simp_tac (local_simpset_of ctxt) 1)) *}
        "for debugging spy_analz"

    end

lemma

      A ∪ (B ∪ A) = B ∪ A

#### Inductive Definition of All Parts" of a Message

lemma parts_mono:

      G ⊆ H ==> parts G ⊆ parts H

lemma Friend_image_eq:

      (Friend x ∈ Friend ` A) = (x ∈ A)

lemma Key_image_eq:

      (Key x ∈ Key ` A) = (x ∈ A)

lemma Nonce_Key_image_eq:

      Nonce x ∉ Key ` A

#### Inverse of keys

lemma invKey_eq:

      (invKey K = invKey K') = (K = K')

### keysFor operator

lemma keysFor_empty:

      keysFor {} = {}

lemma keysFor_Un:

      keysFor (H ∪ H') = keysFor H ∪ keysFor H'

lemma keysFor_UN:

      keysFor (UN i:A. H i) = (UN i:A. keysFor (H i))

lemma keysFor_mono:

      G ⊆ H ==> keysFor G ⊆ keysFor H

lemma keysFor_insert_Agent:

      keysFor (insert (Agent A) H) = keysFor H

lemma keysFor_insert_Nonce:

      keysFor (insert (Nonce N) H) = keysFor H

lemma keysFor_insert_Number:

      keysFor (insert (Number N) H) = keysFor H

lemma keysFor_insert_Key:

      keysFor (insert (Key K) H) = keysFor H

lemma keysFor_insert_Hash:

      keysFor (insert (Hash X) H) = keysFor H

lemma keysFor_insert_MPair:

      keysFor (insert {|X, Y|} H) = keysFor H

lemma keysFor_insert_Crypt:

      keysFor (insert (Crypt K X) H) = insert (invKey K) (keysFor H)

lemma keysFor_image_Key:

      keysFor (Key ` E) = {}

lemma Crypt_imp_invKey_keysFor:

      Crypt K X ∈ H ==> invKey K ∈ keysFor H

### Inductive relation "parts"

lemma MPair_parts:

      [| {|X, Y|} ∈ parts H; [| X ∈ parts H; Y ∈ parts H |] ==> P |] ==> P

lemma parts_increasing:

      H ⊆ parts H

lemmas parts_insertI:

      c ∈ parts G ==> c ∈ parts (insert a G)

lemmas parts_insertI:

      c ∈ parts G ==> c ∈ parts (insert a G)

lemma parts_empty:

      parts {} = {}

lemma parts_emptyE:

      X ∈ parts {} ==> P

lemma parts_singleton:

      X ∈ parts H ==> ∃Y∈H. X ∈ parts {Y}

#### Unions

lemma parts_Un_subset1:

      parts G ∪ parts H ⊆ parts (G ∪ H)

lemma parts_Un_subset2:

      parts (G ∪ H) ⊆ parts G ∪ parts H

lemma parts_Un:

      parts (G ∪ H) = parts G ∪ parts H

lemma parts_insert:

      parts (insert X H) = parts {X} ∪ parts H

lemma parts_insert2:

      parts (insert X (insert Y H)) = parts {X} ∪ parts {Y} ∪ parts H

lemma parts_UN_subset1:

      (UN x:A. parts (H x)) ⊆ parts (UN x:A. H x)

lemma parts_UN_subset2:

      parts (UN x:A. H x) ⊆ (UN x:A. parts (H x))

lemma parts_UN:

      parts (UN x:A. H x) = (UN x:A. parts (H x))

lemmas in_parts_UnE:

      [| c ∈ parts (G3 ∪ H3); c ∈ parts G3 ==> P; c ∈ parts H3 ==> P |] ==> P

lemmas in_parts_UnE:

      [| c ∈ parts (G3 ∪ H3); c ∈ parts G3 ==> P; c ∈ parts H3 ==> P |] ==> P

lemma parts_insert_subset:

      insert X (parts H) ⊆ parts (insert X H)

#### Idempotence and transitivity

lemma parts_partsD:

      X ∈ parts (parts H) ==> X ∈ parts H

lemma parts_idem:

      parts (parts H) = parts H

lemma parts_subset_iff:

      (parts G ⊆ parts H) = (G ⊆ parts H)

lemma parts_trans:

      [| X ∈ parts G; G ⊆ parts H |] ==> X ∈ parts H

lemma parts_cut:

      [| Y ∈ parts (insert X G); X ∈ parts H |] ==> Y ∈ parts (G ∪ H)

lemma parts_cut_eq:

      X ∈ parts H ==> parts (insert X H) = parts H

#### Rewrite rules for pulling out atomic messages

lemmas parts_insert_eq_I:

      (!!x. x ∈ parts (insert X1 H1) ==> x ∈ insert X1 (parts H1))
      ==> parts (insert X1 H1) = insert X1 (parts H1)

lemmas parts_insert_eq_I:

      (!!x. x ∈ parts (insert X1 H1) ==> x ∈ insert X1 (parts H1))
      ==> parts (insert X1 H1) = insert X1 (parts H1)

lemma parts_insert_Agent:

      parts (insert (Agent agt) H) = insert (Agent agt) (parts H)

lemma parts_insert_Nonce:

      parts (insert (Nonce N) H) = insert (Nonce N) (parts H)

lemma parts_insert_Number:

      parts (insert (Number N) H) = insert (Number N) (parts H)

lemma parts_insert_Key:

      parts (insert (Key K) H) = insert (Key K) (parts H)

lemma parts_insert_Hash:

      parts (insert (Hash X) H) = insert (Hash X) (parts H)

lemma parts_insert_Crypt:

      parts (insert (Crypt K X) H) = insert (Crypt K X) (parts (insert X H))

lemma parts_insert_MPair:

      parts (insert {|X, Y|} H) = insert {|X, Y|} (parts (insert X (insert Y H)))

lemma parts_image_Key:

      parts (Key ` N) = Key ` N

lemma msg_Nonce_supply:

      ∃N. ∀n. N ≤ n --> Nonce n ∉ parts {msg}

### Inductive relation "analz"

lemma analz_mono:

      G ⊆ H ==> analz G ⊆ analz H

lemma MPair_analz:

      [| {|X, Y|} ∈ analz H; [| X ∈ analz H; Y ∈ analz H |] ==> P |] ==> P

lemma analz_increasing:

      H ⊆ analz H

lemma analz_subset_parts:

      analz H ⊆ parts H

lemmas analz_into_parts:

      c ∈ analz H ==> c ∈ parts H

lemmas analz_into_parts:

      c ∈ analz H ==> c ∈ parts H

lemmas not_parts_not_analz:

      c ∉ parts H ==> c ∉ analz H

lemmas not_parts_not_analz:

      c ∉ parts H ==> c ∉ analz H

lemma parts_analz:

      parts (analz H) = parts H

lemma analz_parts:

      analz (parts H) = parts H

lemmas analz_insertI:

      c ∈ analz G ==> c ∈ analz (insert a G)

lemmas analz_insertI:

      c ∈ analz G ==> c ∈ analz (insert a G)

#### General equational properties

lemma analz_empty:

      analz {} = {}

lemma analz_Un:

      analz G ∪ analz H ⊆ analz (G ∪ H)

lemma analz_insert:

      insert X (analz H) ⊆ analz (insert X H)

#### Rewrite rules for pulling out atomic messages

lemmas analz_insert_eq_I:

      (!!x. x ∈ analz (insert X1 H1) ==> x ∈ insert X1 (analz H1))
      ==> analz (insert X1 H1) = insert X1 (analz H1)

lemmas analz_insert_eq_I:

      (!!x. x ∈ analz (insert X1 H1) ==> x ∈ insert X1 (analz H1))
      ==> analz (insert X1 H1) = insert X1 (analz H1)

lemma analz_insert_Agent:

      analz (insert (Agent agt) H) = insert (Agent agt) (analz H)

lemma analz_insert_Nonce:

      analz (insert (Nonce N) H) = insert (Nonce N) (analz H)

lemma analz_insert_Number:

      analz (insert (Number N) H) = insert (Number N) (analz H)

lemma analz_insert_Hash:

      analz (insert (Hash X) H) = insert (Hash X) (analz H)

lemma analz_insert_Key:

      K ∉ keysFor (analz H) ==> analz (insert (Key K) H) = insert (Key K) (analz H)

lemma analz_insert_MPair:

      analz (insert {|X, Y|} H) = insert {|X, Y|} (analz (insert X (insert Y H)))

lemma analz_insert_Crypt:

      Key (invKey K) ∉ analz H
      ==> analz (insert (Crypt K X) H) = insert (Crypt K X) (analz H)

lemma lemma1:

      Key (invKey K) ∈ analz H
      ==> analz (insert (Crypt K X) H) ⊆ insert (Crypt K X) (analz (insert X H))

lemma lemma2:

      Key (invKey K) ∈ analz H
      ==> insert (Crypt K X) (analz (insert X H)) ⊆ analz (insert (Crypt K X) H)

lemma analz_insert_Decrypt:

      Key (invKey K) ∈ analz H
      ==> analz (insert (Crypt K X) H) = insert (Crypt K X) (analz (insert X H))

lemma analz_Crypt_if:

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

lemma analz_insert_Crypt_subset:

      analz (insert (Crypt K X) H) ⊆ insert (Crypt K X) (analz (insert X H))

lemma analz_image_Key:

      analz (Key ` N) = Key ` N

#### Idempotence and transitivity

lemma analz_analzD:

      X ∈ analz (analz H) ==> X ∈ analz H

lemma analz_idem:

      analz (analz H) = analz H

lemma analz_subset_iff:

      (analz G ⊆ analz H) = (G ⊆ analz H)

lemma analz_trans:

      [| X ∈ analz G; G ⊆ analz H |] ==> X ∈ analz H

lemma analz_cut:

      [| Y ∈ analz (insert X H); X ∈ analz H |] ==> Y ∈ analz H

lemma analz_insert_eq:

      X ∈ analz H ==> analz (insert X H) = analz H

lemma analz_subset_cong:

      [| analz G ⊆ analz G'; analz H ⊆ analz H' |] ==> analz (G ∪ H) ⊆ analz (G' ∪ H')

lemma analz_cong:

      [| analz G = analz G'; analz H = analz H' |] ==> analz (G ∪ H) = analz (G' ∪ H')

lemma analz_insert_cong:

      analz H = analz H' ==> analz (insert X H) = analz (insert X H')

lemma analz_trivial:

      [| ∀X Y. {|X, Y|} ∉ H; ∀X K. Crypt K X ∉ H |] ==> analz H = H

lemma analz_UN_analz_lemma:

      X ∈ analz (UN i:A. analz (H i)) ==> X ∈ analz (UN i:A. H i)

lemma analz_UN_analz:

      analz (UN i:A. analz (H i)) = analz (UN i:A. H i)

### Inductive relation "synth"

lemma synth_mono:

      G ⊆ H ==> synth G ⊆ synth H

lemmas Nonce_synth:

      [| Nonce n ∈ synth H; Nonce n ∈ H ==> P |] ==> P

lemmas Key_synth:

      [| Key K ∈ synth H; Key K ∈ H ==> P |] ==> P

lemmas Hash_synth:

      [| Hash X ∈ synth H; Hash X ∈ H ==> P; X ∈ synth H ==> P |] ==> P

lemmas MPair_synth:

      [| {|X, Y|} ∈ synth H; {|X, Y|} ∈ H ==> P;
         [| X ∈ synth H; Y ∈ synth H |] ==> P |]
      ==> P

lemmas Crypt_synth:

      [| Crypt K X ∈ synth H; Crypt K X ∈ H ==> P;
         [| X ∈ synth H; Key K ∈ H |] ==> P |]
      ==> P

lemma synth_increasing:

      H ⊆ synth H

#### Unions

lemma synth_Un:

      synth G ∪ synth H ⊆ synth (G ∪ H)

lemma synth_insert:

      insert X (synth H) ⊆ synth (insert X H)

#### Idempotence and transitivity

lemma synth_synthD:

      X ∈ synth (synth H) ==> X ∈ synth H

lemma synth_idem:

      synth (synth H) = synth H

lemma synth_subset_iff:

      (synth G ⊆ synth H) = (G ⊆ synth H)

lemma synth_trans:

      [| X ∈ synth G; G ⊆ synth H |] ==> X ∈ synth H

lemma synth_cut:

      [| Y ∈ synth (insert X H); X ∈ synth H |] ==> Y ∈ synth H

lemma Agent_synth:

      Agent A ∈ synth H

lemma Number_synth:

      Number n ∈ synth H

lemma Nonce_synth_eq:

      (Nonce N ∈ synth H) = (Nonce N ∈ H)

lemma Key_synth_eq:

      (Key K ∈ synth H) = (Key K ∈ H)

lemma Crypt_synth_eq:

      Key K ∉ H ==> (Crypt K X ∈ synth H) = (Crypt K X ∈ H)

lemma keysFor_synth:

      keysFor (synth H) = keysFor H ∪ invKey ` {K. Key K ∈ H}

#### Combinations of parts, analz and synth

lemma parts_synth:

      parts (synth H) = parts H ∪ synth H

lemma analz_analz_Un:

      analz (analz G ∪ H) = analz (G ∪ H)

lemma analz_synth_Un:

      analz (synth G ∪ H) = analz (G ∪ H) ∪ synth G

lemma analz_synth:

      analz (synth H) = analz H ∪ synth H

#### For reasoning about the Fake rule in traces

lemma parts_insert_subset_Un:

      X ∈ G ==> parts (insert X H) ⊆ parts G ∪ parts H

lemma Fake_parts_insert:

      X ∈ synth (analz H) ==> parts (insert X H) ⊆ synth (analz H) ∪ parts H

lemma Fake_parts_insert_in_Un:

      [| Z ∈ parts (insert X H); X ∈ synth (analz H) |]
      ==> Z ∈ synth (analz H) ∪ parts H

lemma Fake_analz_insert:

      X ∈ synth (analz G) ==> analz (insert X H) ⊆ synth (analz G) ∪ analz (G ∪ H)

lemma analz_conj_parts:

      (X ∈ analz H ∧ X ∈ parts H) = (X ∈ analz H)

lemma analz_disj_parts:

      (X ∈ analz H ∨ X ∈ parts H) = (X ∈ parts H)

lemma MPair_synth_analz:

      ({|X, Y|} ∈ synth (analz H)) = (X ∈ synth (analz H) ∧ Y ∈ synth (analz H))

lemma Crypt_synth_analz:

      [| Key K ∈ analz H; Key (invKey K) ∈ analz H |]
      ==> (Crypt K X ∈ synth (analz H)) = (X ∈ synth (analz H))

lemma Hash_synth_analz:

      X ∉ synth (analz H)
      ==> (Hash {|X, Y|} ∈ synth (analz H)) = (Hash {|X, Y|} ∈ analz H)

### HPair: a combination of Hash and MPair

#### Freeness

lemma Agent_neq_HPair:

      Agent A ≠ Hash[X] Y

lemma Nonce_neq_HPair:

      Nonce N ≠ Hash[X] Y

lemma Number_neq_HPair:

      Number N ≠ Hash[X] Y

lemma Key_neq_HPair:

      Key K ≠ Hash[X] Y

lemma Hash_neq_HPair:

      Hash Z ≠ Hash[X] Y

lemma Crypt_neq_HPair:

      Crypt K X' ≠ Hash[X] Y

lemmas HPair_neqs:

      Agent A ≠ Hash[X] Y

      Nonce N ≠ Hash[X] Y

      Number N ≠ Hash[X] Y

      Key K ≠ Hash[X] Y

      Hash Z ≠ Hash[X] Y

      Crypt K X' ≠ Hash[X] Y

lemmas HPair_neqs:

      Agent A ≠ Hash[X] Y

      Nonce N ≠ Hash[X] Y

      Number N ≠ Hash[X] Y

      Key K ≠ Hash[X] Y

      Hash Z ≠ Hash[X] Y

      Crypt K X' ≠ Hash[X] Y

lemma HPair_eq:

      (Hash[X'] Y' = Hash[X] Y) = (X' = X ∧ Y' = Y)

lemma MPair_eq_HPair:

      ({|X', Y'|} = Hash[X] Y) = (X' = Hash {|X, Y|} ∧ Y' = Y)

lemma HPair_eq_MPair:

      (Hash[X] Y = {|X', Y'|}) = (X' = Hash {|X, Y|} ∧ Y' = Y)

#### Specialized laws, proved in terms of those for Hash and MPair

lemma keysFor_insert_HPair:

      keysFor (insert Hash[X] Y H) = keysFor H

lemma parts_insert_HPair:

      parts (insert Hash[X] Y H) =
      insert Hash[X] Y (insert (Hash {|X, Y|}) (parts (insert Y H)))

lemma analz_insert_HPair:

      analz (insert Hash[X] Y H) =
      insert Hash[X] Y (insert (Hash {|X, Y|}) (analz (insert Y H)))

lemma HPair_synth_analz:

      X ∉ synth (analz H)
      ==> (Hash[X] Y ∈ synth (analz H)) =
          (Hash {|X, Y|} ∈ analz H ∧ Y ∈ synth (analz H))

theorems pushKeys:

      insert (Key K) (insert (Agent C) A) = insert (Agent C) (insert (Key K) A)

      insert (Key K) (insert (Nonce N) A) = insert (Nonce N) (insert (Key K) A)

      insert (Key K) (insert (Number N) A) = insert (Number N) (insert (Key K) A)

      insert (Key K) (insert (Hash X) A) = insert (Hash X) (insert (Key K) A)

      insert (Key K) (insert {|X, Y|} A) = insert {|X, Y|} (insert (Key K) A)

      insert (Key K) (insert (Crypt X K') A) = insert (Crypt X K') (insert (Key K) A)

theorems pushCrypts:

      insert (Crypt X K) (insert (Agent C) A) =
      insert (Agent C) (insert (Crypt X K) A)

      insert (Crypt X K) (insert (Nonce N) A) =
      insert (Nonce N) (insert (Crypt X K) A)

      insert (Crypt X K) (insert (Number N) A) =
      insert (Number N) (insert (Crypt X K) A)

      insert (Crypt X K) (insert (Hash X') A) =
      insert (Hash X') (insert (Crypt X K) A)

      insert (Crypt X K) (insert {|X', Y|} A) =
      insert {|X', Y|} (insert (Crypt X K) A)

lemmas pushes:

      insert (Key K) (insert (Agent C) A) = insert (Agent C) (insert (Key K) A)

      insert (Key K) (insert (Nonce N) A) = insert (Nonce N) (insert (Key K) A)

      insert (Key K) (insert (Number N) A) = insert (Number N) (insert (Key K) A)

      insert (Key K) (insert (Hash X) A) = insert (Hash X) (insert (Key K) A)

      insert (Key K) (insert {|X, Y|} A) = insert {|X, Y|} (insert (Key K) A)

      insert (Key K) (insert (Crypt X K') A) = insert (Crypt X K') (insert (Key K) A)

      insert (Crypt X K) (insert (Agent C) A) =
      insert (Agent C) (insert (Crypt X K) A)

      insert (Crypt X K) (insert (Nonce N) A) =
      insert (Nonce N) (insert (Crypt X K) A)

      insert (Crypt X K) (insert (Number N) A) =
      insert (Number N) (insert (Crypt X K) A)

      insert (Crypt X K) (insert (Hash X') A) =
      insert (Hash X') (insert (Crypt X K) A)

      insert (Crypt X K) (insert {|X', Y|} A) =
      insert {|X', Y|} (insert (Crypt X K) A)

lemmas pushes:

      insert (Key K) (insert (Agent C) A) = insert (Agent C) (insert (Key K) A)

      insert (Key K) (insert (Nonce N) A) = insert (Nonce N) (insert (Key K) A)

      insert (Key K) (insert (Number N) A) = insert (Number N) (insert (Key K) A)

      insert (Key K) (insert (Hash X) A) = insert (Hash X) (insert (Key K) A)

      insert (Key K) (insert {|X, Y|} A) = insert {|X, Y|} (insert (Key K) A)

      insert (Key K) (insert (Crypt X K') A) = insert (Crypt X K') (insert (Key K) A)

      insert (Crypt X K) (insert (Agent C) A) =
      insert (Agent C) (insert (Crypt X K) A)

      insert (Crypt X K) (insert (Nonce N) A) =
      insert (Nonce N) (insert (Crypt X K) A)

      insert (Crypt X K) (insert (Number N) A) =
      insert (Number N) (insert (Crypt X K) A)

      insert (Crypt X K) (insert (Hash X') A) =
      insert (Hash X') (insert (Crypt X K) A)

      insert (Crypt X K) (insert {|X', Y|} A) =
      insert {|X', Y|} (insert (Crypt X K) A)

### Tactics useful for many protocol proofs

lemma Crypt_notin_image_Key:

      Crypt K X ∉ Key ` A

lemma Hash_notin_image_Key:

      Hash X ∉ Key ` A

lemma synth_analz_mono:

      G ⊆ H ==> synth (analz G) ⊆ synth (analz H)

lemma Fake_analz_eq:

      X ∈ synth (analz H) ==> synth (analz (insert X H)) = synth (analz H)

lemma gen_analz_insert_eq:

      [| X ∈ analz H; H ⊆ G |] ==> analz (insert X G) = analz G

lemma synth_analz_insert_eq:

      [| X ∈ synth (analz H); H ⊆ G |]
      ==> (Key K ∈ analz (insert X G)) = (Key K ∈ analz G)

lemma Fake_parts_sing:

      X ∈ synth (analz H) ==> parts {X} ⊆ synth (analz H) ∪ parts H

lemmas Fake_parts_sing_imp_Un:

      [| c ∈ parts {X1}; X1 ∈ synth (analz H1) |] ==> c ∈ synth (analz H1) ∪ parts H1

lemmas Fake_parts_sing_imp_Un:

      [| c ∈ parts {X1}; X1 ∈ synth (analz H1) |] ==> c ∈ synth (analz H1) ∪ parts H1