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