src/HOL/Auth/Guard/P2.thy
author wenzelm
Mon Aug 31 21:28:08 2015 +0200 (2015-08-31)
changeset 61070 b72a990adfe2
parent 58889 5b7a9633cfa8
child 61830 4f5ab843cf5b
permissions -rw-r--r--
prefer symbols;
wenzelm@41775
     1
(*  Title:      HOL/Auth/Guard/P2.thy
wenzelm@41775
     2
    Author:     Frederic Blanqui, University of Cambridge Computer Laboratory
wenzelm@41775
     3
    Copyright   2002  University of Cambridge
paulson@13508
     4
wenzelm@41775
     5
From G. Karjoth, N. Asokan and C. Gulcu
wenzelm@41775
     6
"Protecting the computation results of free-roaming agents"
wenzelm@41775
     7
Mobiles Agents 1998, LNCS 1477.
wenzelm@41775
     8
*)
paulson@13508
     9
wenzelm@58889
    10
section{*Protocol P2*}
paulson@13508
    11
haftmann@16417
    12
theory P2 imports Guard_Public List_Msg begin
paulson@13508
    13
paulson@13508
    14
subsection{*Protocol Definition*}
paulson@13508
    15
paulson@13508
    16
paulson@13508
    17
text{*Like P1 except the definitions of @{text chain}, @{text shop},
paulson@13508
    18
  @{text next_shop} and @{text nonce}*}
paulson@13508
    19
paulson@13508
    20
subsubsection{*offer chaining:
paulson@13508
    21
B chains his offer for A with the head offer of L for sending it to C*}
paulson@13508
    22
haftmann@35416
    23
definition chain :: "agent => nat => agent => msg => agent => msg" where
paulson@13508
    24
"chain B ofr A L C ==
paulson@13508
    25
let m1= sign B (Nonce ofr) in
paulson@13508
    26
let m2= Hash {|head L, Agent C|} in
paulson@13508
    27
{|Crypt (pubK A) m1, m2|}"
paulson@13508
    28
paulson@13508
    29
declare Let_def [simp]
paulson@13508
    30
paulson@13508
    31
lemma chain_inj [iff]: "(chain B ofr A L C = chain B' ofr' A' L' C')
paulson@13508
    32
= (B=B' & ofr=ofr' & A=A' & head L = head L' & C=C')"
paulson@13508
    33
by (auto simp: chain_def Let_def)
paulson@13508
    34
paulson@13508
    35
lemma Nonce_in_chain [iff]: "Nonce ofr:parts {chain B ofr A L C}"
paulson@13508
    36
by (auto simp: chain_def sign_def)
paulson@13508
    37
paulson@13508
    38
subsubsection{*agent whose key is used to sign an offer*}
paulson@13508
    39
krauss@35418
    40
fun shop :: "msg => msg" where
paulson@13508
    41
"shop {|Crypt K {|B,ofr,Crypt K' H|},m2|} = Agent (agt K')"
paulson@13508
    42
paulson@13508
    43
lemma shop_chain [simp]: "shop (chain B ofr A L C) = Agent B"
paulson@13508
    44
by (simp add: chain_def sign_def)
paulson@13508
    45
paulson@13508
    46
subsubsection{*nonce used in an offer*}
paulson@13508
    47
krauss@35418
    48
fun nonce :: "msg => msg" where
paulson@13508
    49
"nonce {|Crypt K {|B,ofr,CryptH|},m2|} = ofr"
paulson@13508
    50
paulson@13508
    51
lemma nonce_chain [simp]: "nonce (chain B ofr A L C) = Nonce ofr"
paulson@13508
    52
by (simp add: chain_def sign_def)
paulson@13508
    53
paulson@13508
    54
subsubsection{*next shop*}
paulson@13508
    55
krauss@35418
    56
fun next_shop :: "msg => agent" where
paulson@13508
    57
"next_shop {|m1,Hash {|headL,Agent C|}|} = C"
paulson@13508
    58
paulson@13508
    59
lemma "next_shop (chain B ofr A L C) = C"
paulson@13508
    60
by (simp add: chain_def sign_def)
paulson@13508
    61
paulson@13508
    62
subsubsection{*anchor of the offer list*}
paulson@13508
    63
haftmann@35416
    64
definition anchor :: "agent => nat => agent => msg" where
paulson@13508
    65
"anchor A n B == chain A n A (cons nil nil) B"
paulson@13508
    66
paulson@13508
    67
lemma anchor_inj [iff]:
paulson@13508
    68
     "(anchor A n B = anchor A' n' B') = (A=A' & n=n' & B=B')"
paulson@13508
    69
by (auto simp: anchor_def)
paulson@13508
    70
paulson@13508
    71
lemma Nonce_in_anchor [iff]: "Nonce n:parts {anchor A n B}"
paulson@13508
    72
by (auto simp: anchor_def)
paulson@13508
    73
paulson@13508
    74
lemma shop_anchor [simp]: "shop (anchor A n B) = Agent A"
paulson@13508
    75
by (simp add: anchor_def)
paulson@13508
    76
paulson@13508
    77
subsubsection{*request event*}
paulson@13508
    78
haftmann@35416
    79
definition reqm :: "agent => nat => nat => msg => agent => msg" where
paulson@13508
    80
"reqm A r n I B == {|Agent A, Number r, cons (Agent A) (cons (Agent B) I),
paulson@13508
    81
cons (anchor A n B) nil|}"
paulson@13508
    82
