doc-src/TutorialI/Protocol/Public.thy
author berghofe
Mon Jul 23 14:31:34 2007 +0200 (2007-07-23)
changeset 23925 ee98c2528a8f
parent 16417 9bc16273c2d4
child 25341 ca3761e38a87
permissions -rw-r--r--
LaTeX code is now generated directly from theory files.
paulson@11250
     1
(*  Title:      HOL/Auth/Public
paulson@11250
     2
    ID:         $Id$
paulson@11250
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
paulson@11250
     4
    Copyright   1996  University of Cambridge
paulson@11250
     5
paulson@11250
     6
Theory of Public Keys (common to all public-key protocols)
paulson@11250
     7
paulson@11250
     8
Private and public keys; initial states of agents
berghofe@23925
     9
*)(*<*)
haftmann@16417
    10
theory Public imports Event
berghofe@23925
    11
begin
berghofe@23925
    12
(*>*)
paulson@11250
    13
berghofe@23925
    14
text {*
berghofe@23925
    15
The function
berghofe@23925
    16
@{text pubK} maps agents to their public keys.  The function
berghofe@23925
    17
@{text priK} maps agents to their private keys.  It is defined in terms of
berghofe@23925
    18
@{text invKey} and @{text pubK} by a translation; therefore @{text priK} is
berghofe@23925
    19
not a proper constant, so we declare it using \isacommand{syntax}
berghofe@23925
    20
(cf.\ \S\ref{sec:syntax-translations}).
berghofe@23925
    21
*}
paulson@11250
    22
berghofe@23925
    23
consts pubK :: "agent => key"
berghofe@23925
    24
syntax priK :: "agent => key"
berghofe@23925
    25
translations "priK x" \<rightleftharpoons> "invKey(pubK x)"
berghofe@23925
    26
(*<*)
paulson@11250
    27
primrec
paulson@11250
    28
        (*Agents know their private key and all public keys*)
paulson@11250
    29
  initState_Server:  "initState Server     =    
paulson@11250
    30
 		         insert (Key (priK Server)) (Key ` range pubK)"
paulson@11250
    31
  initState_Friend:  "initState (Friend i) =    
paulson@11250
    32
 		         insert (Key (priK (Friend i))) (Key ` range pubK)"
paulson@11250
    33
  initState_Spy:     "initState Spy        =    
paulson@11250
    34
 		         (Key`invKey`pubK`bad) Un (Key ` range pubK)"
berghofe@23925
    35
(*>*)
paulson@11250
    36
berghofe@23925
    37
text {*
berghofe@23925
    38
\noindent
berghofe@23925
    39
The set @{text bad} consists of those agents whose private keys are known to
berghofe@23925
    40
the spy.
berghofe@23925
    41
berghofe@23925
    42
Two axioms are asserted about the public-key cryptosystem. 
berghofe@23925
    43
No two agents have the same public key, and no private key equals
berghofe@23925
    44
any public key.
berghofe@23925
    45
*}
paulson@11250
    46
paulson@11250
    47
axioms
paulson@11250
    48
  inj_pubK:        "inj pubK"
paulson@11250
    49
  priK_neq_pubK:   "priK A ~= pubK B"
berghofe@23925
    50
(*<*)
berghofe@23925
    51
lemmas [iff] = inj_pubK [THEN inj_eq]
paulson@11250
    52
berghofe@23925
    53
lemma priK_inj_eq[iff]: "(priK A = priK B) = (A=B)"
berghofe@23925
    54
  apply safe
berghofe@23925
    55
  apply (drule_tac f=invKey in arg_cong)
berghofe@23925
    56
  apply simp
berghofe@23925
    57
  done
berghofe@23925
    58
berghofe@23925
    59
lemmas [iff] = priK_neq_pubK priK_neq_pubK [THEN not_sym]
berghofe@23925
    60
berghofe@23925
    61
lemma not_symKeys_pubK[iff]: "pubK A \<notin> symKeys"
berghofe@23925
    62
  by (simp add: symKeys_def)
berghofe@23925
    63
berghofe@23925
    64
lemma not_symKeys_priK[iff]: "priK A \<notin> symKeys"
berghofe@23925
    65
  by (simp add: symKeys_def)
berghofe@23925
    66
berghofe@23925
    67
lemma symKeys_neq_imp_neq: "(K \<in> symKeys) \<noteq> (K' \<in> symKeys) ==> K \<noteq> K'"
berghofe@23925
    68
  by blast
berghofe@23925
    69
berghofe@23925
    70
lemma analz_symKeys_Decrypt: "[| Crypt K X \<in> analz H;  K \<in> symKeys;  Key K \<in> analz H |]
berghofe@23925
    71
     ==> X \<in> analz H"
berghofe@23925
    72
  by (auto simp add: symKeys_def)
berghofe@23925
    73
berghofe@23925
    74
berghofe@23925
    75
(** "Image" equations that hold for injective functions **)
berghofe@23925
    76
berghofe@23925
    77
lemma invKey_image_eq[simp]: "(invKey x : invKey`A) = (x:A)"
berghofe@23925
    78
  by auto
berghofe@23925
    79
berghofe@23925
    80
(*holds because invKey is injective*)
berghofe@23925
    81
lemma pubK_image_eq[simp]: "(pubK x : pubK`A) = (x:A)"
berghofe@23925
    82
  by auto
berghofe@23925
    83
berghofe@23925
    84
