src/HOL/Auth/CertifiedEmail.thy
author webertj
Mon Mar 07 19:30:53 2005 +0100 (2005-03-07)
changeset 15584 3478bb4f93ff
parent 15068 58d216b32199
child 16417 9bc16273c2d4
permissions -rw-r--r--
refute_params: default value itself=1 added (for type classes)
paulson@13922
     1
(*  Title:      HOL/Auth/CertifiedEmail
paulson@13922
     2
    ID:         $Id$
paulson@13922
     3
    Author:     Giampaolo Bella, Christiano Longo and Lawrence C Paulson
paulson@13956
     4
*)
paulson@13922
     5
paulson@13956
     6
header{*The Certified Electronic Mail Protocol by Abadi et al.*}
paulson@13922
     7
paulson@13922
     8
theory CertifiedEmail = Public:
paulson@13922
     9
paulson@13922
    10
syntax
paulson@13922
    11
  TTP        :: agent
paulson@13922
    12
  RPwd       :: "agent => key"
paulson@13922
    13
paulson@13922
    14
translations
paulson@13926
    15
  "TTP"   == "Server "
paulson@13926
    16
  "RPwd"  == "shrK "
paulson@13922
    17
paulson@13922
    18
 
paulson@13922
    19
(*FIXME: the four options should be represented by pairs of 0 or 1.
paulson@13922
    20
  Right now only BothAuth is modelled.*)
paulson@13922
    21
consts
paulson@13922
    22
  NoAuth   :: nat
paulson@13922
    23
  TTPAuth  :: nat
paulson@13922
    24
  SAuth    :: nat
paulson@13922
    25
  BothAuth :: nat
paulson@13922
    26
paulson@13922
    27
text{*We formalize a fixed way of computing responses.  Could be better.*}
paulson@13922
    28
constdefs
paulson@13922
    29
  "response"    :: "agent => agent => nat => msg"
paulson@13922
    30
   "response S R q == Hash {|Agent S, Key (shrK R), Nonce q|}"
paulson@13922
    31
paulson@13922
    32
paulson@13922
    33
consts  certified_mail   :: "event list set"
paulson@13922
    34
inductive "certified_mail"
paulson@13922
    35
  intros 
paulson@13922
    36
paulson@13922
    37
Nil: --{*The empty trace*}
paulson@13922
    38
     "[] \<in> certified_mail"
paulson@13922
    39
paulson@13922
    40
Fake: --{*The Spy may say anything he can say.  The sender field is correct,
paulson@13922
    41
          but agents don't use that information.*}
paulson@14145
    42
      "[| evsf \<in> certified_mail; X \<in> synth(analz(spies evsf))|] 
paulson@13956
    43
       ==> Says Spy B X # evsf \<in> certified_mail"
paulson@13922
    44
paulson@13922
    45
FakeSSL: --{*The Spy may open SSL sessions with TTP, who is the only agent
paulson@13922
    46
    equipped with the necessary credentials to serve as an SSL server.*}
paulson@14145
    47
	 "[| evsfssl \<in> certified_mail; X \<in> synth(analz(spies evsfssl))|]
paulson@13922
    48
          ==> Notes TTP {|Agent Spy, Agent TTP, X|} # evsfssl \<in> certified_mail"
paulson@13922
    49
paulson@13922
    50
CM1: --{*The sender approaches the recipient.  The message is a number.*}
paulson@15068
    51
 "[|evs1 \<in> certified_mail;
paulson@15068
    52
    Key K \<notin> used evs1;
paulson@15068
    53
    K \<in> symKeys;
paulson@15068
    54
    Nonce q \<notin> used evs1;
paulson@15068
    55
    hs = Hash{|Number cleartext, Nonce q, response S R q, Crypt K (Number m)|};
paulson@15068
    56
    S2TTP = Crypt(pubEK TTP) {|Agent S, Number BothAuth, Key K, Agent R, hs|}|]
paulson@15068
    57
  ==> Says S R {|Agent S, Agent TTP, Crypt K (Number m), Number BothAuth, 
paulson@15068
    58
		 Number cleartext, Nonce q, S2TTP|} # evs1 
paulson@15068
    59
	\<in> certified_mail"
paulson@13922
    60
paulson@14735
    61
CM2: --{*The recipient records @{term S2TTP} while transmitting it and her
paulson@13922
    62
     password to @{term TTP} over an SSL channel.*}
paulson@15068
    63
 "[|evs2 \<in> certified_mail;