paulson@13508
    83
lemma reqm_inj [iff]: "(reqm A r n I B = reqm A' r' n' I' B')
paulson@13508
    84
= (A=A' & r=r' & n=n' & I=I' & B=B')"
paulson@13508
    85
by (auto simp: reqm_def)
paulson@13508
    86
paulson@13508
    87
lemma Nonce_in_reqm [iff]: "Nonce n:parts {reqm A r n I B}"
paulson@13508
    88
by (auto simp: reqm_def)
paulson@13508
    89
haftmann@35416
    90
definition req :: "agent => nat => nat => msg => agent => event" where
paulson@13508
    91
"req A r n I B == Says A B (reqm A r n I B)"
paulson@13508
    92
paulson@13508
    93
lemma req_inj [iff]: "(req A r n I B = req A' r' n' I' B')
paulson@13508
    94
= (A=A' & r=r' & n=n' & I=I' & B=B')"
paulson@13508
    95
by (auto simp: req_def)
paulson@13508
    96
paulson@13508
    97
subsubsection{*propose event*}
paulson@13508
    98
haftmann@35416
    99
definition prom :: "agent => nat => agent => nat => msg => msg =>
haftmann@35416
   100
msg => agent => msg" where
paulson@13508
   101
"prom B ofr A r I L J C == {|Agent A, Number r,
paulson@13508
   102
app (J, del (Agent B, I)), cons (chain B ofr A L C) L|}"
paulson@13508
   103
paulson@13508
   104
lemma prom_inj [dest]: "prom B ofr A r I L J C = prom B' ofr' A' r' I' L' J' C'
paulson@13508
   105
==> B=B' & ofr=ofr' & A=A' & r=r' & L=L' & C=C'"
paulson@13508
   106
by (auto simp: prom_def)
paulson@13508
   107
paulson@13508
   108
lemma Nonce_in_prom [iff]: "Nonce ofr:parts {prom B ofr A r I L J C}"
paulson@13508
   109
by (auto simp: prom_def)
paulson@13508
   110
haftmann@35416
   111
definition pro :: "agent => nat => agent => nat => msg => msg =>
haftmann@35416
   112
                  msg => agent => event" where
paulson@13508
   113
"pro B ofr A r I L J C == Says B C (prom B ofr A r I L J C)"
paulson@13508
   114
paulson@13508
   115
lemma pro_inj [dest]: "pro B ofr A r I L J C = pro B' ofr' A' r' I' L' J' C'
paulson@13508
   116
==> B=B' & ofr=ofr' & A=A' & r=r' & L=L' & C=C'"
paulson@13508
   117
by (auto simp: pro_def dest: prom_inj)
paulson@13508
   118
paulson@13508
   119
subsubsection{*protocol*}
paulson@13508
   120
berghofe@23746
   121
inductive_set p2 :: "event list set"
berghofe@23746
   122
where
paulson@13508
   123
berghofe@23746
   124
  Nil: "[]:p2"
paulson@13508
   125
berghofe@23746
   126
| Fake: "[| evsf:p2; X:synth (analz (spies evsf)) |] ==> Says Spy B X # evsf : p2"
paulson@13508
   127
berghofe@23746
   128
| Request: "[| evsr:p2; Nonce n ~:used evsr; I:agl |] ==> req A r n I B # evsr : p2"
paulson@13508
   129
berghofe@23746
   130
| Propose: "[| evsp:p2; Says A' B {|Agent A,Number r,I,cons M L|}:set evsp;
berghofe@23746
   131
  I:agl; J:agl; isin (Agent C, app (J, del (Agent B, I)));
berghofe@23746
   132
  Nonce ofr ~:used evsp |] ==> pro B ofr A r I (cons M L) J C # evsp : p2"
paulson@13508
   133
paulson@13508
   134
subsubsection{*valid offer lists*}
paulson@13508
   135
berghofe@23746
   136
inductive_set
berghofe@23746
   137
  valid :: "agent => nat => agent => msg set"
berghofe@23746
   138
  for A :: agent and  n :: nat and B :: agent
berghofe@23746
   139
where
berghofe@23746
   140
  Request [intro]: "cons (anchor A n B) nil:valid A n B"
paulson@13508
   141
berghofe@23746
   142
| Propose [intro]: "L:valid A n B
berghofe@23746
   143
  ==> cons (chain (next_shop (head L)) ofr A L C) L:valid A n B"
paulson@13508
   144
paulson@13508
   145
subsubsection{*basic properties of valid*}
paulson@13508
   146
paulson@13508
   147
lemma valid_not_empty: "L:valid A n B ==> EX M L'. L = cons M L'"
paulson@13508
   148
by (erule valid.cases, auto)
paulson@13508
   149
paulson@13508
   150
