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