lemma priK_pubK_image_eq[simp]: "(priK x ~: pubK`A)"
berghofe@23925
    85
  by auto
berghofe@23925
    86
berghofe@23925
    87
berghofe@23925
    88
(** Rewrites should not refer to  initState(Friend i) 
berghofe@23925
    89
    -- not in normal form! **)
berghofe@23925
    90
berghofe@23925
    91
lemma keysFor_parts_initState[simp]: "keysFor (parts (initState C)) = {}"
berghofe@23925
    92
  apply (unfold keysFor_def)
berghofe@23925
    93
  apply (induct C)
berghofe@23925
    94
  apply (auto intro: range_eqI)
berghofe@23925
    95
  done
berghofe@23925
    96
berghofe@23925
    97
berghofe@23925
    98
(*** Function "spies" ***)
berghofe@23925
    99
berghofe@23925
   100
(*Agents see their own private keys!*)
berghofe@23925
   101
lemma priK_in_initState[iff]: "Key (priK A) : initState A"
berghofe@23925
   102
  by (induct A) auto
berghofe@23925
   103
berghofe@23925
   104
(*All public keys are visible*)
berghofe@23925
   105
lemma spies_pubK[iff]: "Key (pubK A) : spies evs"
berghofe@23925
   106
  by (induct evs) (simp_all add: imageI knows_Cons split: event.split)
berghofe@23925
   107
berghofe@23925
   108
(*Spy sees private keys of bad agents!*)
berghofe@23925
   109
lemma Spy_spies_bad[intro!]: "A: bad ==> Key (priK A) : spies evs"
berghofe@23925
   110
  by (induct evs) (simp_all add: imageI knows_Cons split: event.split)
berghofe@23925
   111
berghofe@23925
   112
lemmas [iff] = spies_pubK [THEN analz.Inj]
berghofe@23925
   113
berghofe@23925
   114
berghofe@23925
   115
(*** Fresh nonces ***)
berghofe@23925
   116
berghofe@23925
   117
lemma Nonce_notin_initState[iff]: "Nonce N ~: parts (initState B)"
berghofe@23925
   118
  by (induct B) auto
berghofe@23925
   119
berghofe@23925
   120
lemma Nonce_notin_used_empty[simp]: "Nonce N ~: used []"
berghofe@23925
   121
  by (simp add: used_Nil)
berghofe@23925
   122
berghofe@23925
   123
berghofe@23925
   124
(*** Supply fresh nonces for possibility theorems. ***)
berghofe@23925
   125
berghofe@23925
   126
(*In any trace, there is an upper bound N on the greatest nonce in use.*)
berghofe@23925
   127
lemma Nonce_supply_lemma: "EX N. ALL n. N<=n --> Nonce n \<notin> used evs"
berghofe@23925
   128
apply (induct_tac "evs")
berghofe@23925
   129
apply (rule_tac x = 0 in exI)
berghofe@23925
   130
apply (simp_all (no_asm_simp) add: used_Cons split add: event.split)
berghofe@23925
   131
apply safe
berghofe@23925
   132
apply (rule msg_Nonce_supply [THEN exE], blast elim!: add_leE)+
berghofe@23925
   133
done
berghofe@23925
   134
berghofe@23925
   135
lemma Nonce_supply1: "EX N. Nonce N \<notin> used evs"
berghofe@23925
   136
by (rule Nonce_supply_lemma [THEN exE], blast)
berghofe@23925
   137
berghofe@23925
   138
lemma Nonce_supply: "Nonce (@ N. Nonce N \<notin> used evs) \<notin> used evs"
berghofe@23925
   139
apply (rule Nonce_supply_lemma [THEN exE])
berghofe@23925
   140
apply (rule someI, fast)
berghofe@23925
   141
done
berghofe@23925
   142
berghofe@23925
   143
berghofe@23925
   144
(*** Specialized rewriting for the analz_image_... theorems ***)
berghofe@23925
   145
berghofe@23925
   146
lemma insert_Key_singleton: "insert (Key K) H = Key ` {K} Un H"
berghofe@23925
   147
  by blast
berghofe@23925
   148
berghofe@23925
   149
lemma insert_Key_image: "insert (Key K) (Key`KK Un C) = Key ` (insert K KK) Un C"
berghofe@23925
   150
  by blast
berghofe@23925
   151
paulson@11250
   152
paulson@11250
   153
(*Specialized methods*)
paulson@11250
   154
berghofe@23925
   155
(*Tactic for possibility theorems*)
berghofe@23925
   156
ML {*
berghofe@23925
   157
fun possibility_tac st = st |>
berghofe@23925
   158
    REPEAT (*omit used_Says so that Nonces start from different traces!*)
berghofe@23925
   159
    (ALLGOALS (simp_tac (simpset() delsimps [used_Says]))
berghofe@23925
   160
     THEN
berghofe@23925
   161
     REPEAT_FIRST (eq_assume_tac ORELSE' 
berghofe@23925
   162
                   resolve_tac [refl, conjI, @{thm Nonce_supply}]));
berghofe@23925
   163
*}
berghofe@23925
   164
paulson@11250
   165
method_setup possibility = {*
paulson@11250
   166
    Method.no_args (Method.METHOD (fn facts => possibility_tac)) *}
paulson@11250
   167
    "for proving possibility theorems"
paulson@11250
   168
paulson@11250
   169
end
berghofe@23925
   170
(*>*)