lemma valid_pos_len: "L:valid A n B ==> 0 < len L"
paulson@13508
   151
by (erule valid.induct, auto)
paulson@13508
   152
paulson@13508
   153
subsubsection{*list of offers*}
paulson@13508
   154
krauss@35418
   155
fun offers :: "msg => msg"
krauss@35418
   156
where
krauss@35418
   157
  "offers (cons M L) = cons {|shop M, nonce M|} (offers L)"
krauss@35418
   158
| "offers other = nil"
paulson@13508
   159
paulson@13508
   160
paulson@13508
   161
subsection{*Properties of Protocol P2*}
paulson@13508
   162
paulson@13508
   163
text{*same as @{text P1_Prop} except that publicly verifiable forward
paulson@13508
   164
integrity is replaced by forward privacy*}
paulson@13508
   165
paulson@13508
   166
subsection{*strong forward integrity:
paulson@13508
   167
except the last one, no offer can be modified*}
paulson@13508
   168
paulson@13508
   169
lemma strong_forward_integrity: "ALL L. Suc i < len L
paulson@13508
   170
--> L:valid A n B --> repl (L,Suc i,M):valid A n B --> M = ith (L,Suc i)"
paulson@13508
   171
apply (induct i)
paulson@13508
   172
(* i = 0 *)
paulson@13508
   173
apply clarify
paulson@13508
   174
apply (frule len_not_empty, clarsimp)
paulson@13508
   175
apply (frule len_not_empty, clarsimp)
berghofe@23746
   176
