# Theory Shared

Up to index of Isabelle/HOL/Auth

theory Shared
imports Event
begin

    (*  Title:      HOL/Auth/Shared
        ID:         $Id: Shared.thy,v 1.34 2005/06/17 14:13:06 haftmann Exp $
        Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
        Copyright   1996  University of Cambridge

    Theory of Shared Keys (common to all symmetric-key protocols)

    Shared, long-term keys; initial states of agents
    *)

    theory Shared imports Event begin

    consts
      shrK    :: "agent => key"  (*symmetric keys*);

    specification (shrK)
      inj_shrK: "inj shrK"
      --{*No two agents have the same long-term key*}
       apply (rule exI [of _ "agent_case 0 (λn. n + 2) 1"])
       apply (simp add: inj_on_def split: agent.split)
       done

    text{*All keys are symmetric*}

    defs  all_symmetric_def: "all_symmetric == True"

    lemma isSym_keys: "K ∈ symKeys"
    by (simp add: symKeys_def all_symmetric_def invKey_symmetric)

    text{*Server knows all long-term keys; other agents know only their own*}
    primrec
      initState_Server:  "initState Server     = Key ` range shrK"
      initState_Friend:  "initState (Friend i) = {Key (shrK (Friend i))}"
      initState_Spy:     "initState Spy        = Key`shrK`bad"

    subsection{*Basic properties of shrK*}

    (*Injectiveness: Agents' long-term keys are distinct.*)
    declare inj_shrK [THEN inj_eq, iff]

    lemma invKey_K [simp]: "invKey K = K"
    apply (insert isSym_keys)
    apply (simp add: symKeys_def)
    done

    lemma analz_Decrypt' [dest]:
         "[| Crypt K X ∈ analz H;  Key K  ∈ analz H |] ==> X ∈ analz H"
    by auto

    text{*Now cancel the @{text dest} attribute given to
     @{text analz.Decrypt} in its declaration.*}
    declare analz.Decrypt [rule del]

    text{*Rewrites should not refer to  @{term "initState(Friend i)"} because
      that expression is not in normal form.*}

    lemma keysFor_parts_initState [simp]: "keysFor (parts (initState C)) = {}"
    apply (unfold keysFor_def)
    apply (induct_tac "C", auto)
    done

    (*Specialized to shared-key model: no @{term invKey}*)
    lemma keysFor_parts_insert:
         "[| K ∈ keysFor (parts (insert X G));  X ∈ synth (analz H) |]
          ==> K ∈ keysFor (parts (G ∪ H)) | Key K ∈ parts H";
    by (force dest: Event.keysFor_parts_insert)

    lemma Crypt_imp_keysFor: "Crypt K X ∈ H ==> K ∈ keysFor H"
    by (drule Crypt_imp_invKey_keysFor, simp)

    subsection{*Function "knows"*}

    (*Spy sees shared keys of agents!*)
    lemma Spy_knows_Spy_bad [intro!]: "A: bad ==> Key (shrK A) ∈ knows Spy evs"
    apply (induct_tac "evs")
    apply (simp_all (no_asm_simp) add: imageI knows_Cons split add: event.split)
    done

    (*For case analysis on whether or not an agent is compromised*)
    lemma Crypt_Spy_analz_bad: "[| Crypt (shrK A) X ∈ analz (knows Spy evs);  A: bad |]
          ==> X ∈ analz (knows Spy evs)"
    apply (force dest!: analz.Decrypt)
    done

    (** Fresh keys never clash with long-term shared keys **)

    (*Agents see their own shared keys!*)
    lemma shrK_in_initState [iff]: "Key (shrK A) ∈ initState A"
    by (induct_tac "A", auto)

    lemma shrK_in_used [iff]: "Key (shrK A) ∈ used evs"
    by (rule initState_into_used, blast)

    (*Used in parts_induct_tac and analz_Fake_tac to distinguish session keys
      from long-term shared keys*)
    lemma Key_not_used [simp]: "Key K ∉ used evs ==> K ∉ range shrK"
    by blast

    lemma shrK_neq [simp]: "Key K ∉ used evs ==> shrK B ≠ K"
    by blast

    declare shrK_neq [THEN not_sym, simp]

    subsection{*Fresh nonces*}

    lemma Nonce_notin_initState [iff]: "Nonce N ∉ parts (initState B)"
    by (induct_tac "B", auto)

    lemma Nonce_notin_used_empty [simp]: "Nonce N ∉ used []"
    apply (simp (no_asm) add: used_Nil)
    done

    subsection{*Supply fresh nonces for possibility theorems.*}

    (*In any trace, there is an upper bound N on the greatest nonce in use.*)
    lemma Nonce_supply_lemma: "∃N. ALL n. N<=n --> Nonce n ∉ used evs"
    apply (induct_tac "evs")
    apply (rule_tac x = 0 in exI)
    apply (simp_all (no_asm_simp) add: used_Cons split add: event.split)
    apply safe
    apply (rule msg_Nonce_supply [THEN exE], blast elim!: add_leE)+
    done

    lemma Nonce_supply1: "∃N. Nonce N ∉ used evs"
    by (rule Nonce_supply_lemma [THEN exE], blast)

    lemma Nonce_supply2: "∃N N'. Nonce N ∉ used evs & Nonce N' ∉ used evs' & N ≠ N'"
    apply (cut_tac evs = evs in Nonce_supply_lemma)
    apply (cut_tac evs = "evs'" in Nonce_supply_lemma, clarify)
    apply (rule_tac x = N in exI)
    apply (rule_tac x = "Suc (N+Na)" in exI)
    apply (simp (no_asm_simp) add: less_not_refl3 le_add1 le_add2 less_Suc_eq_le)
    done

    lemma Nonce_supply3: "∃N N' N''. Nonce N ∉ used evs & Nonce N' ∉ used evs' &
                        Nonce N'' ∉ used evs'' & N ≠ N' & N' ≠ N'' & N ≠ N''"
    apply (cut_tac evs = evs in Nonce_supply_lemma)
    apply (cut_tac evs = "evs'" in Nonce_supply_lemma)
    apply (cut_tac evs = "evs''" in Nonce_supply_lemma, clarify)
    apply (rule_tac x = N in exI)
    apply (rule_tac x = "Suc (N+Na)" in exI)
    apply (rule_tac x = "Suc (Suc (N+Na+Nb))" in exI)
    apply (simp (no_asm_simp) add: less_not_refl3 le_add1 le_add2 less_Suc_eq_le)
    done

    lemma Nonce_supply: "Nonce (@ N. Nonce N ∉ used evs) ∉ used evs"
    apply (rule Nonce_supply_lemma [THEN exE])
    apply (rule someI, blast)
    done

    text{*Unlike the corresponding property of nonces, we cannot prove
        @{term "finite KK ==> ∃K. K ∉ KK & Key K ∉ used evs"}.
        We have infinitely many agents and there is nothing to stop their
        long-term keys from exhausting all the natural numbers.  Instead,
        possibility theorems must assume the existence of a few keys.*}

    subsection{*Tactics for possibility theorems*}

    ML
    {*
    val inj_shrK      = thm "inj_shrK";
    val isSym_keys    = thm "isSym_keys";
    val Nonce_supply = thm "Nonce_supply";
    val invKey_K = thm "invKey_K";
    val analz_Decrypt' = thm "analz_Decrypt'";
    val keysFor_parts_initState = thm "keysFor_parts_initState";
    val keysFor_parts_insert = thm "keysFor_parts_insert";
    val Crypt_imp_keysFor = thm "Crypt_imp_keysFor";
    val Spy_knows_Spy_bad = thm "Spy_knows_Spy_bad";
    val Crypt_Spy_analz_bad = thm "Crypt_Spy_analz_bad";
    val shrK_in_initState = thm "shrK_in_initState";
    val shrK_in_used = thm "shrK_in_used";
    val Key_not_used = thm "Key_not_used";
    val shrK_neq = thm "shrK_neq";
    val Nonce_notin_initState = thm "Nonce_notin_initState";
    val Nonce_notin_used_empty = thm "Nonce_notin_used_empty";
    val Nonce_supply_lemma = thm "Nonce_supply_lemma";
    val Nonce_supply1 = thm "Nonce_supply1";
    val Nonce_supply2 = thm "Nonce_supply2";
    val Nonce_supply3 = thm "Nonce_supply3";
    val Nonce_supply = thm "Nonce_supply";
    *}

    ML
    {*
    (*Omitting used_Says makes the tactic much faster: it leaves expressions
        such as  Nonce ?N ∉ used evs that match Nonce_supply*)
    fun gen_possibility_tac ss state = state |>
       (REPEAT
        (ALLGOALS (simp_tac (ss delsimps [used_Says, used_Notes, used_Gets]
                             setSolver safe_solver))
         THEN
         REPEAT_FIRST (eq_assume_tac ORELSE'
                       resolve_tac [refl, conjI, Nonce_supply])))

    (*Tactic for possibility theorems (ML script version)*)
    fun possibility_tac state = gen_possibility_tac (simpset()) state

    (*For harder protocols (such as Recur) where we have to set up some
      nonces and keys initially*)
    fun basic_possibility_tac st = st |>
        REPEAT
        (ALLGOALS (asm_simp_tac (simpset() setSolver safe_solver))
         THEN
         REPEAT_FIRST (resolve_tac [refl, conjI]))
    *}

    subsection{*Specialized Rewriting for Theorems About @{term analz} and Image*}

    lemma subset_Compl_range: "A <= - (range shrK) ==> shrK x ∉ A"
    by blast

    lemma insert_Key_singleton: "insert (Key K) H = Key ` {K} ∪ H"
    by blast

    lemma insert_Key_image: "insert (Key K) (Key`KK ∪ C) = Key`(insert K KK) ∪ C"
    by blast

    (** Reverse the normal simplification of "image" to build up (not break down)
        the set of keys.  Use analz_insert_eq with (Un_upper2 RS analz_mono) to
        erase occurrences of forwarded message components (X). **)

    lemmas analz_image_freshK_simps =
           simp_thms mem_simps --{*these two allow its use with @{text "only:"}*}
           disj_comms
           image_insert [THEN sym] image_Un [THEN sym] empty_subsetI insert_subset
           analz_insert_eq Un_upper2 [THEN analz_mono, THEN [2] rev_subsetD]
           insert_Key_singleton subset_Compl_range
           Key_not_used insert_Key_image Un_assoc [THEN sym]

    (*Lemma for the trivial direction of the if-and-only-if*)
    lemma analz_image_freshK_lemma:
         "(Key K ∈ analz (Key`nE ∪ H)) --> (K ∈ nE | Key K ∈ analz H)  ==>
             (Key K ∈ analz (Key`nE ∪ H)) = (K ∈ nE | Key K ∈ analz H)"
    by (blast intro: analz_mono [THEN [2] rev_subsetD])

    ML
    {*
    val analz_image_freshK_lemma = thm "analz_image_freshK_lemma";

    val analz_image_freshK_ss =
         simpset() delsimps [image_insert, image_Un]
                   delsimps [imp_disjL]    (*reduces blow-up*)
                   addsimps thms "analz_image_freshK_simps"
    *}

    (*Lets blast_tac perform this step without needing the simplifier*)
    lemma invKey_shrK_iff [iff]:
         "(Key (invKey K) ∈ X) = (Key K ∈ X)"
    by auto

    (*Specialized methods*)

    method_setup analz_freshK = {*
        Method.no_args
         (Method.METHOD
          (fn facts => EVERY [REPEAT_FIRST (resolve_tac [allI, ballI, impI]),
                              REPEAT_FIRST (rtac analz_image_freshK_lemma),
                              ALLGOALS (asm_simp_tac analz_image_freshK_ss)])) *}
        "for proving the Session Key Compromise theorem"

    method_setup possibility = {*
        Method.ctxt_args (fn ctxt =>
            Method.METHOD (fn facts =>
                gen_possibility_tac (local_simpset_of ctxt))) *}
        "for proving possibility theorems"

    lemma knows_subset_knows_Cons: "knows A evs <= knows A (e # evs)"
    by (induct e, auto simp: knows_Cons)

    end

lemma isSym_keys:

      K ∈ symKeys

### Basic properties of shrK

lemma invKey_K:

      invKey K = K

lemma analz_Decrypt':

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

lemma keysFor_parts_initState:

      keysFor (parts (initState C)) = {}

lemma keysFor_parts_insert:

      [| K ∈ keysFor (parts (insert X G)); X ∈ synth (analz H) |]
      ==> K ∈ keysFor (parts (G ∪ H)) ∨ Key K ∈ parts H

lemma Crypt_imp_keysFor:

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

### Function "knows"

lemma Spy_knows_Spy_bad:

      A ∈ bad ==> Key (shrK A) ∈ knows Spy evs

lemma Crypt_Spy_analz_bad:

      [| Crypt (shrK A) X ∈ analz (knows Spy evs); A ∈ bad |]
      ==> X ∈ analz (knows Spy evs)

lemma shrK_in_initState:

      Key (shrK A) ∈ initState A

lemma shrK_in_used:

      Key (shrK A) ∈ used evs

lemma Key_not_used:

      Key K ∉ used evs ==> K ∉ range shrK

lemma shrK_neq:

      Key K ∉ used evs ==> shrK B ≠ K

### Fresh nonces

lemma Nonce_notin_initState:

      Nonce N ∉ parts (initState B)

lemma Nonce_notin_used_empty:

      Nonce N ∉ used []

### Supply fresh nonces for possibility theorems.

lemma Nonce_supply_lemma:

      ∃N. ∀n. N ≤ n --> Nonce n ∉ used evs

lemma Nonce_supply1:

      ∃N. Nonce N ∉ used evs

lemma Nonce_supply2:

      ∃N N'. Nonce N ∉ used evs ∧ Nonce N' ∉ used evs' ∧ N ≠ N'

lemma Nonce_supply3:

      ∃N N' N''.
         Nonce N ∉ used evs ∧
         Nonce N' ∉ used evs' ∧ Nonce N'' ∉ used evs'' ∧ N ≠ N' ∧ N' ≠ N'' ∧ N ≠ N''

lemma Nonce_supply:

      Nonce (SOME N. Nonce N ∉ used evs) ∉ used evs

### Tactics for possibility theorems

### Specialized Rewriting for Theorems About @{term analz} and Image

lemma subset_Compl_range:

      A ⊆ - range shrK ==> shrK x ∉ A

lemma insert_Key_singleton:

      insert (Key K) H = Key ` {K} ∪ H

lemma insert_Key_image:

      insert (Key K) (Key ` KK ∪ C) = Key ` insert K KK ∪ C

lemmas analz_image_freshK_simps:

      (¬ ¬ P) = P

      ((¬ P) = (¬ Q)) = (P = Q)

      (P ≠ Q) = (P = (¬ Q))

      (P ∨ ¬ P) = True

      (¬ P ∨ P) = True

      (x = x) = True

      (¬ True) = False

      (¬ False) = True

      (¬ P) ≠ P

      P ≠ (¬ P)

      (True = P) = P

      (P = True) = P

      (False = P) = (¬ P)

      (P = False) = (¬ P)

      (True --> P) = P

      (False --> P) = True

      (P --> True) = True

      (P --> P) = True

      (P --> False) = (¬ P)

      (P --> ¬ P) = (¬ P)

      (P ∧ True) = P

      (True ∧ P) = P

      (P ∧ False) = False

      (False ∧ P) = False

      (P ∧ P) = P

      (P ∧ P ∧ Q) = (P ∧ Q)

      (P ∧ ¬ P) = False

      (¬ P ∧ P) = False

      (P ∨ True) = True

      (True ∨ P) = True

      (P ∨ False) = P

      (False ∨ P) = P

      (P ∨ P) = P

      (P ∨ P ∨ Q) = (P ∨ Q)

      (∀x. P) = P

      (∃x. P) = P

      ∃x. x = t

      ∃x. t = x

      (∃x. x = t ∧ P x) = P t

      (∃x. t = x ∧ P x) = P t

      (∀x. x = t --> P x) = P t

      (∀x. t = x --> P x) = P t

      (a ∈ insert b A) = (a = b ∨ a ∈ A)

      (c ∈ {}) = False

      (c ∈ A ∪ B) = (c ∈ A ∨ c ∈ B)

      (c ∈ A ∩ B) = (c ∈ A ∧ c ∈ B)

      (c ∈ - A) = (c ∉ A)

      (c ∈ A - B) = (c ∈ A ∧ c ∉ B)

      (a ∈ {x. P x}) = P a

      (b ∈ (UN x:A. B x)) = (∃x∈A. b ∈ B x)

      (A ∈ Union C) = (∃X∈C. A ∈ X)

      (b ∈ (INT x:A. B x)) = (∀x∈A. b ∈ B x)

      (A ∈ Inter C) = (∀X∈C. A ∈ X)

      (P ∨ Q) = (Q ∨ P)

      (P ∨ Q ∨ R) = (Q ∨ P ∨ R)

      insert (f1 a1) (f1 ` B1) = f1 ` insert a1 B1

      f1 ` A1 ∪ f1 ` B1 = f1 ` (A1 ∪ B1)

      {} ⊆ A

      (insert x A ⊆ B) = (x ∈ B ∧ A ⊆ B)

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

      c ∈ analz G1 ==> c ∈ analz (A2 ∪ G1)

      insert (Key K) H = Key ` {K} ∪ H

      A ⊆ - range shrK ==> shrK x ∉ A

      Key K ∉ used evs ==> K ∉ range shrK

      insert (Key K) (Key ` KK ∪ C) = Key ` insert K KK ∪ C

      A1 ∪ (B1 ∪ C1) = A1 ∪ B1 ∪ C1

lemmas analz_image_freshK_simps:

      (¬ ¬ P) = P

      ((¬ P) = (¬ Q)) = (P = Q)

      (P ≠ Q) = (P = (¬ Q))

      (P ∨ ¬ P) = True

      (¬ P ∨ P) = True

      (x = x) = True

      (¬ True) = False

      (¬ False) = True

      (¬ P) ≠ P

      P ≠ (¬ P)

      (True = P) = P

      (P = True) = P

      (False = P) = (¬ P)

      (P = False) = (¬ P)

      (True --> P) = P

      (False --> P) = True

      (P --> True) = True

      (P --> P) = True

      (P --> False) = (¬ P)

      (P --> ¬ P) = (¬ P)

      (P ∧ True) = P

      (True ∧ P) = P

      (P ∧ False) = False

      (False ∧ P) = False

      (P ∧ P) = P

      (P ∧ P ∧ Q) = (P ∧ Q)

      (P ∧ ¬ P) = False

      (¬ P ∧ P) = False

      (P ∨ True) = True

      (True ∨ P) = True

      (P ∨ False) = P

      (False ∨ P) = P

      (P ∨ P) = P

      (P ∨ P ∨ Q) = (P ∨ Q)

      (∀x. P) = P

      (∃x. P) = P

      ∃x. x = t

      ∃x. t = x

      (∃x. x = t ∧ P x) = P t

      (∃x. t = x ∧ P x) = P t

      (∀x. x = t --> P x) = P t

      (∀x. t = x --> P x) = P t

      (a ∈ insert b A) = (a = b ∨ a ∈ A)

      (c ∈ {}) = False

      (c ∈ A ∪ B) = (c ∈ A ∨ c ∈ B)

      (c ∈ A ∩ B) = (c ∈ A ∧ c ∈ B)

      (c ∈ - A) = (c ∉ A)

      (c ∈ A - B) = (c ∈ A ∧ c ∉ B)

      (a ∈ {x. P x}) = P a

      (b ∈ (UN x:A. B x)) = (∃x∈A. b ∈ B x)

      (A ∈ Union C) = (∃X∈C. A ∈ X)

      (b ∈ (INT x:A. B x)) = (∀x∈A. b ∈ B x)

      (A ∈ Inter C) = (∀X∈C. A ∈ X)

      (P ∨ Q) = (Q ∨ P)

      (P ∨ Q ∨ R) = (Q ∨ P ∨ R)

      insert (f1 a1) (f1 ` B1) = f1 ` insert a1 B1

      f1 ` A1 ∪ f1 ` B1 = f1 ` (A1 ∪ B1)

      {} ⊆ A

      (insert x A ⊆ B) = (x ∈ B ∧ A ⊆ B)

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

      c ∈ analz G1 ==> c ∈ analz (A2 ∪ G1)

      insert (Key K) H = Key ` {K} ∪ H

      A ⊆ - range shrK ==> shrK x ∉ A

      Key K ∉ used evs ==> K ∉ range shrK

      insert (Key K) (Key ` KK ∪ C) = Key ` insert K KK ∪ C

      A1 ∪ (B1 ∪ C1) = A1 ∪ B1 ∪ C1

lemma analz_image_freshK_lemma:

      Key K ∈ analz (Key ` nE ∪ H) --> K ∈ nE ∨ Key K ∈ analz H
      ==> (Key K ∈ analz (Key ` nE ∪ H)) = (K ∈ nE ∨ Key K ∈ analz H)

lemma invKey_shrK_iff:

      (Key (invKey K) ∈ X) = (Key K ∈ X)

lemma knows_subset_knows_Cons:

      knows A evs ⊆ knows A (e # evs)