paulson@15068
    64
    Gets R {|Agent S, Agent TTP, em, Number BothAuth, Number cleartext, 
paulson@15068
    65
	     Nonce q, S2TTP|} \<in> set evs2;
paulson@15068
    66
    TTP \<noteq> R;  
paulson@15068
    67
    hr = Hash {|Number cleartext, Nonce q, response S R q, em|} |]
paulson@15068
    68
  ==> 
paulson@15068
    69
   Notes TTP {|Agent R, Agent TTP, S2TTP, Key(RPwd R), hr|} # evs2
paulson@15068
    70
      \<in> certified_mail"
paulson@13922
    71
paulson@13922
    72
CM3: --{*@{term TTP} simultaneously reveals the key to the recipient and gives
paulson@13922
    73
         a receipt to the sender.  The SSL channel does not authenticate 
paulson@14735
    74
         the client (@{term R}), but @{term TTP} accepts the message only 
paulson@14735
    75
         if the given password is that of the claimed sender, @{term R}.
paulson@13922
    76
         He replies over the established SSL channel.*}
paulson@13922
    77
 "[|evs3 \<in> certified_mail;
paulson@14735
    78
    Notes TTP {|Agent R, Agent TTP, S2TTP, Key(RPwd R), hr|} \<in> set evs3;
paulson@14735
    79
    S2TTP = Crypt (pubEK TTP) 
paulson@14735
    80
                     {|Agent S, Number BothAuth, Key k, Agent R, hs|};
paulson@14735
    81
    TTP \<noteq> R;  hs = hr;  k \<in> symKeys|]
paulson@15068
    82
  ==> 
paulson@15068
    83
   Notes R {|Agent TTP, Agent R, Key k, hr|} # 
paulson@15068
    84
   Gets S (Crypt (priSK TTP) S2TTP) # 
paulson@15068
    85
   Says TTP S (Crypt (priSK TTP) S2TTP) # evs3 \<in> certified_mail"
paulson@13922
    86
paulson@13922
    87
Reception:
paulson@13922
    88
 "[|evsr \<in> certified_mail; Says A B X \<in> set evsr|]
paulson@13922
    89
  ==> Gets B X#evsr \<in> certified_mail"
paulson@13922
    90
paulson@13922
    91
paulson@14145
    92
declare Says_imp_knows_Spy [THEN analz.Inj, dest]
paulson@14145
    93
declare analz_into_parts [dest]
paulson@14145
    94
paulson@13922
    95
(*A "possibility property": there are traces that reach the end*)
paulson@14200
    96
lemma "[| Key K \<notin> used []; K \<in> symKeys |] ==> 
paulson@14200
    97
       \<exists>S2TTP. \<exists>evs \<in> certified_mail.
paulson@13956
    98
           Says TTP S (Crypt (priSK TTP) S2TTP) \<in> set evs"
paulson@13922
    99
apply (intro exI bexI)
paulson@13922
   100
apply (rule_tac [2] certified_mail.Nil
paulson@13922
   101
                    [THEN certified_mail.CM1, THEN certified_mail.Reception,
paulson@13922
   102
                     THEN certified_mail.CM2, 
paulson@14200
   103
                     THEN certified_mail.CM3]) 
paulson@14200
   104
apply (possibility, auto) 
paulson@13922
   105
done
paulson@13922
   106
paulson@13922
   107
paulson@13922
   108
lemma Gets_imp_Says:
paulson@13922
   109
 "[| Gets B X \<in> set evs; evs \<in> certified_mail |] ==> \<exists>A. Says A B X \<in> set evs"
paulson@13922
   110
apply (erule rev_mp)
paulson@13922
   111
apply (erule certified_mail.induct, auto)
paulson@13922
   112
done
paulson@13922
   113
paulson@13922
   114
paulson@13922
   115
lemma Gets_imp_parts_knows_Spy:
paulson@13922
   116
     "[|Gets A X \<in> set evs; evs \<in> certified_mail|] ==> X \<in> parts(spies evs)"
paulson@13922
   117
apply (drule Gets_imp_Says, simp)
paulson@13922
   118
apply (blast dest: Says_imp_knows_Spy parts.Inj) 
paulson@13922
   119
done
paulson@13922
   120
paulson@13922
   121
lemma CM2_S2TTP_analz_knows_Spy:
paulson@13922
   122
 "[|Gets R {|Agent A, Agent B, em, Number AO, Number cleartext, 
paulson@13922
   123
              Nonce q, S2TTP|} \<in> set evs;
