src/HOL/Auth/Shared.thy
author paulson
Thu, 24 Jul 2003 16:36:29 +0200
changeset 14126 28824746d046
parent 13956 8fe7e12290e1
child 14181 942db403d4bb
permissions -rw-r--r--
Tidying and replacement of some axioms by specifications
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
1934
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
     1
(*  Title:      HOL/Auth/Shared
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
     2
    ID:         $Id$
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
     4
    Copyright   1996  University of Cambridge
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
     5
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
     6
Theory of Shared Keys (common to all symmetric-key protocols)
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
     7
3512
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents: 3472
diff changeset
     8
Shared, long-term keys; initial states of agents
1934
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
     9
*)
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
    10
13926
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13907
diff changeset
    11
theory Shared = Event:
1934
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
    12
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
    13
consts
14126
28824746d046 Tidying and replacement of some axioms by specifications
paulson
parents: 13956
diff changeset
    14
  shrK    :: "agent => key"  (*symmetric keys*);
28824746d046 Tidying and replacement of some axioms by specifications
paulson
parents: 13956
diff changeset
    15
28824746d046 Tidying and replacement of some axioms by specifications
paulson
parents: 13956
diff changeset
    16
specification (shrK)
28824746d046 Tidying and replacement of some axioms by specifications
paulson
parents: 13956
diff changeset
    17
  inj_shrK: "inj shrK"
28824746d046 Tidying and replacement of some axioms by specifications
paulson
parents: 13956
diff changeset
    18
  --{*No two agents have the same long-term key*}
28824746d046 Tidying and replacement of some axioms by specifications
paulson
parents: 13956
diff changeset
    19
   apply (rule exI [of _ "agent_case 0 (\<lambda>n. n + 2) 1"]) 
28824746d046 Tidying and replacement of some axioms by specifications
paulson
parents: 13956
diff changeset
    20
   apply (simp add: inj_on_def split: agent.split) 
28824746d046 Tidying and replacement of some axioms by specifications
paulson
parents: 13956
diff changeset
    21
   done
1967
0ff58b41c037 "bad" set simplifies statements of many theorems
paulson
parents: 1965
diff changeset
    22
14126
28824746d046 Tidying and replacement of some axioms by specifications
paulson
parents: 13956
diff changeset
    23
text{*All keys are symmetric*}
28824746d046 Tidying and replacement of some axioms by specifications
paulson
parents: 13956
diff changeset
    24
28824746d046 Tidying and replacement of some axioms by specifications
paulson
parents: 13956
diff changeset
    25
defs  all_symmetric_def: "all_symmetric == True"
1934
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
    26
14126
28824746d046 Tidying and replacement of some axioms by specifications
paulson
parents: 13956
diff changeset
    27
lemma isSym_keys: "K \<in> symKeys"	
28824746d046 Tidying and replacement of some axioms by specifications
paulson
parents: 13956
diff changeset
    28
by (simp add: symKeys_def all_symmetric_def invKey_cases) 
28824746d046 Tidying and replacement of some axioms by specifications
paulson
parents: 13956
diff changeset
    29
28824746d046 Tidying and replacement of some axioms by specifications
paulson
parents: 13956
diff changeset
    30
text{*Server knows all long-term keys; other agents know only their own*}
5183
89f162de39cf Adapted to new datatype package.
berghofe
parents: 3683
diff changeset
    31
primrec
11104
f2024fed9f0c partial conversion to Isar script style
paulson
parents: 10833
diff changeset
    32
  initState_Server:  "initState Server     = Key ` range shrK"
f2024fed9f0c partial conversion to Isar script style
paulson
parents: 10833
diff changeset
    33
  initState_Friend:  "initState (Friend i) = {Key (shrK (Friend i))}"
f2024fed9f0c partial conversion to Isar script style
paulson
parents: 10833
diff changeset
    34
  initState_Spy:     "initState Spy        = Key`shrK`bad"
2032
1bbf1bdcaf56 Introduction of "lost" argument
paulson
parents: 2012
diff changeset
    35
1934
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
    36
13926
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13907
diff changeset
    37
