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