paulson@13922
   124
    evs \<in> certified_mail|] 
paulson@14145
   125
  ==> S2TTP \<in> analz(spies evs)"
paulson@13922
   126
apply (drule Gets_imp_Says, simp) 
paulson@13922
   127
apply (blast dest: Says_imp_knows_Spy analz.Inj) 
paulson@13922
   128
done
paulson@13922
   129
paulson@13922
   130
lemmas CM2_S2TTP_parts_knows_Spy = 
paulson@13922
   131
    CM2_S2TTP_analz_knows_Spy [THEN analz_subset_parts [THEN subsetD]]
paulson@13922
   132
paulson@13922
   133
lemma hr_form_lemma [rule_format]:
paulson@13922
   134
 "evs \<in> certified_mail
paulson@14145
   135
  ==> hr \<notin> synth (analz (spies evs)) --> 
paulson@13922
   136
      (\<forall>S2TTP. Notes TTP {|Agent R, Agent TTP, S2TTP, pwd, hr|}
paulson@13922
   137
          \<in> set evs --> 
paulson@13922
   138
      (\<exists>clt q S em. hr = Hash {|Number clt, Nonce q, response S R q, em|}))"
paulson@13922
   139
apply (erule certified_mail.induct)
paulson@13922
   140
apply (synth_analz_mono_contra, simp_all, blast+)
paulson@13922
   141
done 
paulson@13922
   142
paulson@13922
   143
text{*Cannot strengthen the first disjunct to @{term "R\<noteq>Spy"} because
paulson@13922
   144
the fakessl rule allows Spy to spoof the sender's name.  Maybe can
paulson@13922
   145
strengthen the second disjunct with @{term "R\<noteq>Spy"}.*}
paulson@13922
   146
lemma hr_form:
paulson@13922
   147
 "[|Notes TTP {|Agent R, Agent TTP, S2TTP, pwd, hr|} \<in> set evs;
paulson@13922
   148
    evs \<in> certified_mail|]
paulson@14145
   149
  ==> hr \<in> synth (analz (spies evs)) | 
paulson@13922
   150
      (\<exists>clt q S em. hr = Hash {|Number clt, Nonce q, response S R q, em|})"
paulson@13922
   151
by (blast intro: hr_form_lemma) 
paulson@13922
   152
paulson@14145
   153
lemma Spy_dont_know_private_keys [dest!]:
paulson@14145
   154
    "[|Key (privateKey b A) \<in> parts (spies evs); evs \<in> certified_mail|]
paulson@14145
   155
     ==> A \<in> bad"
paulson@14145
   156
apply (erule rev_mp) 
paulson@13922
   157
apply (erule certified_mail.induct, simp_all)
paulson@13922
   158
txt{*Fake*}
paulson@14207
   159
apply (blast dest: Fake_parts_insert_in_Un) 
paulson@13922
   160
txt{*Message 1*}
paulson@13922
   161
apply blast  
paulson@13922
   162
txt{*Message 3*}
paulson@13922
   163
apply (frule_tac hr_form, assumption)
paulson@13922
   164
apply (elim disjE exE) 
paulson@13922
   165
apply (simp_all add: parts_insert2) 
paulson@14145
   166
 apply (force dest!: parts_insert_subset_Un [THEN [2] rev_subsetD] 
paulson@14145
   167
                     analz_subset_parts [THEN subsetD], blast) 
paulson@13922
   168
done
paulson@13922
   169
paulson@13922
   170
lemma Spy_know_private_keys_iff [simp]:
paulson@13922
   171
    "evs \<in> certified_mail
paulson@13922
   172
     ==> (Key (privateKey b A) \<in> parts (spies evs)) = (A \<in> bad)"
paulson@14207
   173
by blast 
paulson@13922
   174
paulson@13956
   175
lemma Spy_dont_know_TTPKey_parts [simp]:
paulson@14145
   176
     "evs \<in> certified_mail ==> Key (privateKey b TTP) \<notin> parts(spies evs)" 
paulson@13956
   177
by simp
paulson@13934
   178
paulson@13956
   179
lemma Spy_dont_know_TTPKey_analz [simp]:
paulson@14145
   180
     "evs \<in> certified_mail ==> Key (privateKey b TTP) \<notin> analz(spies evs)"
paulson@14145
   181
by auto
paulson@13934
   182
paulson@13934
   183
text{*Thus, prove any goal that assumes that @{term Spy} knows a private key
paulson@13934
   184
belonging to @{term TTP}*}
paulson@13956
   185