subsection{*Basic properties of shrK*}
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13907
diff changeset
    38
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13907
diff changeset
    39
(*Injectiveness: Agents' long-term keys are distinct.*)
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13907
diff changeset
    40
declare inj_shrK [THEN inj_eq, iff]
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13907
diff changeset
    41
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13907
diff changeset
    42
lemma invKey_K [simp]: "invKey K = K"
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13907
diff changeset
    43
apply (insert isSym_keys)
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13907
diff changeset
    44
apply (simp add: symKeys_def) 
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13907
diff changeset
    45
done
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13907
diff changeset
    46
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13907
diff changeset
    47
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13907
diff changeset
    48
lemma analz_Decrypt' [dest]:
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13907
diff changeset
    49
     "[| Crypt K X \<in> analz H;  Key K  \<in> analz H |] ==> X \<in> analz H"
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13907
diff changeset
    50
by auto
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13907
diff changeset
    51
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13907
diff changeset
    52
text{*Now cancel the @{text dest} attribute given to
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13907
diff changeset
    53
 @{text analz.Decrypt} in its declaration.*}
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13907
diff changeset
    54
ML
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13907
diff changeset
    55
{*
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13907
diff changeset
    56
Delrules [analz.Decrypt];
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13907
diff changeset
    57
*}
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13907
diff changeset
    58
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13907
diff changeset
    59
text{*Rewrites should not refer to  @{term "initState(Friend i)"} because
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13907
diff changeset
    60
  that expression is not in normal form.*}
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13907
diff changeset
    61
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13907
diff changeset
    62
lemma keysFor_parts_initState [simp]: "keysFor (parts (initState C)) = {}"
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13907
diff changeset
    63
apply (unfold keysFor_def)
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13907
diff changeset
    64
apply (induct_tac "C", auto)
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13907
diff changeset
    65
done
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13907
diff changeset
    66
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13907
diff changeset
    67
(*Specialized to shared-key model: no @{term invKey}*)
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13907
diff changeset
    68
lemma keysFor_parts_insert:
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13907
diff changeset
    69
     "[| K \<in> keysFor (parts (insert X G));  X \<in> synth (analz H) |] \
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13907
diff changeset
    70
\     ==> K \<in> keysFor (parts (G \<union> H)) | Key K \<in> parts H";
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13907
diff changeset
    71
by (force dest: Event.keysFor_parts_insert)  
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13907
diff changeset
    72
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13907
diff changeset
    73
lemma Crypt_imp_keysFor: "Crypt K X \<in> H ==> K \<in> keysFor H"
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13907
diff changeset
    74
by (drule Crypt_imp_invKey_keysFor, simp)
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13907
diff changeset
    75
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13907
diff changeset
    76
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13907
diff changeset
    77
subsection{*Function "knows"*}
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13907
diff changeset
    78
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13907
diff changeset
    79
(*Spy sees shared keys of agents!*)
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13907
diff changeset
    80
lemma Spy_knows_Spy_bad [intro!]: "A: bad ==> Key (shrK A) \<in> knows Spy evs"
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13907
diff changeset
    81
apply (induct_tac "evs")
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13907
diff changeset
    82
apply (simp_all (no_asm_simp) add: imageI knows_Cons split add: event.split)
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13907
diff changeset
    83
done
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13907
diff changeset
    84
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13907
diff changeset
    85
(*For case analysis on whether or not an agent is compromised*)
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13907
diff changeset
    86
lemma Crypt_Spy_analz_bad: "[| Crypt (shrK A) X \<in> analz (knows Spy evs);  A: bad |]  
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13907
diff changeset
    87
      ==> X \<in> analz (knows Spy evs)"
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13907
diff changeset
    88
apply (force dest!: analz.Decrypt)
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13907
diff changeset
    89
done
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13907
diff changeset
    90
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13907
diff changeset
    91
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13907
diff changeset
    92
(** Fresh keys never clash with long-term shared keys **)
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13907
diff changeset
    93
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13907
diff changeset
    94
(*Agents see their own shared keys!*)
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13907
diff changeset
    95
lemma shrK_in_initState [iff]: "Key (shrK A) \<in> initState A"
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13907
diff changeset
    96
by (induct_tac "A", auto)
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13907
diff changeset
    97
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13907
diff changeset
    98
lemma shrK_in_used [iff]: "Key (shrK A) \<in> used evs"
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13907
diff changeset
    99
by (rule initState_into_used, blast)
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13907
diff changeset
   100
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13907
diff changeset
   101
(*Used in parts_induct_tac and analz_Fake_tac to distinguish session keys
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13907
diff changeset
   102
  from long-term shared keys*)
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13907
diff changeset
   103
lemma Key_not_used [simp]: "Key K \<notin> used evs ==> K \<notin> range shrK"
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13907
diff changeset
   104
by blast
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13907
diff changeset
   105
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13907
diff changeset
   106
lemma shrK_neq [simp]: "Key K \<notin> used evs ==> shrK B \<noteq> K"
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13907
diff changeset
   107
by blast
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13907
diff changeset
   108
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13907
diff changeset
   109
declare shrK_neq [THEN not_sym, simp]
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13907
diff changeset
   110
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13907
diff changeset
   111
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13907
diff changeset
   112
subsection{*Fresh nonces*}
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13907
diff changeset
   113
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13907
diff changeset
   114
lemma Nonce_notin_initState [iff]: "Nonce N \<notin> parts (initState B)"
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13907
diff changeset
   115
by (induct_tac "B", auto)
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13907
diff changeset
   116
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13907
diff changeset
   117
lemma Nonce_notin_used_empty [simp]: "Nonce N \<notin> used []"
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13907
diff changeset
   118
apply (simp (no_asm) add: used_Nil)
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13907
diff changeset
   119
done
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13907
diff changeset
   120
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13907
diff changeset
   121
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13907
diff changeset
   122
subsection{*Supply fresh nonces for possibility theorems.*}
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13907
diff changeset
   123
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13907
diff changeset
   124
(*In any trace, there is an upper bound N on the greatest nonce in use.*)
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13907
diff changeset
   125
lemma Nonce_supply_lemma: "\<exists>N. ALL n. N<=n --> Nonce n \<notin> used evs"
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13907
diff changeset
   126
apply (induct_tac "evs")
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13907
diff changeset
   127
apply (rule_tac x = 0 in exI)
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13907
diff changeset
   128
apply (simp_all (no_asm_simp) add: used_Cons split add: event.split)
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13907
diff changeset
   129
apply safe
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13907
diff changeset
   130
apply (rule msg_Nonce_supply [THEN exE], blast elim!: add_leE)+
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13907
diff changeset
   131
done
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13907
diff changeset
   132
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13907
diff changeset
   133
lemma Nonce_supply1: "\<exists>N. Nonce N \<notin> used evs"
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13907
diff changeset
   134
by (rule Nonce_supply_lemma [THEN exE], blast)
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13907
diff changeset
   135
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13907
diff changeset
   136
lemma Nonce_supply2: "\<exists>N N'. Nonce N \<notin> used evs & Nonce N' \<notin> used evs' & N \<noteq> N'"
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13907
diff changeset
   137
apply (cut_tac evs = evs in Nonce_supply_lemma)
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13907
diff changeset
   138
apply (cut_tac evs = "evs'" in Nonce_supply_lemma, clarify)
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13907
diff changeset
   139
apply (rule_tac x = N in exI)
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13907
diff changeset
   140
apply (rule_tac x = "Suc (N+Na) " in exI)
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13907
diff changeset
   141
apply (simp (no_asm_simp) add: less_not_refl3 le_add1 le_add2 less_Suc_eq_le)
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13907
diff changeset
   142
done
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13907
diff changeset
   143
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13907
diff changeset
   144
lemma Nonce_supply3: "\<exists>N N' N''. Nonce N \<notin> used evs & Nonce N' \<notin> used evs' &  
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13907
diff changeset
   145
                    Nonce N'' \<notin> used evs'' & N \<noteq> N' & N' \<noteq> N'' & N \<noteq> N''"
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13907
diff changeset
   146
apply (cut_tac evs = evs in Nonce_supply_lemma)
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13907
diff changeset
   147
apply (cut_tac evs = "evs'" in Nonce_supply_lemma)
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13907
diff changeset
   148
apply (cut_tac evs = "evs''" in Nonce_supply_lemma, clarify)
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13907
diff changeset
   149
apply (rule_tac x = N in exI)
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13907
diff changeset
   150
apply (rule_tac x = "Suc (N+Na) " in exI)
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13907
diff changeset
   151
apply (rule_tac x = "Suc (Suc (N+Na+Nb))" in exI)
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13907
diff changeset
   152
apply (simp (no_asm_simp) add: less_not_refl3 le_add1 le_add2 less_Suc_eq_le)
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13907
diff changeset
   153
done
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13907
diff changeset
   154
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13907
diff changeset
   155
lemma Nonce_supply: "Nonce (@ N. Nonce N \<notin> used evs) \<notin> used evs"
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13907
diff changeset
   156
apply (rule Nonce_supply_lemma [THEN exE])
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13907
diff changeset
   157
apply (rule someI, blast)
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13907
diff changeset
   158
done
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13907
diff changeset
   159
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13907
diff changeset
   160
subsection{*Supply fresh keys for possibility theorems.*}
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13907
diff changeset
   161
11104
f2024fed9f0c partial conversion to Isar script style
paulson
parents: 10833
diff changeset
   162
axioms
13926
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13907
diff changeset
   163
  Key_supply_ax:  "finite KK ==> \<exists>K. K \<notin> KK & Key K \<notin> used evs"
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13907
diff changeset
   164
  --{*Unlike the corresponding property of nonces, this cannot be proved.
2516
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
   165
    We have infinitely many agents and there is nothing to stop their
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
   166
    long-term keys from exhausting all the natural numbers.  The axiom
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
   167
    assumes that their keys are dispersed so as to leave room for infinitely
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
   168
    many fresh session keys.  We could, alternatively, restrict agents to
13926
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13907
diff changeset
   169
    an unspecified finite number.  We could however replace @{term"used evs"} 
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13907
diff changeset
   170
    by @{term "used []"}.*}
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13907
diff changeset
   171
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13907
diff changeset
   172
lemma Key_supply1: "\<exists>K. Key K \<notin> used evs"
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13907
diff changeset
   173
by (rule Finites.emptyI [THEN Key_supply_ax, THEN exE], blast)
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13907
diff changeset
   174
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13907
diff changeset
   175
lemma Key_supply2: "\<exists>K K'. Key K \<notin> used evs & Key K' \<notin> used evs' & K \<noteq> K'"
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13907
diff changeset
   176
apply (cut_tac evs = evs in Finites.emptyI [THEN Key_supply_ax])
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13907
diff changeset
   177
apply (erule exE)
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13907
diff changeset
   178
apply (cut_tac evs="evs'" in Finites.emptyI [THEN Finites.insertI, THEN Key_supply_ax], auto) 
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13907
diff changeset
   179
done
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13907
diff changeset
   180
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13907
diff changeset
   181
lemma Key_supply3: "\<exists>K K' K''. Key K \<notin> used evs & Key K' \<notin> used evs' &  
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13907
diff changeset
   182
                       Key K'' \<notin> used evs'' & K \<noteq> K' & K' \<noteq> K'' & K \<noteq> K''"
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13907
diff changeset
   183
apply (cut_tac evs = evs in Finites.emptyI [THEN Key_supply_ax])
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13907
diff changeset
   184
apply (erule exE)
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13907
diff changeset
   185
(*Blast_tac requires instantiation of the keys for some reason*)
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13907
diff changeset
   186
apply (cut_tac evs="evs'" and a1 = K in Finites.emptyI [THEN Finites.insertI, THEN Key_supply_ax])
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13907
diff changeset
   187
apply (erule exE)
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13907
diff changeset
   188
apply (cut_tac evs = "evs''" and a1 = Ka and a2 = K 
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13907
diff changeset
   189
       in Finites.emptyI [THEN Finites.insertI, THEN Finites.insertI, THEN Key_supply_ax], blast)
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13907
diff changeset
   190
done
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13907
diff changeset
   191
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13907
diff changeset
   192
lemma Key_supply: "Key (@ K. Key K \<notin> used evs) \<notin> used evs"
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13907
diff changeset
   193
apply (rule Finites.emptyI [THEN Key_supply_ax, THEN exE])
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13907
diff changeset
   194
apply (rule someI, blast)
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13907
diff changeset
   195
done
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13907
diff changeset
   196
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13907
diff changeset
   197
subsection{*Tactics for possibility theorems*}
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13907
diff changeset
   198
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13907
diff changeset
   199
ML
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13907
diff changeset
   200
{*
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13907
diff changeset
   201
val inj_shrK      = thm "inj_shrK";
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13907
diff changeset
   202
val isSym_keys    = thm "isSym_keys";
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13907
diff changeset
   203
val Key_supply_ax = thm "Key_supply_ax";
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13907
diff changeset
   204
val Key_supply = thm "Key_supply";
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13907
diff changeset
   205
val Nonce_supply = thm "Nonce_supply";
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13907
diff changeset
   206
val invKey_K = thm "invKey_K";
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13907
diff changeset
   207
val analz_Decrypt' = thm "analz_Decrypt'";
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13907
diff changeset
   208
val keysFor_parts_initState = thm "keysFor_parts_initState";
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13907
diff changeset
   209
val keysFor_parts_insert = thm "keysFor_parts_insert";
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13907
diff changeset
   210
val Crypt_imp_keysFor = thm "Crypt_imp_keysFor";
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13907
diff changeset
   211
val Spy_knows_Spy_bad = thm "Spy_knows_Spy_bad";
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13907
diff changeset
   212
val Crypt_Spy_analz_bad = thm "Crypt_Spy_analz_bad";
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13907
diff changeset
   213
val shrK_in_initState = thm "shrK_in_initState";
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13907
diff changeset
   214
val shrK_in_used = thm "shrK_in_used";
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13907
diff changeset
   215
val Key_not_used = thm "Key_not_used";
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13907
diff changeset
   216
val shrK_neq = thm "shrK_neq";
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13907
diff changeset
   217
val Nonce_notin_initState = thm "Nonce_notin_initState";
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13907
diff changeset
   218
val Nonce_notin_used_empty = thm "Nonce_notin_used_empty";
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13907
diff changeset
   219
val Nonce_supply_lemma = thm "Nonce_supply_lemma";
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13907
diff changeset
   220
val Nonce_supply1 = thm "Nonce_supply1";
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13907
diff changeset
   221
val Nonce_supply2 = thm "Nonce_supply2";
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13907
diff changeset
   222
val Nonce_supply3 = thm "Nonce_supply3";
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13907
diff changeset
   223
val Nonce_supply = thm "Nonce_supply";
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13907
diff changeset
   224
val Key_supply1 = thm "Key_supply1";
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13907
diff changeset
   225
val Key_supply2 = thm "Key_supply2";
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13907
diff changeset
   226
val Key_supply3 = thm "Key_supply3";
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13907
diff changeset
   227
val Key_supply = thm "Key_supply";
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13907
diff changeset
   228
*}
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13907
diff changeset
   229
11104
f2024fed9f0c partial conversion to Isar script style
paulson
parents: 10833
diff changeset
   230
13926
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13907
diff changeset
   231
ML
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13907
diff changeset
   232
{*
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13907
diff changeset
   233
(*Omitting used_Says makes the tactic much faster: it leaves expressions
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13907
diff changeset
   234
    such as  Nonce ?N \<notin> used evs that match Nonce_supply*)
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13907
diff changeset
   235
fun gen_possibility_tac ss state = state |>
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13907
diff changeset
   236
   (REPEAT 
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13907
diff changeset
   237
    (ALLGOALS (simp_tac (ss delsimps [used_Says, used_Notes, used_Gets] 
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13907
diff changeset
   238
                         setSolver safe_solver))
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13907
diff changeset
   239
     THEN
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13907
diff changeset
   240
     REPEAT_FIRST (eq_assume_tac ORELSE' 
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13907
diff changeset
   241
                   resolve_tac [refl, conjI, Nonce_supply, Key_supply])))
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13907
diff changeset
   242
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13907
diff changeset
   243
(*Tactic for possibility theorems (ML script version)*)
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13907
diff changeset
   244
fun possibility_tac state = gen_possibility_tac (simpset()) state
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13907
diff changeset
   245
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13907
diff changeset
   246
(*For harder protocols (such as Recur) where we have to set up some
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13907
diff changeset
   247
  nonces and keys initially*)
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13907
diff changeset
   248
fun basic_possibility_tac st = st |>
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13907
diff changeset
   249
    REPEAT 
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13907
diff changeset
   250
    (ALLGOALS (asm_simp_tac (simpset() setSolver safe_solver))
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13907
diff changeset
   251
     THEN
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13907
diff changeset
   252
     REPEAT_FIRST (resolve_tac [refl, conjI]))
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13907
diff changeset
   253
*}
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13907
diff changeset
   254
13956
8fe7e12290e1 improved presentation of HOL/Auth theories
paulson
parents: 13926
diff changeset
   255
subsection{*Specialized Rewriting for Theorems About @{term analz} and Image*}
13926
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13907
diff changeset
   256
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13907
diff changeset
   257
lemma subset_Compl_range: "A <= - (range shrK) ==> shrK x \<notin> A"
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13907
diff changeset
   258
by blast
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13907
diff changeset
   259
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13907
diff changeset
   260
lemma insert_Key_singleton: "insert (Key K) H = Key ` {K} \<union> H"
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13907
diff changeset
   261
by blast
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13907
diff changeset
   262
13956
8fe7e12290e1 improved presentation of HOL/Auth theories
paulson
parents: 13926
diff changeset
   263
lemma insert_Key_image: "insert (Key K) (Key`KK \<union> C) = Key`(insert K KK) \<union> C"
13926
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13907
diff changeset
   264
by blast
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13907
diff changeset
   265
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13907
diff changeset
   266
(** Reverse the normal simplification of "image" to build up (not break down)
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13907
diff changeset
   267
    the set of keys.  Use analz_insert_eq with (Un_upper2 RS analz_mono) to
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13907
diff changeset
   268
    erase occurrences of forwarded message components (X). **)
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13907
diff changeset
   269
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13907
diff changeset
   270
lemmas analz_image_freshK_simps =
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13907
diff changeset
   271
       simp_thms mem_simps --{*these two allow its use with @{text "only:"}*}
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13907
diff changeset
   272
       disj_comms 
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13907
diff changeset
   273
       image_insert [THEN sym] image_Un [THEN sym] empty_subsetI insert_subset
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13907
diff changeset
   274
       analz_insert_eq Un_upper2 [THEN analz_mono, THEN [2] rev_subsetD]
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13907
diff changeset
   275
       insert_Key_singleton subset_Compl_range
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13907
diff changeset
   276
       Key_not_used insert_Key_image Un_assoc [THEN sym]
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13907
diff changeset
   277
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13907
diff changeset
   278
(*Lemma for the trivial direction of the if-and-only-if*)
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13907
diff changeset
   279
lemma analz_image_freshK_lemma:
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13907
diff changeset
   280
     "(Key K \<in> analz (Key`nE \<union> H)) --> (K \<in> nE | Key K \<in> analz H)  ==>  
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13907
diff changeset
   281
         (Key K \<in> analz (Key`nE \<union> H)) = (K \<in> nE | Key K \<in> analz H)"
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13907
diff changeset
   282
by (blast intro: analz_mono [THEN [2] rev_subsetD])
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13907
diff changeset
   283
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13907
diff changeset
   284
ML
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13907
diff changeset
   285
{*
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13907
diff changeset
   286
val analz_image_freshK_lemma = thm "analz_image_freshK_lemma";
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13907
diff changeset
   287
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13907
diff changeset
   288
val analz_image_freshK_ss = 
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13907
diff changeset
   289
     simpset() delsimps [image_insert, image_Un]
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13907
diff changeset
   290
	       delsimps [imp_disjL]    (*reduces blow-up*)
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13907
diff changeset
   291
	       addsimps thms "analz_image_freshK_simps"
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13907
diff changeset
   292
*}
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13907
diff changeset
   293
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13907
diff changeset
   294
11104
f2024fed9f0c partial conversion to Isar script style
paulson
parents: 10833
diff changeset
   295
f2024fed9f0c partial conversion to Isar script style
paulson
parents: 10833
diff changeset
   296
(*Lets blast_tac perform this step without needing the simplifier*)
f2024fed9f0c partial conversion to Isar script style
paulson
parents: 10833
diff changeset
   297
lemma invKey_shrK_iff [iff]:
11270
a315a3862bb4 better treatment of methods: uses Method.ctxt_args to refer to current
paulson
parents: 11230
diff changeset
   298
     "(Key (invKey K) \<in> X) = (Key K \<in> X)"
13507
febb8e5d2a9d tidying of Isar scripts
paulson
parents: 12415
diff changeset
   299
by auto
11104
f2024fed9f0c partial conversion to Isar script style
paulson
parents: 10833
diff changeset
   300
f2024fed9f0c partial conversion to Isar script style
paulson
parents: 10833
diff changeset
   301
(*Specialized methods*)
f2024fed9f0c partial conversion to Isar script style
paulson
parents: 10833
diff changeset
   302
f2024fed9f0c partial conversion to Isar script style
paulson
parents: 10833
diff changeset
   303
method_setup analz_freshK = {*
f2024fed9f0c partial conversion to Isar script style
paulson
parents: 10833
diff changeset
   304
    Method.no_args
f2024fed9f0c partial conversion to Isar script style
paulson
parents: 10833
diff changeset
   305
     (Method.METHOD
13907
2bc462b99e70 tidying
paulson
parents: 13507
diff changeset
   306
      (fn facts => EVERY [REPEAT_FIRST (resolve_tac [allI, ballI, impI]),
11104
f2024fed9f0c partial conversion to Isar script style
paulson
parents: 10833
diff changeset
   307
                          REPEAT_FIRST (rtac analz_image_freshK_lemma),
f2024fed9f0c partial conversion to Isar script style
paulson
parents: 10833
diff changeset
   308
                          ALLGOALS (asm_simp_tac analz_image_freshK_ss)])) *}
f2024fed9f0c partial conversion to Isar script style
paulson
parents: 10833
diff changeset
   309
    "for proving the Session Key Compromise theorem"
f2024fed9f0c partial conversion to Isar script style
paulson
parents: 10833
diff changeset
   310
f2024fed9f0c partial conversion to Isar script style
paulson
parents: 10833
diff changeset
   311
method_setup possibility = {*
11270
a315a3862bb4 better treatment of methods: uses Method.ctxt_args to refer to current
paulson
parents: 11230
diff changeset
   312
    Method.ctxt_args (fn ctxt =>
a315a3862bb4 better treatment of methods: uses Method.ctxt_args to refer to current
paulson
parents: 11230
diff changeset
   313
        Method.METHOD (fn facts =>
a315a3862bb4 better treatment of methods: uses Method.ctxt_args to refer to current
paulson
parents: 11230
diff changeset
   314
            gen_possibility_tac (Simplifier.get_local_simpset ctxt))) *}
11104
f2024fed9f0c partial conversion to Isar script style
paulson
parents: 10833
diff changeset
   315
    "for proving possibility theorems"
2516
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
   316
12415
74977582a585 Slightly generalized the agents' knowledge theorems
paulson
parents: 11270
diff changeset
   317
lemma knows_subset_knows_Cons: "knows A evs <= knows A (e # evs)"
74977582a585 Slightly generalized the agents' knowledge theorems
paulson
parents: 11270
diff changeset
   318
by (induct e, auto simp: knows_Cons)
74977582a585 Slightly generalized the agents' knowledge theorems
paulson
parents: 11270
diff changeset
   319
1934
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
   320
end