apply (ind_cases "{|x,xa,l'a|}:valid A n B" for x xa l'a)
berghofe@23746
   177
apply (ind_cases "{|x,M,l'a|}:valid A n B" for x l'a)
paulson@13508
   178
apply (simp add: chain_def)
paulson@13508
   179
(* i > 0 *)
paulson@13508
   180
apply clarify
paulson@13508
   181
apply (frule len_not_empty, clarsimp)
berghofe@23746
   182
apply (ind_cases "{|x,repl(l',Suc na,M)|}:valid A n B" for x l' na)
paulson@13508
   183
apply (frule len_not_empty, clarsimp)
berghofe@23746
   184
apply (ind_cases "{|x,l'|}:valid A n B" for x l')
paulson@13508
   185
by (drule_tac x=l' in spec, simp, blast)
paulson@13508
   186
paulson@13508
   187
subsection{*insertion resilience:
paulson@13508
   188
except at the beginning, no offer can be inserted*}
paulson@13508
   189
paulson@13508
   190
lemma chain_isnt_head [simp]: "L:valid A n B ==>
paulson@13508
   191
head L ~= chain (next_shop (head L)) ofr A L C"
paulson@13508
   192
by (erule valid.induct, auto simp: chain_def sign_def anchor_def)
paulson@13508
   193
paulson@13508
   194
lemma insertion_resilience: "ALL L. L:valid A n B --> Suc i < len L
paulson@13508
   195
--> ins (L,Suc i,M) ~:valid A n B"
paulson@13508
   196
apply (induct i)
paulson@13508
   197
(* i = 0 *)
paulson@13508
   198
apply clarify
paulson@13508
   199
apply (frule len_not_empty, clarsimp)
berghofe@23746
   200
apply (ind_cases "{|x,l'|}:valid A n B" for x l', simp)
berghofe@23746
   201
apply (ind_cases "{|x,M,l'|}:valid A n B" for x l', clarsimp)
berghofe@23746
   202
apply (ind_cases "{|head l',l'|}:valid A n B" for l', simp, simp)
paulson@13508
   203
(* i > 0 *)
paulson@13508
   204
apply clarify
paulson@13508
   205
apply (frule len_not_empty, clarsimp)
berghofe@23746
   206
apply (ind_cases "{|x,l'|}:valid A n B" for x l')
paulson@13508
   207
apply (frule len_not_empty, clarsimp)
berghofe@23746
   208
apply (ind_cases "{|x,ins(l',Suc na,M)|}:valid A n B" for x l' na)
paulson@13508
   209
apply (frule len_not_empty, clarsimp)
paulson@13508
   210
by (drule_tac x=l' in spec, clarsimp)
paulson@13508
   211
paulson@13508
   212
subsection{*truncation resilience:
paulson@13508
   213
only shop i can truncate at offer i*}
paulson@13508
   214
paulson@13508
   215
lemma truncation_resilience: "ALL L. L:valid A n B --> Suc i < len L
paulson@13508
   216
--> cons M (trunc (L,Suc i)):valid A n B --> shop M = shop (ith (L,i))"
paulson@13508
   217
apply (induct i)
paulson@13508
   218
(* i = 0 *)
paulson@13508
   219
apply clarify
paulson@13508
   220
apply (frule len_not_empty, clarsimp)
berghofe@23746
   221
apply (ind_cases "{|x,l'|}:valid A n B" for x l')
paulson@13508
   222
apply (frule len_not_empty, clarsimp)
berghofe@23746
   223
apply (ind_cases "{|M,l'|}:valid A n B" for l')
paulson@13508
   224
apply (frule len_not_empty, clarsimp, simp)
paulson@13508
   225
(* i > 0 *)
paulson@13508
   226
apply clarify
paulson@13508
   227
apply (frule len_not_empty, clarsimp)
berghofe@23746
   228
apply (ind_cases "{|x,l'|}:valid A n B" for x l')
paulson@13508
   229
apply (frule len_not_empty, clarsimp)
paulson@13508
   230
by (drule_tac x=l' in spec, clarsimp)
paulson@13508
   231
paulson@13508
   232
subsection{*declarations for tactics*}
paulson@13508
   233
paulson@13508
   234
declare knows_Spy_partsEs [elim]
paulson@13508
   235
declare Fake_parts_insert [THEN subsetD, dest]
paulson@13508
   236
declare initState.simps [simp del]
paulson@13508
   237
paulson@13508
   238
subsection{*get components of a message*}
paulson@13508
   239
paulson@13508
   240
lemma get_ML [dest]: "Says A' B {|A,R,I,M,L|}:set evs ==>
paulson@13508
   241
M:parts (spies evs) & L:parts (spies evs)"
paulson@13508
   242
by blast
paulson@13508
   243
paulson@13508
   244
subsection{*general properties of p2*}
paulson@13508
   245
paulson@13508
   246
lemma reqm_neq_prom [iff]:
paulson@13508
   247
"reqm A r n I B ~= prom B' ofr A' r' I' (cons M L) J C"
paulson@13508
   248
by (auto simp: reqm_def prom_def)
paulson@13508
   249
paulson@13508
   250
lemma prom_neq_reqm [iff]:
paulson@13508
   251
"prom B' ofr A' r' I' (cons M L) J C ~= reqm A r n I B"
paulson@13508
   252
by (auto simp: reqm_def prom_def)
paulson@13508
   253
paulson@13508
   254
lemma req_neq_pro [iff]: "req A r n I B ~= pro B' ofr A' r' I' (cons M L) J C"
paulson@13508
   255
by (auto simp: req_def pro_def)
paulson@13508
   256
paulson@13508
   257
lemma pro_neq_req [iff]: "pro B' ofr A' r' I' (cons M L) J C ~= req A r n I B"
paulson@13508
   258
by (auto simp: req_def pro_def)
paulson@13508
   259
paulson@13508
   260
lemma p2_has_no_Gets: "evs:p2 ==> ALL A X. Gets A X ~:set evs"
paulson@13508
   261
by (erule p2.induct, auto simp: req_def pro_def)
paulson@13508
   262
paulson@13508
   263
lemma p2_is_Gets_correct [iff]: "Gets_correct p2"
paulson@13508
   264
by (auto simp: Gets_correct_def dest: p2_has_no_Gets)
paulson@13508
   265
paulson@13508
   266
lemma p2_is_one_step [iff]: "one_step p2"
berghofe@23746
   267
by (unfold one_step_def, clarify, ind_cases "ev#evs:p2" for ev evs, auto)
paulson@13508
   268
paulson@13508
   269
lemma p2_has_only_Says' [rule_format]: "evs:p2 ==>
paulson@13508
   270
ev:set evs --> (EX A B X. ev=Says A B X)"
paulson@13508
   271
by (erule p2.induct, auto simp: req_def pro_def)
paulson@13508
   272
paulson@13508
   273
lemma p2_has_only_Says [iff]: "has_only_Says p2"
paulson@13508
   274
by (auto simp: has_only_Says_def dest: p2_has_only_Says')
paulson@13508
   275
paulson@13508
   276
lemma p2_is_regular [iff]: "regular p2"
paulson@13508
   277
apply (simp only: regular_def, clarify)
paulson@13508
   278
apply (erule_tac p2.induct)
paulson@13508
   279
apply (simp_all add: initState.simps knows.simps pro_def prom_def
paulson@13508
   280
req_def reqm_def anchor_def chain_def sign_def)
paulson@13508
   281
by (auto dest: no_Key_in_agl no_Key_in_appdel parts_trans)
paulson@13508
   282
paulson@13508
   283
subsection{*private keys are safe*}
paulson@13508
   284
paulson@13508
   285
lemma priK_parts_Friend_imp_bad [rule_format,dest]:
paulson@13508
   286
     "[| evs:p2; Friend B ~= A |]
paulson@13508
   287
      ==> (Key (priK A):parts (knows (Friend B) evs)) --> (A:bad)"
paulson@13508
   288
apply (erule p2.induct)
paulson@13508
   289
apply (simp_all add: initState.simps knows.simps pro_def prom_def
nipkow@17778
   290
                req_def reqm_def anchor_def chain_def sign_def) 
paulson@13508
   291
apply (blast dest: no_Key_in_agl)
paulson@13508
   292
apply (auto del: parts_invKey disjE  dest: parts_trans
paulson@13508
   293
            simp add: no_Key_in_appdel)
paulson@13508
   294
done
paulson@13508
   295
paulson@13508
   296
lemma priK_analz_Friend_imp_bad [rule_format,dest]:
paulson@13508
   297
     "[| evs:p2; Friend B ~= A |]
paulson@13508
   298
==> (Key (priK A):analz (knows (Friend B) evs)) --> (A:bad)"
paulson@13508
   299
by auto
paulson@13508
   300
paulson@13508
   301
lemma priK_notin_knows_max_Friend:
paulson@13508
   302
     "[| evs:p2; A ~:bad; A ~= Friend C |]
paulson@13508
   303
      ==> Key (priK A) ~:analz (knows_max (Friend C) evs)"
paulson@13508
   304
apply (rule not_parts_not_analz, simp add: knows_max_def, safe)
paulson@13508
   305
apply (drule_tac H="spies' evs" in parts_sub)
paulson@13508
   306
apply (rule_tac p=p2 in knows_max'_sub_spies', simp+)
paulson@13508
   307
apply (drule_tac H="spies evs" in parts_sub)
paulson@13508
   308
by (auto dest: knows'_sub_knows [THEN subsetD] priK_notin_initState_Friend)
paulson@13508
   309
paulson@13508
   310
subsection{*general guardedness properties*}
paulson@13508
   311
paulson@13508
   312
lemma agl_guard [intro]: "I:agl ==> I:guard n Ks"
paulson@13508
   313
by (erule agl.induct, auto)
paulson@13508
   314
paulson@13508
   315
lemma Says_to_knows_max'_guard: "[| Says A' C {|A'',r,I,L|}:set evs;
paulson@13508
   316
Guard n Ks (knows_max' C evs) |] ==> L:guard n Ks"
paulson@13508
   317
by (auto dest: Says_to_knows_max')
paulson@13508
   318
paulson@13508
   319
lemma Says_from_knows_max'_guard: "[| Says C A' {|A'',r,I,L|}:set evs;
paulson@13508
   320
Guard n Ks (knows_max' C evs) |] ==> L:guard n Ks"
paulson@13508
   321
by (auto dest: Says_from_knows_max')
paulson@13508
   322
paulson@13508
   323
lemma Says_Nonce_not_used_guard: "[| Says A' B {|A'',r,I,L|}:set evs;
paulson@13508
   324
Nonce n ~:used evs |] ==> L:guard n Ks"
paulson@13508
   325
by (drule not_used_not_parts, auto)
paulson@13508
   326
paulson@13508
   327
subsection{*guardedness of messages*}
paulson@13508
   328
paulson@13508
   329
lemma chain_guard [iff]: "chain B ofr A L C:guard n {priK A}"
paulson@13508
   330
by (case_tac "ofr=n", auto simp: chain_def sign_def)
paulson@13508
   331
paulson@13508
   332
lemma chain_guard_Nonce_neq [intro]: "n ~= ofr
paulson@13508
   333
==> chain B ofr A' L C:guard n {priK A}"
paulson@13508
   334
by (auto simp: chain_def sign_def)
paulson@13508
   335
paulson@13508
   336
lemma anchor_guard [iff]: "anchor A n' B:guard n {priK A}"
paulson@13508
   337
by (case_tac "n'=n", auto simp: anchor_def)
paulson@13508
   338
paulson@13508
   339
lemma anchor_guard_Nonce_neq [intro]: "n ~= n'
paulson@13508
   340
==> anchor A' n' B:guard n {priK A}"
paulson@13508
   341
by (auto simp: anchor_def)
paulson@13508
   342
paulson@13508
   343
lemma reqm_guard [intro]: "I:agl ==> reqm A r n' I B:guard n {priK A}"
paulson@13508
   344
by (case_tac "n'=n", auto simp: reqm_def)
paulson@13508
   345
paulson@13508
   346
lemma reqm_guard_Nonce_neq [intro]: "[| n ~= n'; I:agl |]
paulson@13508
   347
==> reqm A' r n' I B:guard n {priK A}"
paulson@13508
   348
by (auto simp: reqm_def)
paulson@13508
   349
paulson@13508
   350
lemma prom_guard [intro]: "[| I:agl; J:agl; L:guard n {priK A} |]
paulson@13508
   351
==> prom B ofr A r I L J C:guard n {priK A}"
paulson@13508
   352
by (auto simp: prom_def)
paulson@13508
   353
paulson@13508
   354
lemma prom_guard_Nonce_neq [intro]: "[| n ~= ofr; I:agl; J:agl;
paulson@13508
   355
L:guard n {priK A} |] ==> prom B ofr A' r I L J C:guard n {priK A}"
paulson@13508
   356
by (auto simp: prom_def)
paulson@13508
   357
paulson@13508
   358
subsection{*Nonce uniqueness*}
paulson@13508
   359
paulson@13508
   360
lemma uniq_Nonce_in_chain [dest]: "Nonce k:parts {chain B ofr A L C} ==> k=ofr"
paulson@13508
   361
by (auto simp: chain_def sign_def)
paulson@13508
   362
paulson@13508
   363
lemma uniq_Nonce_in_anchor [dest]: "Nonce k:parts {anchor A n B} ==> k=n"
paulson@13508
   364
by (auto simp: anchor_def chain_def sign_def)
paulson@13508
   365
paulson@13508
   366
lemma uniq_Nonce_in_reqm [dest]: "[| Nonce k:parts {reqm A r n I B};
paulson@13508
   367
I:agl |] ==> k=n"
paulson@13508
   368
by (auto simp: reqm_def dest: no_Nonce_in_agl)
paulson@13508
   369
paulson@13508
   370
lemma uniq_Nonce_in_prom [dest]: "[| Nonce k:parts {prom B ofr A r I L J C};
paulson@13508
   371
I:agl; J:agl; Nonce k ~:parts {L} |] ==> k=ofr"
paulson@13508
   372
by (auto simp: prom_def dest: no_Nonce_in_agl no_Nonce_in_appdel)
paulson@13508
   373
paulson@13508
   374
subsection{*requests are guarded*}
paulson@13508
   375
paulson@13508
   376
lemma req_imp_Guard [rule_format]: "[| evs:p2; A ~:bad |] ==>
paulson@13508
   377
req A r n I B:set evs --> Guard n {priK A} (spies evs)"
paulson@13508
   378
apply (erule p2.induct, simp)
paulson@13508
   379
apply (simp add: req_def knows.simps, safe)
paulson@13508
   380
apply (erule in_synth_Guard, erule Guard_analz, simp)
paulson@13508
   381
by (auto simp: req_def pro_def dest: Says_imp_knows_Spy)
paulson@13508
   382
paulson@13508
   383
lemma req_imp_Guard_Friend: "[| evs:p2; A ~:bad; req A r n I B:set evs |]
paulson@13508
   384
==> Guard n {priK A} (knows_max (Friend C) evs)"
paulson@13508
   385
apply (rule Guard_knows_max')
paulson@13508
   386
apply (rule_tac H="spies evs" in Guard_mono)
paulson@13508
   387
apply (rule req_imp_Guard, simp+)
paulson@13508
   388
apply (rule_tac B="spies' evs" in subset_trans)
paulson@13508
   389
apply (rule_tac p=p2 in knows_max'_sub_spies', simp+)
paulson@13508
   390
by (rule knows'_sub_knows)
paulson@13508
   391
paulson@13508
   392
subsection{*propositions are guarded*}
paulson@13508
   393
paulson@13508
   394
lemma pro_imp_Guard [rule_format]: "[| evs:p2; B ~:bad; A ~:bad |] ==>
paulson@13508
   395
pro B ofr A r I (cons M L) J C:set evs --> Guard ofr {priK A} (spies evs)"
paulson@13508
   396
apply (erule p2.induct) (* +3 subgoals *)
paulson@13508
   397
(* Nil *)
paulson@13508
   398
apply simp
paulson@13508
   399
(* Fake *)
paulson@13508
   400
apply (simp add: pro_def, safe) (* +4 subgoals *)
paulson@13508
   401
(* 1 *)
paulson@13508
   402
apply (erule in_synth_Guard, drule Guard_analz, simp, simp)
paulson@13508
   403
(* 2 *)
paulson@13508
   404
apply simp
paulson@13508
   405
(* 3 *)
paulson@13508
   406
apply (simp, simp add: req_def pro_def, blast)
paulson@13508
   407
(* 4 *)
paulson@13508
   408
apply (simp add: pro_def)
paulson@13508
   409
apply (blast dest: prom_inj Says_Nonce_not_used_guard Nonce_not_used_Guard)
paulson@13508
   410
(* 5 *)
paulson@13508
   411
apply simp
paulson@13508
   412
apply safe (* +1 subgoal *)
paulson@13508
   413
apply (simp add: pro_def)
paulson@13508
   414
apply (blast dest: prom_inj Says_Nonce_not_used_guard)
paulson@13508
   415
(* 6 *)
paulson@13508
   416
apply (simp add: pro_def)
paulson@13508
   417
apply (blast dest: Says_imp_knows_Spy)
paulson@13508
   418
(* Request *)
paulson@13508
   419
apply (simp add: pro_def)
paulson@13508
   420
apply (blast dest: prom_inj Says_Nonce_not_used_guard Nonce_not_used_Guard)
paulson@13508
   421
(* Propose *)
paulson@13508
   422
apply simp
paulson@13508
   423
apply safe (* +1 subgoal *)
paulson@13508
   424
(* 1 *)
paulson@13508
   425
apply (simp add: pro_def)
paulson@13508
   426
apply (blast dest: prom_inj Says_Nonce_not_used_guard)
paulson@13508
   427
(* 2 *)
paulson@13508
   428
apply (simp add: pro_def)
paulson@13508
   429
by (blast dest: Says_imp_knows_Spy)
paulson@13508
   430
paulson@13508
   431
lemma pro_imp_Guard_Friend: "[| evs:p2; B ~:bad; A ~:bad;
paulson@13508
   432
pro B ofr A r I (cons M L) J C:set evs |]
paulson@13508
   433
==> Guard ofr {priK A} (knows_max (Friend D) evs)"
paulson@13508
   434
apply (rule Guard_knows_max')
paulson@13508
   435
apply (rule_tac H="spies evs" in Guard_mono)
paulson@13508
   436
apply (rule pro_imp_Guard, simp+)
paulson@13508
   437
apply (rule_tac B="spies' evs" in subset_trans)
paulson@13508
   438
apply (rule_tac p=p2 in knows_max'_sub_spies', simp+)
paulson@13508
   439
by (rule knows'_sub_knows)
paulson@13508
   440
paulson@13508
   441
subsection{*data confidentiality:
paulson@13508
   442
no one other than the originator can decrypt the offers*}
paulson@13508
   443
paulson@13508
   444
lemma Nonce_req_notin_spies: "[| evs:p2; req A r n I B:set evs; A ~:bad |]
paulson@13508
   445
==> Nonce n ~:analz (spies evs)"
paulson@13508
   446
by (frule req_imp_Guard, simp+, erule Guard_Nonce_analz, simp+)
paulson@13508
   447
paulson@13508
   448
lemma Nonce_req_notin_knows_max_Friend: "[| evs:p2; req A r n I B:set evs;
paulson@13508
   449
A ~:bad; A ~= Friend C |] ==> Nonce n ~:analz (knows_max (Friend C) evs)"
paulson@13508
   450
apply (clarify, frule_tac C=C in req_imp_Guard_Friend, simp+)
paulson@13508
   451
apply (simp add: knows_max_def, drule Guard_invKey_keyset, simp+)
paulson@13508
   452
by (drule priK_notin_knows_max_Friend, auto simp: knows_max_def)
paulson@13508
   453
paulson@13508
   454
lemma Nonce_pro_notin_spies: "[| evs:p2; B ~:bad; A ~:bad;
paulson@13508
   455
pro B ofr A r I (cons M L) J C:set evs |] ==> Nonce ofr ~:analz (spies evs)"
paulson@13508
   456
by (frule pro_imp_Guard, simp+, erule Guard_Nonce_analz, simp+)
paulson@13508
   457
paulson@13508
   458
lemma Nonce_pro_notin_knows_max_Friend: "[| evs:p2; B ~:bad; A ~:bad;
paulson@13508
   459
A ~= Friend D; pro B ofr A r I (cons M L) J C:set evs |]
paulson@13508
   460
==> Nonce ofr ~:analz (knows_max (Friend D) evs)"
paulson@13508
   461
apply (clarify, frule_tac A=A in pro_imp_Guard_Friend, simp+)
paulson@13508
   462
apply (simp add: knows_max_def, drule Guard_invKey_keyset, simp+)
paulson@13508
   463
by (drule priK_notin_knows_max_Friend, auto simp: knows_max_def)
paulson@13508
   464
paulson@13508
   465
subsection{*forward privacy:
paulson@13508
   466
only the originator can know the identity of the shops*}
paulson@13508
   467
paulson@13508
   468
lemma forward_privacy_Spy: "[| evs:p2; B ~:bad; A ~:bad;
paulson@13508
   469
pro B ofr A r I (cons M L) J C:set evs |]
paulson@13508
   470
==> sign B (Nonce ofr) ~:analz (spies evs)"
paulson@13508
   471
by (auto simp:sign_def dest: Nonce_pro_notin_spies)
paulson@13508
   472
paulson@13508
   473
lemma forward_privacy_Friend: "[| evs:p2; B ~:bad; A ~:bad; A ~= Friend D;
paulson@13508
   474
pro B ofr A r I (cons M L) J C:set evs |]
paulson@13508
   475
==> sign B (Nonce ofr) ~:analz (knows_max (Friend D) evs)"
paulson@13508
   476
by (auto simp:sign_def dest:Nonce_pro_notin_knows_max_Friend )
paulson@13508
   477
paulson@13508
   478
subsection{*non repudiability: an offer signed by B has been sent by B*}
paulson@13508
   479
paulson@13508
   480
lemma Crypt_reqm: "[| Crypt (priK A) X:parts {reqm A' r n I B}; I:agl |] ==> A=A'"
paulson@13508
   481
by (auto simp: reqm_def anchor_def chain_def sign_def dest: no_Crypt_in_agl)
paulson@13508
   482
paulson@13508
   483
lemma Crypt_prom: "[| Crypt (priK A) X:parts {prom B ofr A' r I L J C};
paulson@13508
   484
I:agl; J:agl |] ==> A=B | Crypt (priK A) X:parts {L}"
paulson@13508
   485
apply (simp add: prom_def anchor_def chain_def sign_def)
paulson@13508
   486
by (blast dest: no_Crypt_in_agl no_Crypt_in_appdel)
paulson@13508
   487
paulson@13508
   488
lemma Crypt_safeness: "[| evs:p2; A ~:bad |] ==> Crypt (priK A) X:parts (spies evs)
paulson@13508
   489
--> (EX B Y. Says A B Y:set evs & Crypt (priK A) X:parts {Y})"
paulson@13508
   490
apply (erule p2.induct)
paulson@13508
   491
(* Nil *)
paulson@13508
   492
apply simp
paulson@13508
   493
(* Fake *)
paulson@13508
   494
apply clarsimp
paulson@13508
   495
apply (drule_tac P="%G. Crypt (priK A) X:G" in parts_insert_substD, simp)
paulson@13508
   496
apply (erule disjE)
paulson@13508
   497
apply (drule_tac K="priK A" in Crypt_synth, simp+, blast, blast)
paulson@13508
   498
(* Request *)
paulson@13508
   499
apply (simp add: req_def, clarify)
paulson@13508
   500
apply (drule_tac P="%G. Crypt (priK A) X:G" in parts_insert_substD, simp)
paulson@13508
   501
apply (erule disjE)
paulson@13508
   502
apply (frule Crypt_reqm, simp, clarify)
paulson@13508
   503
apply (rule_tac x=B in exI, rule_tac x="reqm A r n I B" in exI, simp, blast)
paulson@13508
   504
(* Propose *)
paulson@13508
   505
apply (simp add: pro_def, clarify)
paulson@13508
   506
apply (drule_tac P="%G. Crypt (priK A) X:G" in parts_insert_substD, simp)
paulson@13508
   507
apply (rotate_tac -1, erule disjE)
paulson@13508
   508
apply (frule Crypt_prom, simp, simp)
paulson@13508
   509
apply (rotate_tac -1, erule disjE)
paulson@13508
   510
apply (rule_tac x=C in exI)
paulson@13508
   511
apply (rule_tac x="prom B ofr Aa r I (cons M L) J C" in exI, blast)
paulson@13508
   512
apply (subgoal_tac "cons M L:parts (spies evsp)")
paulson@13508
   513
apply (drule_tac G="{cons M L}" and H="spies evsp" in parts_trans, blast, blast)
paulson@13508
   514
apply (drule Says_imp_spies, rotate_tac -1, drule parts.Inj)
paulson@13508
   515
apply (drule parts.Snd, drule parts.Snd, drule parts.Snd)
paulson@13508
   516
by auto
paulson@13508
   517
paulson@13508
   518
lemma Crypt_Hash_imp_sign: "[| evs:p2; A ~:bad |] ==>
paulson@13508
   519
Crypt (priK A) (Hash X):parts (spies evs)
paulson@13508
   520
--> (EX B Y. Says A B Y:set evs & sign A X:parts {Y})"
paulson@13508
   521
apply (erule p2.induct)
paulson@13508
   522
(* Nil *)
paulson@13508
   523
apply simp
paulson@13508
   524
(* Fake *)
paulson@13508
   525
apply clarsimp
paulson@13508
   526
apply (drule_tac P="%G. Crypt (priK A) (Hash X):G" in parts_insert_substD)
paulson@13508
   527
apply simp
paulson@13508
   528
apply (erule disjE)
paulson@13508
   529
apply (drule_tac K="priK A" in Crypt_synth, simp+, blast, blast)
paulson@13508
   530
(* Request *)
paulson@13508
   531
apply (simp add: req_def, clarify)
paulson@13508
   532
apply (drule_tac P="%G. Crypt (priK A) (Hash X):G" in parts_insert_substD)
paulson@13508
   533
apply simp
paulson@13508
   534
apply (erule disjE)
paulson@13508
   535
apply (frule Crypt_reqm, simp+)
paulson@13508
   536
apply (rule_tac x=B in exI, rule_tac x="reqm Aa r n I B" in exI)
paulson@13508
   537
apply (simp add: reqm_def sign_def anchor_def no_Crypt_in_agl)
paulson@13508
   538
apply (simp add: chain_def sign_def, blast)
paulson@13508
   539
(* Propose *)
paulson@13508
   540
apply (simp add: pro_def, clarify)
paulson@13508
   541
apply (drule_tac P="%G. Crypt (priK A) (Hash X):G" in parts_insert_substD)
paulson@13508
   542
apply simp
paulson@13508
   543
apply (rotate_tac -1, erule disjE)
paulson@13508
   544
apply (simp add: prom_def sign_def no_Crypt_in_agl no_Crypt_in_appdel)
paulson@13508
   545
apply (simp add: chain_def sign_def)
paulson@13508
   546
apply (rotate_tac -1, erule disjE)
paulson@13508
   547
apply (rule_tac x=C in exI)
paulson@13508
   548
apply (rule_tac x="prom B ofr Aa r I (cons M L) J C" in exI)
paulson@13508
   549
apply (simp add: prom_def chain_def sign_def)
paulson@13508
   550
apply (erule impE) 
paulson@13508
   551
apply (blast dest: get_ML parts_sub) 
paulson@13508
   552
apply (blast del: MPair_parts)+
paulson@13508
   553
done
paulson@13508
   554
paulson@13508
   555
lemma sign_safeness: "[| evs:p2; A ~:bad |] ==> sign A X:parts (spies evs)
paulson@13508
   556
--> (EX B Y. Says A B Y:set evs & sign A X:parts {Y})"
paulson@13508
   557
apply (clarify, simp add: sign_def, frule parts.Snd)
paulson@13508
   558
apply (blast dest: Crypt_Hash_imp_sign [unfolded sign_def])
paulson@13508
   559
done
paulson@13508
   560
paulson@13508
   561
end