declare Spy_dont_know_TTPKey_parts [THEN [2] rev_notE, elim!]
paulson@13934
   186
paulson@13922
   187
paulson@13922
   188
lemma CM3_k_parts_knows_Spy:
paulson@13922
   189
 "[| evs \<in> certified_mail;
paulson@13922
   190
     Notes TTP {|Agent A, Agent TTP,
paulson@13956
   191
                 Crypt (pubEK TTP) {|Agent S, Number AO, Key K, 
paulson@13922
   192
                 Agent R, hs|}, Key (RPwd R), hs|} \<in> set evs|]
paulson@13922
   193
  ==> Key K \<in> parts(spies evs)"
paulson@13922
   194
apply (rotate_tac 1)
paulson@13922
   195
apply (erule rev_mp)
paulson@13922
   196
apply (erule certified_mail.induct, simp_all)
paulson@13922
   197
   apply (blast  intro:parts_insertI)
paulson@13922
   198
txt{*Fake SSL*}
paulson@14145
   199
apply (blast dest: parts.Body) 
paulson@13922
   200
txt{*Message 2*}
paulson@14145
   201
apply (blast dest!: Gets_imp_Says elim!: knows_Spy_partsEs)
paulson@13922
   202
txt{*Message 3*}
paulson@13922
   203
apply (frule_tac hr_form, assumption)
paulson@13922
   204
apply (elim disjE exE) 
paulson@13922
   205
apply (simp_all add: parts_insert2)
paulson@13922
   206
apply (blast intro: subsetD [OF parts_mono [OF Set.subset_insertI]])  
paulson@13922
   207
done
paulson@13922
   208
paulson@13922
   209
lemma Spy_dont_know_RPwd [rule_format]:
paulson@13922
   210
    "evs \<in> certified_mail ==> Key (RPwd A) \<in> parts(spies evs) --> A \<in> bad"
paulson@13922
   211
apply (erule certified_mail.induct, simp_all) 
paulson@13922
   212
txt{*Fake*}
paulson@14207
   213
apply (blast dest: Fake_parts_insert_in_Un) 
paulson@13922
   214
txt{*Message 1*}
paulson@13922
   215
apply blast  
paulson@13922
   216
txt{*Message 3*}
paulson@13922
   217
apply (frule CM3_k_parts_knows_Spy, assumption)
paulson@13922
   218
apply (frule_tac hr_form, assumption)
paulson@13922
   219
apply (elim disjE exE) 
paulson@13922
   220
apply (simp_all add: parts_insert2) 
paulson@14145
   221
apply (force dest!: parts_insert_subset_Un [THEN [2] rev_subsetD]
paulson@14145
   222
                    analz_subset_parts [THEN subsetD])
paulson@13922
   223
done
paulson@13922
   224
paulson@13922
   225
paulson@13922
   226
lemma Spy_know_RPwd_iff [simp]:
paulson@14145
   227
    "evs \<in> certified_mail ==> (Key (RPwd A) \<in> parts(spies evs)) = (A\<in>bad)"
paulson@13922
   228
by (auto simp add: Spy_dont_know_RPwd) 
paulson@13922
   229
paulson@13922
   230
lemma Spy_analz_RPwd_iff [simp]:
paulson@14145
   231
    "evs \<in> certified_mail ==> (Key (RPwd A) \<in> analz(spies evs)) = (A\<in>bad)"
paulson@14145
   232
by (auto simp add: Spy_dont_know_RPwd [OF _ analz_subset_parts [THEN subsetD]])
paulson@13922
   233
paulson@13922
   234
paulson@13922
   235
text{*Unused, but a guarantee of sorts*}
paulson@13922
   236
theorem CertAutenticity:
paulson@13956
   237
     "[|Crypt (priSK TTP) X \<in> parts (spies evs); evs \<in> certified_mail|] 
paulson@13956
   238
      ==> \<exists>A. Says TTP A (Crypt (priSK TTP) X) \<in> set evs"
paulson@13922
   239
apply (erule rev_mp)
paulson@13922
   240
apply (erule certified_mail.induct, simp_all) 
paulson@13922
   241
txt{*Fake*}
paulson@14145
   242
apply (blast dest: Spy_dont_know_private_keys Fake_parts_insert_in_Un)
paulson@13922
   243
txt{*Message 1*}
paulson@13922
   244
apply blast 
paulson@13922
   245
txt{*Message 3*}
paulson@13922
   246
apply (frule_tac hr_form, assumption)
paulson@13922
   247
