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