apply (elim disjE exE) 
paulson@14145
   248
apply (simp_all add: parts_insert2 parts_insert_knows_A) 
paulson@14207
   249
 apply (blast dest!: Fake_parts_sing_imp_Un, blast)
paulson@13922
   250
done
paulson@13922
   251
paulson@13922
   252
paulson@13922
   253
subsection{*Proving Confidentiality Results*}
paulson@13922
   254
paulson@13922
   255
lemma analz_image_freshK [rule_format]:
paulson@13922
   256
 "evs \<in> certified_mail ==>
paulson@13956
   257
   \<forall>K KK. invKey (pubEK TTP) \<notin> KK -->
paulson@14145
   258
          (Key K \<in> analz (Key`KK Un (spies evs))) =
paulson@14145
   259
          (K \<in> KK | Key K \<in> analz (spies evs))"
paulson@13922
   260
apply (erule certified_mail.induct)
paulson@13922
   261
apply (drule_tac [6] A=TTP in symKey_neq_priEK) 
paulson@13922
   262
apply (erule_tac [6] disjE [OF hr_form]) 
paulson@13922
   263
apply (drule_tac [5] CM2_S2TTP_analz_knows_Spy) 
paulson@13922
   264
prefer 9
paulson@13922
   265
apply (elim exE)
paulson@13922
   266
apply (simp_all add: synth_analz_insert_eq
paulson@13922
   267
                     subset_trans [OF _ subset_insertI]
paulson@13922
   268
                     subset_trans [OF _ Un_upper2] 
paulson@13922
   269
                del: image_insert image_Un add: analz_image_freshK_simps)
paulson@13922
   270
done
paulson@13922
   271
paulson@13922
   272
paulson@13922
   273
lemma analz_insert_freshK:
paulson@13956
   274
  "[| evs \<in> certified_mail;  KAB \<noteq> invKey (pubEK TTP) |] ==>
paulson@14145
   275
      (Key K \<in> analz (insert (Key KAB) (spies evs))) =
paulson@14145
   276
      (K = KAB | Key K \<in> analz (spies evs))"
paulson@13922
   277
by (simp only: analz_image_freshK analz_image_freshK_simps)
paulson@13922
   278
paulson@13922
   279
text{*@{term S2TTP} must have originated from a valid sender
paulson@13922
   280
    provided @{term K} is secure.  Proof is surprisingly hard.*}
paulson@13922
   281
paulson@13922
   282
lemma Notes_SSL_imp_used:
paulson@13922
   283
     "[|Notes B {|Agent A, Agent B, X|} \<in> set evs|] ==> X \<in> used evs"
paulson@13922
   284
by (blast dest!: Notes_imp_used)
paulson@13922
   285
paulson@13922
   286
paulson@14145
   287
(*The weaker version, replacing "used evs" by "parts (spies evs)", 
paulson@13922
   288
   isn't inductive: message 3 case can't be proved *)
paulson@13922
   289
lemma S2TTP_sender_lemma [rule_format]:
paulson@13922
   290
 "evs \<in> certified_mail ==>
paulson@14145
   291
    Key K \<notin> analz (spies evs) -->
paulson@13956
   292
    (\<forall>AO. Crypt (pubEK TTP)
paulson@13922
   293
	   {|Agent S, Number AO, Key K, Agent R, hs|} \<in> used evs -->
paulson@13922
   294
    (\<exists>m ctxt q. 
paulson@13922
   295
        hs = Hash{|Number ctxt, Nonce q, response S R q, Crypt K (Number m)|} &
paulson@13922
   296
	Says S R
paulson@13922
   297
	   {|Agent S, Agent TTP, Crypt K (Number m), Number AO,
paulson@13922
   298
	     Number ctxt, Nonce q,
paulson@13956
   299
	     Crypt (pubEK TTP)
paulson@13922
   300
	      {|Agent S, Number AO, Key K, Agent R, hs |}|} \<in> set evs))" 
paulson@13922
   301
apply (erule certified_mail.induct, analz_mono_contra)
paulson@13922
   302
apply (drule_tac [5] CM2_S2TTP_parts_knows_Spy, simp)
paulson@13922
   303
apply (simp add: used_Nil Crypt_notin_initState, simp_all)
paulson@13922
   304
txt{*Fake*}
paulson@14145
   305
apply (blast dest: Fake_parts_sing [THEN subsetD]
paulson@14145
   306
             dest!: analz_subset_parts [THEN subsetD])  
paulson@13922
   307
txt{*Fake SSL*}
paulson@14145
   308
apply (blast dest: Fake_parts_sing [THEN subsetD]
paulson@14145
   309
             dest: analz_subset_parts [THEN subsetD])  
paulson@13922
   310
txt{*Message 1*}
paulson@13956
   311
apply (clarsimp, blast)
paulson@13922
   312
txt{*Message 2*}
paulson@13922
   313
apply (simp add: parts_insert2, clarify) 
paulson@13922
   314
apply (drule parts_cut, assumption, simp) 
paulson@13934
   315
apply (blast intro: usedI) 
paulson@13922
   316
txt{*Message 3*} 
paulson@13922
   317
apply (blast dest: Notes_SSL_imp_used used_parts_subset_parts) 
paulson@13922
   318
done 
paulson@13922
   319
paulson@13922
   320
lemma S2TTP_sender:
paulson@13956
   321
 "[|Crypt (pubEK TTP) {|Agent S, Number AO, Key K, Agent R, hs|} \<in> used evs;
paulson@14145
   322
    Key K \<notin> analz (spies evs);
paulson@13922
   323
    evs \<in> certified_mail|]
paulson@13922
   324
  ==> \<exists>m ctxt q. 
paulson@13922
   325
        hs = Hash{|Number ctxt, Nonce q, response S R q, Crypt K (Number m)|} &
paulson@13922
   326
	Says S R
paulson@13922
   327
	   {|Agent S, Agent TTP, Crypt K (Number m), Number AO,
paulson@13922
   328
	     Number ctxt, Nonce q,
paulson@13956
   329
	     Crypt (pubEK TTP)
paulson@13922
   330
	      {|Agent S, Number AO, Key K, Agent R, hs |}|} \<in> set evs" 
paulson@13922
   331
by (blast intro: S2TTP_sender_lemma) 
paulson@13922
   332
paulson@13922
   333
paulson@13922
   334
text{*Nobody can have used non-existent keys!*}
paulson@14207
   335
lemma new_keys_not_used [simp]:
paulson@13922
   336
    "[|Key K \<notin> used evs; K \<in> symKeys; evs \<in> certified_mail|]
paulson@13922
   337
     ==> K \<notin> keysFor (parts (spies evs))"
paulson@13922
   338
apply (erule rev_mp) 
paulson@13922
   339
apply (erule certified_mail.induct, simp_all) 
paulson@13922
   340
txt{*Fake*}
paulson@13922
   341
apply (force dest!: keysFor_parts_insert) 
paulson@13922
   342
txt{*Message 1*}
paulson@13922
   343
apply blast 
paulson@13922
   344
txt{*Message 3*}
paulson@13922
   345
apply (frule CM3_k_parts_knows_Spy, assumption)
paulson@13922
   346
apply (frule_tac hr_form, assumption) 
paulson@13922
   347
apply (force dest!: keysFor_parts_insert)
paulson@13922
   348
done
paulson@13922
   349
paulson@13922
   350
paulson@13922
   351
text{*Less easy to prove @{term "m'=m"}.  Maybe needs a separate unicity
paulson@13926
   352
theorem for ciphertexts of the form @{term "Crypt K (Number m)"}, 
paulson@13922
   353
where @{term K} is secure.*}
paulson@13922
   354
lemma Key_unique_lemma [rule_format]:
paulson@13922
   355
     "evs \<in> certified_mail ==>
paulson@14145
   356
       Key K \<notin> analz (spies evs) -->
paulson@13922
   357
       (\<forall>m cleartext q hs.
paulson@13922
   358
        Says S R
paulson@13922
   359
           {|Agent S, Agent TTP, Crypt K (Number m), Number AO,
paulson@13922
   360
             Number cleartext, Nonce q,
paulson@13956
   361
             Crypt (pubEK TTP) {|Agent S, Number AO, Key K, Agent R, hs|}|}
paulson@13922
   362
          \<in> set evs -->
paulson@13922
   363
       (\<forall>m' cleartext' q' hs'.
paulson@13922
   364
       Says S' R'
paulson@13922
   365
           {|Agent S', Agent TTP, Crypt K (Number m'), Number AO',
paulson@13922
   366
             Number cleartext', Nonce q',
paulson@13956
   367
             Crypt (pubEK TTP) {|Agent S', Number AO', Key K, Agent R', hs'|}|}
paulson@13922
   368
          \<in> set evs --> R' = R & S' = S & AO' = AO & hs' = hs))" 
paulson@13922
   369
apply (erule certified_mail.induct, analz_mono_contra, simp_all)
paulson@14145
   370
 prefer 2
paulson@14145
   371
 txt{*Message 1*}
paulson@14145
   372
 apply (blast dest!: Says_imp_knows_Spy [THEN parts.Inj] new_keys_not_used Crypt_imp_keysFor)
paulson@14145
   373
txt{*Fake*}
paulson@14145
   374
apply (auto dest!: usedI S2TTP_sender analz_subset_parts [THEN subsetD]) 
paulson@13922
   375
done
paulson@13922
   376
paulson@13922
   377
text{*The key determines the sender, recipient and protocol options.*}
paulson@13926
   378
lemma Key_unique:
paulson@13922
   379
      "[|Says S R
paulson@13922
   380
           {|Agent S, Agent TTP, Crypt K (Number m), Number AO,
paulson@13922
   381
             Number cleartext, Nonce q,
paulson@13956
   382
             Crypt (pubEK TTP) {|Agent S, Number AO, Key K, Agent R, hs|}|}
paulson@13922
   383
          \<in> set evs;
paulson@13922
   384
         Says S' R'
paulson@13922
   385
           {|Agent S', Agent TTP, Crypt K (Number m'), Number AO',
paulson@13922
   386
             Number cleartext', Nonce q',
paulson@13956
   387
             Crypt (pubEK TTP) {|Agent S', Number AO', Key K, Agent R', hs'|}|}
paulson@13922
   388
          \<in> set evs;
paulson@14145
   389
         Key K \<notin> analz (spies evs);
paulson@13922
   390
         evs \<in> certified_mail|]
paulson@13922
   391
       ==> R' = R & S' = S & AO' = AO & hs' = hs"
paulson@13922
   392
by (rule Key_unique_lemma, assumption+)
paulson@13922
   393
paulson@13934
   394
paulson@13926
   395
subsection{*The Guarantees for Sender and Recipient*}
paulson@13926
   396
paulson@13934
   397
text{*A Sender's guarantee:
paulson@13934
   398
      If Spy gets the key then @{term R} is bad and @{term S} moreover
paulson@13922
   399
      gets his return receipt (and therefore has no grounds for complaint).*}
paulson@13926
   400
theorem Spy_see_encrypted_key_imp:
paulson@13922
   401
      "[|Says S R {|Agent S, Agent TTP, Crypt K (Number m), Number AO, 
paulson@13922
   402
                     Number cleartext, Nonce q, S2TTP|} \<in> set evs;
paulson@13956
   403
         S2TTP = Crypt (pubEK TTP) {|Agent S, Number AO, Key K, Agent R, hs|};
paulson@14145
   404
         Key K \<in> analz(spies evs);
paulson@13922
   405
	 evs \<in> certified_mail;
paulson@13922
   406
         S\<noteq>Spy|]
paulson@13956
   407
      ==> R \<in> bad & Gets S (Crypt (priSK TTP) S2TTP) \<in> set evs"
paulson@13922
   408
apply (erule rev_mp)
paulson@13922
   409
apply (erule ssubst)
paulson@13956
   410
apply (erule rev_mp)
paulson@13922
   411
apply (erule certified_mail.induct, simp_all)
paulson@13922
   412
txt{*Fake*}
paulson@13922
   413
apply spy_analz
paulson@13922
   414
txt{*Fake SSL*}
paulson@13922
   415
apply spy_analz
paulson@13922
   416
txt{*Message 3*}
paulson@13922
   417
apply (frule_tac hr_form, assumption)
paulson@13922
   418
apply (elim disjE exE) 
paulson@13922
   419
apply (simp_all add: synth_analz_insert_eq  
paulson@13922
   420
                     subset_trans [OF _ subset_insertI]
paulson@13922
   421
                     subset_trans [OF _ Un_upper2] 
paulson@13922
   422
                del: image_insert image_Un add: analz_image_freshK_simps) 
paulson@13922
   423
apply (simp_all add: symKey_neq_priEK analz_insert_freshK)
paulson@13922
   424
apply (blast dest: Notes_SSL_imp_used S2TTP_sender Key_unique)+
paulson@13922
   425
done
paulson@13922
   426
paulson@13922
   427
text{*Confidentially for the symmetric key*}
paulson@13922
   428
theorem Spy_not_see_encrypted_key:
paulson@13922
   429
      "[|Says S R {|Agent S, Agent TTP, Crypt K (Number m), Number AO, 
paulson@13922
   430
                     Number cleartext, Nonce q, S2TTP|} \<in> set evs;
paulson@13956
   431
         S2TTP = Crypt (pubEK TTP) {|Agent S, Number AO, Key K, Agent R, hs|};
paulson@13922
   432
	 evs \<in> certified_mail;
paulson@13922
   433
         S\<noteq>Spy; R \<notin> bad|]
paulson@14145
   434
      ==> Key K \<notin> analz(spies evs)"
paulson@13922
   435
by (blast dest: Spy_see_encrypted_key_imp) 
paulson@13922
   436
paulson@13922
   437
paulson@13922
   438
text{*Agent @{term R}, who may be the Spy, doesn't receive the key
paulson@13922
   439
 until @{term S} has access to the return receipt.*} 
paulson@13922
   440
theorem S_guarantee:
paulson@13956
   441
      "[|Says S R {|Agent S, Agent TTP, Crypt K (Number m), Number AO, 
paulson@13922
   442
                     Number cleartext, Nonce q, S2TTP|} \<in> set evs;
paulson@13956
   443
         S2TTP = Crypt (pubEK TTP) {|Agent S, Number AO, Key K, Agent R, hs|};
paulson@13956
   444
         Notes R {|Agent TTP, Agent R, Key K, hs|} \<in> set evs;
paulson@13922
   445
         S\<noteq>Spy;  evs \<in> certified_mail|]
paulson@13956
   446
      ==> Gets S (Crypt (priSK TTP) S2TTP) \<in> set evs"
paulson@13922
   447
apply (erule rev_mp)
paulson@13922
   448
apply (erule ssubst)
paulson@13956
   449
apply (erule rev_mp)
paulson@13922
   450
apply (erule certified_mail.induct, simp_all)
paulson@13922
   451
txt{*Message 1*}
paulson@13922
   452
apply (blast dest: Notes_imp_used) 
paulson@13922
   453
txt{*Message 3*} 
paulson@13922
   454
apply (blast dest: Notes_SSL_imp_used S2TTP_sender Key_unique 
paulson@13922
   455
                   Spy_see_encrypted_key_imp) 
paulson@13922
   456
done
paulson@13922
   457
paulson@13922
   458
paulson@13922
   459
text{*Recipient's guarantee: if @{term R} sends message 2, and
paulson@13934
   460
     a delivery certificate exists, then @{term R}
paulson@13922
   461
     receives the necessary key.*}
paulson@13922
   462
theorem R_guarantee:
paulson@13956
   463
  "[|Crypt (priSK TTP) S2TTP \<in> used evs;
paulson@13956
   464
     S2TTP = Crypt (pubEK TTP)
paulson@13934
   465
               {|Agent S, Number AO, Key K, Agent R, 
paulson@13934
   466
                 Hash {|Number cleartext, Nonce q, r, em|}|};
paulson@13922
   467
     hr = Hash {|Number cleartext, Nonce q, r, em|};
paulson@13922
   468
     R\<noteq>Spy;  evs \<in> certified_mail|]
paulson@13922
   469
  ==> Notes R {|Agent TTP, Agent R, Key K, hr|} \<in> set evs"
paulson@13922
   470
apply (erule rev_mp)
paulson@13922
   471
apply (erule ssubst)
paulson@13922
   472
apply (erule ssubst)
paulson@13922
   473
apply (erule certified_mail.induct, simp_all)
paulson@13934
   474
txt{*Fake*} 
paulson@14145
   475
apply (blast dest: Fake_parts_sing [THEN subsetD]
paulson@14145
   476
             dest!: analz_subset_parts [THEN subsetD])  
paulson@13934
   477
txt{*Fake SSL*}
paulson@14145
   478
apply (blast dest: Fake_parts_sing [THEN subsetD]
paulson@14145
   479
            dest!: analz_subset_parts [THEN subsetD])  
paulson@13922
   480
txt{*Message 2*}
paulson@13934
   481
apply (drule CM2_S2TTP_parts_knows_Spy, assumption)
paulson@13934
   482
apply (force dest: parts_cut)
paulson@13934
   483
txt{*Message 3*}
paulson@13934
   484
apply (frule_tac hr_form, assumption)
paulson@13934
   485
apply (elim disjE exE, simp_all) 
paulson@14145
   486
apply (blast dest: Fake_parts_sing [THEN subsetD]
paulson@14145
   487
             dest!: analz_subset_parts [THEN subsetD]) 
paulson@13922
   488
done
paulson@13922
   489
paulson@13922
   490
end