src/HOL/Auth/Guard/Proto.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/Proto.thy
wenzelm@41775
     2
    Author:     Frederic Blanqui, University of Cambridge Computer Laboratory
wenzelm@41775
     3
    Copyright   2002  University of Cambridge
wenzelm@41775
     4
*)
paulson@13508
     5
wenzelm@58889
     6
section{*Other Protocol-Independent Results*}
paulson@13508
     7
haftmann@16417
     8
theory Proto imports Guard_Public begin
paulson@13508
     9
paulson@13508
    10
subsection{*protocols*}
paulson@13508
    11
wenzelm@41774
    12
type_synonym rule = "event set * event"
paulson@13508
    13
wenzelm@20768
    14
abbreviation
wenzelm@21404
    15
  msg' :: "rule => msg" where
wenzelm@20768
    16
  "msg' R == msg (snd R)"
paulson@13508
    17
wenzelm@41774
    18
type_synonym proto = "rule set"
paulson@13508
    19
haftmann@35416
    20
definition wdef :: "proto => bool" where
paulson@13508
    21
"wdef p == ALL R k. R:p --> Number k:parts {msg' R}
paulson@13508
    22
--> Number k:parts (msg`(fst R))"
paulson@13508
    23
paulson@13508
    24
subsection{*substitutions*}
paulson@13508
    25
paulson@13508
    26
record subs =
paulson@13508
    27
  agent   :: "agent => agent"
paulson@13508
    28
  nonce :: "nat => nat"
paulson@13508
    29
  nb    :: "nat => msg"
paulson@13508
    30
  key   :: "key => key"
paulson@13508
    31
haftmann@35416
    32
primrec apm :: "subs => msg => msg" where
haftmann@35416
    33
  "apm s (Agent A) = Agent (agent s A)"
haftmann@35416
    34
| "apm s (Nonce n) = Nonce (nonce s n)"
haftmann@35416
    35
| "apm s (Number n) = nb s n"
haftmann@35416
    36
| "apm s (Key K) = Key (key s K)"
haftmann@35416
    37
| "apm s (Hash X) = Hash (apm s X)"
haftmann@35416
    38
| "apm s (Crypt K X) = (
paulson@13508
    39
if (EX A. K = pubK A) then Crypt (pubK (agent s (agt K))) (apm s X)
paulson@13508
    40
else if (EX A. K = priK A) then Crypt (priK (agent s (agt K))) (apm s X)
paulson@13508
    41
else Crypt (key s K) (apm s X))"
haftmann@35416
    42
| "apm s {|X,Y|} = {|apm s X, apm s Y|}"
paulson@13508
    43
paulson@13508
    44
lemma apm_parts: "X:parts {Y} ==> apm s X:parts {apm s Y}"
paulson@13508
    45
apply (erule parts.induct, simp_all, blast)
paulson@13508
    46
apply (erule parts.Fst)
paulson@13508
    47
apply (erule parts.Snd)
paulson@13508
    48
by (erule parts.Body)+
paulson@13508
    49
paulson@13508
    50
lemma Nonce_apm [rule_format]: "Nonce n:parts {apm s X} ==>
paulson@13508
    51
(ALL k. Number k:parts {X} --> Nonce n ~:parts {nb s k}) -->
paulson@13508
    52
(EX k. Nonce k:parts {X} & nonce s k = n)"
paulson@13508
    53
by (induct X, simp_all, blast)
paulson@13508
    54
paulson@13508
    55
lemma wdef_Nonce: "[| Nonce n:parts {apm s X}; R:p; msg' R = X; wdef p;
paulson@13508
    56
Nonce n ~:parts (apm s `(msg `(fst R))) |] ==>
paulson@13508
    57
(EX k. Nonce k:parts {X} & nonce s k = n)"
paulson@13508
    58
apply (erule Nonce_apm, unfold wdef_def)
haftmann@56681
    59
apply (drule_tac x=R in spec, drule_tac x=k in spec, clarsimp simp: image_eq_UN)
paulson@13508
    60
apply (drule_tac x=x in bspec, simp)
paulson@13508
    61
apply (drule_tac Y="msg x" and s=s in apm_parts, simp)
paulson@13508
    62
by (blast dest: parts_parts)
paulson@13508
    63
haftmann@35416
    64
primrec ap :: "subs => event => event" where
haftmann@35416
    65
  "ap s (Says A B X) = Says (agent s A) (agent s B) (apm s X)"
haftmann@35416
    66
| "ap s (Gets A X) = Gets (agent s A) (apm s X)"
haftmann@35416
    67
| "ap s (Notes A X) = Notes (agent s A) (apm s X)"
paulson@13508
    68
wenzelm@20768
    69
abbreviation
wenzelm@21404
    70
  ap' :: "subs => rule => event" where
wenzelm@20768
    71
  "ap' s R == ap s (snd R)"
paulson@13508
    72
wenzelm@21404
    73
abbreviation
wenzelm@21404
    74
  apm' :: "subs => rule => msg" where
wenzelm@20768
    75
  "apm' s R == apm s (msg' R)"
wenzelm@20768
    76
wenzelm@21404
    77
abbreviation
wenzelm@21404
    78
  priK' :: "subs => agent => key" where
wenzelm@20768
    79
  "priK' s A == priK (agent s A)"
wenzelm@20768
    80
wenzelm@21404
    81
abbreviation
wenzelm@21404
    82
  pubK' :: "subs => agent => key" where
wenzelm@20768
    83
  "pubK' s A == pubK (agent s A)"
paulson@13508
    84
paulson@13508
    85
subsection{*nonces generated by a rule*}
paulson@13508
    86
haftmann@35416
    87
definition newn :: "rule => nat set" where
paulson@13508
    88
"newn R == {n. Nonce n:parts {msg (snd R)} & Nonce n ~:parts (msg`(fst R))}"
paulson@13508
    89
paulson@13508
    90
lemma newn_parts: "n:newn R ==> Nonce (nonce s n):parts {apm' s R}"
paulson@13508
    91
by (auto simp: newn_def dest: apm_parts)
paulson@13508
    92
paulson@13508
    93
subsection{*traces generated by a protocol*}
paulson@13508
    94
haftmann@35416
    95
definition ok :: "event list => rule => subs => bool" where
paulson@13508
    96
"ok evs R s == ((ALL x. x:fst R --> ap s x:set evs)
paulson@13508
    97
& (ALL n. n:newn R --> Nonce (nonce s n) ~:used evs))"
paulson@13508
    98
berghofe@23746
    99
inductive_set
berghofe@23746
   100
  tr :: "proto => event list set"
berghofe@23746
   101
  for p :: proto
berghofe@23746
   102
where
paulson@13508
   103
berghofe@23746
   104
  Nil [intro]: "[]:tr p"
paulson@13508
   105
berghofe@23746
   106
| Fake [intro]: "[| evsf:tr p; X:synth (analz (spies evsf)) |]
berghofe@23746
   107
  ==> Says Spy B X # evsf:tr p"
paulson@13508
   108
berghofe@23746
   109
| Proto [intro]: "[| evs:tr p; R:p; ok evs R s |] ==> ap' s R # evs:tr p"
paulson@13508
   110
paulson@13508
   111
subsection{*general properties*}
paulson@13508
   112
paulson@13508
   113
lemma one_step_tr [iff]: "one_step (tr p)"
paulson@13508
   114
apply (unfold one_step_def, clarify)
berghofe@23746
   115
by (ind_cases "ev # evs:tr p" for ev evs, auto)
paulson@13508
   116
haftmann@35416
   117
definition has_only_Says' :: "proto => bool" where
paulson@13508
   118
"has_only_Says' p == ALL R. R:p --> is_Says (snd R)"
paulson@13508
   119
paulson@13508
   120
lemma has_only_Says'D: "[| R:p; has_only_Says' p |]
paulson@13508
   121
==> (EX A B X. snd R = Says A B X)"
paulson@13508
   122
by (unfold has_only_Says'_def is_Says_def, blast)
paulson@13508
   123
paulson@13508
   124
lemma has_only_Says_tr [simp]: "has_only_Says' p ==> has_only_Says (tr p)"
paulson@13508
   125
apply (unfold has_only_Says_def)
paulson@13508
   126
apply (rule allI, rule allI, rule impI)
paulson@13508
   127
apply (erule tr.induct)
paulson@13508
   128
apply (auto simp: has_only_Says'_def ok_def)
paulson@13508
   129
by (drule_tac x=a in spec, auto simp: is_Says_def)
paulson@13508
   130
paulson@13508
   131
lemma has_only_Says'_in_trD: "[| has_only_Says' p; list @ ev # evs1 \<in> tr p |]
paulson@13508
   132
==> (EX A B X. ev = Says A B X)"
paulson@13508
   133
by (drule has_only_Says_tr, auto)
paulson@13508
   134
paulson@13508
   135
lemma ok_not_used: "[| Nonce n ~:used evs; ok evs R s;
paulson@13508
   136
ALL x. x:fst R --> is_Says x |] ==> Nonce n ~:parts (apm s `(msg `(fst R)))"
haftmann@56681
   137
apply (unfold ok_def, clarsimp simp: image_eq_UN)
paulson@13508
   138
apply (drule_tac x=x in spec, drule_tac x=x in spec)
paulson@13508
   139
by (auto simp: is_Says_def dest: Says_imp_spies not_used_not_spied parts_parts)
paulson@13508
   140
paulson@13508
   141
lemma ok_is_Says: "[| evs' @ ev # evs:tr p; ok evs R s; has_only_Says' p;
paulson@13508
   142
R:p; x:fst R |] ==> is_Says x"
paulson@13508
   143
apply (unfold ok_def is_Says_def, clarify)
paulson@13508
   144
apply (drule_tac x=x in spec, simp)
paulson@13508
   145
apply (subgoal_tac "one_step (tr p)")
paulson@13508
   146
apply (drule trunc, simp, drule one_step_Cons, simp)
paulson@13508
   147
apply (drule has_only_SaysD, simp+)
paulson@13508
   148
by (clarify, case_tac x, auto)
paulson@13508
   149
paulson@13508
   150
subsection{*types*}
paulson@13508
   151
wenzelm@41774
   152
type_synonym keyfun = "rule => subs => nat => event list => key set"
paulson@13508
   153
wenzelm@41774
   154
type_synonym secfun = "rule => nat => subs => key set => msg"
paulson@13508
   155
paulson@13508
   156
subsection{*introduction of a fresh guarded nonce*}
paulson@13508
   157
haftmann@35416
   158
definition fresh :: "proto => rule => subs => nat => key set => event list
haftmann@35416
   159
=> bool" where
paulson@13508
   160
"fresh p R s n Ks evs == (EX evs1 evs2. evs = evs2 @ ap' s R # evs1
paulson@13508
   161
& Nonce n ~:used evs1 & R:p & ok evs1 R s & Nonce n:parts {apm' s R}
paulson@13508
   162
& apm' s R:guard n Ks)"
paulson@13508
   163
paulson@13508
   164
lemma freshD: "fresh p R s n Ks evs ==> (EX evs1 evs2.
paulson@13508
   165
evs = evs2 @ ap' s R # evs1 & Nonce n ~:used evs1 & R:p & ok evs1 R s
paulson@13508
   166
& Nonce n:parts {apm' s R} & apm' s R:guard n Ks)"
paulson@13508
   167
by (unfold fresh_def, blast)
paulson@13508
   168
paulson@13508
   169
lemma freshI [intro]: "[| Nonce n ~:used evs1; R:p; Nonce n:parts {apm' s R};
paulson@13508
   170
ok evs1 R s; apm' s R:guard n Ks |]
paulson@13508
   171
==> fresh p R s n Ks (list @ ap' s R # evs1)"
paulson@13508
   172
by (unfold fresh_def, blast)
paulson@13508
   173
paulson@13508
   174
lemma freshI': "[| Nonce n ~:used evs1; (l,r):p;
paulson@13508
   175
Nonce n:parts {apm s (msg r)}; ok evs1 (l,r) s; apm s (msg r):guard n Ks |]
paulson@13508
   176
==> fresh p (l,r) s n Ks (evs2 @ ap s r # evs1)"
paulson@13508
   177
by (drule freshI, simp+)
paulson@13508
   178
paulson@13508
   179
lemma fresh_used: "[| fresh p R' s' n Ks evs; has_only_Says' p |]
paulson@13508
   180
==> Nonce n:used evs"
paulson@13508
   181
apply (unfold fresh_def, clarify)
paulson@13508
   182
apply (drule has_only_Says'D)
paulson@13508
   183
by (auto intro: parts_used_app)
paulson@13508
   184
paulson@13508
   185
lemma fresh_newn: "[| evs' @ ap' s R # evs:tr p; wdef p; has_only_Says' p;
paulson@13508
   186
Nonce n ~:used evs; R:p; ok evs R s; Nonce n:parts {apm' s R} |]
paulson@13508
   187
==> EX k. k:newn R & nonce s k = n"
paulson@13508
   188
apply (drule wdef_Nonce, simp+)
paulson@13508
   189
apply (frule ok_not_used, simp+)
paulson@13508
   190
apply (clarify, erule ok_is_Says, simp+)
haftmann@56681
   191
apply (clarify, rule_tac x=k in exI, simp add: newn_def image_eq_UN)
paulson@13508
   192
apply (clarify, drule_tac Y="msg x" and s=s in apm_parts)
paulson@13508
   193
apply (drule ok_not_used, simp+)
haftmann@56681
   194
by (clarify, erule ok_is_Says, simp_all add: image_eq_UN)
paulson@13508
   195
paulson@13508
   196
lemma fresh_rule: "[| evs' @ ev # evs:tr p; wdef p; Nonce n ~:used evs;
paulson@13508
   197
Nonce n:parts {msg ev} |] ==> EX R s. R:p & ap' s R = ev"
paulson@13508
   198
apply (drule trunc, simp, ind_cases "ev # evs:tr p", simp)
paulson@13508
   199
by (drule_tac x=X in in_sub, drule parts_sub, simp, simp, blast+)
paulson@13508
   200
paulson@13508
   201
lemma fresh_ruleD: "[| fresh p R' s' n Ks evs; keys R' s' n evs <= Ks; wdef p;
paulson@13508
   202
has_only_Says' p; evs:tr p; ALL R k s. nonce s k = n --> Nonce n:used evs -->
paulson@13508
   203
R:p --> k:newn R --> Nonce n:parts {apm' s R} --> apm' s R:guard n Ks -->
paulson@13508
   204
apm' s R:parts (spies evs) --> keys R s n evs <= Ks --> P |] ==> P"
paulson@13508
   205
apply (frule fresh_used, simp)
paulson@13508
   206
apply (unfold fresh_def, clarify)
paulson@13508
   207
apply (drule_tac x=R' in spec)
paulson@13508
   208
apply (drule fresh_newn, simp+, clarify)
paulson@13508
   209
apply (drule_tac x=k in spec)
paulson@13508
   210
apply (drule_tac x=s' in spec)
paulson@13508
   211
apply (subgoal_tac "apm' s' R':parts (spies (evs2 @ ap' s' R' # evs1))")
paulson@13508
   212
apply (case_tac R', drule has_only_Says'D, simp, clarsimp)
paulson@13508
   213
apply (case_tac R', drule has_only_Says'D, simp, clarsimp)
paulson@13508
   214
apply (rule_tac Y="apm s' X" in parts_parts, blast)
paulson@13508
   215
by (rule parts.Inj, rule Says_imp_spies, simp, blast)
paulson@13508
   216
paulson@13508
   217
subsection{*safe keys*}
paulson@13508
   218
haftmann@35416
   219
definition safe :: "key set => msg set => bool" where
paulson@13508
   220
"safe Ks G == ALL K. K:Ks --> Key K ~:analz G"
paulson@13508
   221
paulson@13508
   222
lemma safeD [dest]: "[| safe Ks G; K:Ks |] ==> Key K ~:analz G"
paulson@13508
   223
by (unfold safe_def, blast)
paulson@13508
   224
paulson@13508
   225
lemma safe_insert: "safe Ks (insert X G) ==> safe Ks G"
paulson@13508
   226
by (unfold safe_def, blast)
paulson@13508
   227
paulson@13508
   228
lemma Guard_safe: "[| Guard n Ks G; safe Ks G |] ==> Nonce n ~:analz G"
paulson@13508
   229
by (blast dest: Guard_invKey)
paulson@13508
   230
paulson@13508
   231
subsection{*guardedness preservation*}
paulson@13508
   232
haftmann@35416
   233
definition preserv :: "proto => keyfun => nat => key set => bool" where
paulson@13508
   234
"preserv p keys n Ks == (ALL evs R' s' R s. evs:tr p -->
paulson@13508
   235
Guard n Ks (spies evs) --> safe Ks (spies evs) --> fresh p R' s' n Ks evs -->
paulson@13508
   236
keys R' s' n evs <= Ks --> R:p --> ok evs R s --> apm' s R:guard n Ks)"
paulson@13508
   237
paulson@13508
   238
lemma preservD: "[| preserv p keys n Ks; evs:tr p; Guard n Ks (spies evs);
paulson@13508
   239
safe Ks (spies evs); fresh p R' s' n Ks evs; R:p; ok evs R s;
paulson@13508
   240
keys R' s' n evs <= Ks |] ==> apm' s R:guard n Ks"
paulson@13508
   241
by (unfold preserv_def, blast)
paulson@13508
   242
paulson@13508
   243
lemma preservD': "[| preserv p keys n Ks; evs:tr p; Guard n Ks (spies evs);
paulson@13508
   244
safe Ks (spies evs); fresh p R' s' n Ks evs; (l,Says A B X):p;
paulson@13508
   245
ok evs (l,Says A B X) s; keys R' s' n evs <= Ks |] ==> apm s X:guard n Ks"
paulson@13508
   246
by (drule preservD, simp+)
paulson@13508
   247
paulson@13508
   248
subsection{*monotonic keyfun*}
paulson@13508
   249
haftmann@35416
   250
definition monoton :: "proto => keyfun => bool" where
paulson@13508
   251
"monoton p keys == ALL R' s' n ev evs. ev # evs:tr p -->
paulson@13508
   252
keys R' s' n evs <= keys R' s' n (ev # evs)"
paulson@13508
   253
paulson@13508
   254
lemma monotonD [dest]: "[| keys R' s' n (ev # evs) <= Ks; monoton p keys;
paulson@13508
   255
ev # evs:tr p |] ==> keys R' s' n evs <= Ks"
paulson@13508
   256
by (unfold monoton_def, blast)
paulson@13508
   257
paulson@13508
   258
subsection{*guardedness theorem*}
paulson@13508
   259
paulson@13508
   260
lemma Guard_tr [rule_format]: "[| evs:tr p; has_only_Says' p;
paulson@13508
   261
preserv p keys n Ks; monoton p keys; Guard n Ks (initState Spy) |] ==>
paulson@13508
   262
safe Ks (spies evs) --> fresh p R' s' n Ks evs --> keys R' s' n evs <= Ks -->
paulson@13508
   263
Guard n Ks (spies evs)"
paulson@13508
   264
apply (erule tr.induct)
paulson@13508
   265
(* Nil *)
paulson@13508
   266
apply simp
paulson@13508
   267
(* Fake *)
paulson@13508
   268
apply (clarify, drule freshD, clarsimp)
paulson@13508
   269
apply (case_tac evs2)
paulson@13508
   270
(* evs2 = [] *)
paulson@13508
   271
apply (frule has_only_Says'D, simp)
paulson@13508
   272
apply (clarsimp, blast)
paulson@13508
   273
(* evs2 = aa # list *)
paulson@13508
   274
apply (clarsimp, rule conjI)
paulson@13508
   275
apply (blast dest: safe_insert)
paulson@13508
   276
(* X:guard n Ks *)
paulson@13508
   277
apply (rule in_synth_Guard, simp, rule Guard_analz)
paulson@13508
   278
apply (blast dest: safe_insert)
paulson@13508
   279
apply (drule safe_insert, simp add: safe_def)
paulson@13508
   280
(* Proto *)
paulson@13508
   281
apply (clarify, drule freshD, clarify)
paulson@13508
   282
apply (case_tac evs2)
paulson@13508
   283
(* evs2 = [] *)
paulson@13508
   284
apply (frule has_only_Says'D, simp)
paulson@13508
   285
apply (frule_tac R=R' in has_only_Says'D, simp)
paulson@13508
   286
apply (case_tac R', clarsimp, blast)
paulson@13508
   287
(* evs2 = ab # list *)
paulson@13508
   288
apply (frule has_only_Says'D, simp)
paulson@13508
   289
apply (clarsimp, rule conjI)
paulson@13508
   290
apply (drule Proto, simp+, blast dest: safe_insert)
paulson@13508
   291
(* apm s X:guard n Ks *)
paulson@13508
   292
apply (frule Proto, simp+)
paulson@13508
   293
apply (erule preservD', simp+)
paulson@13508
   294
apply (blast dest: safe_insert)
paulson@13508
   295
apply (blast dest: safe_insert)
paulson@13508
   296
by (blast, simp, simp, blast)
paulson@13508
   297
paulson@13508
   298
subsection{*useful properties for guardedness*}
paulson@13508
   299
paulson@13508
   300
lemma newn_neq_used: "[| Nonce n:used evs; ok evs R s; k:newn R |]
paulson@13508
   301
==> n ~= nonce s k"
paulson@13508
   302
by (auto simp: ok_def)
paulson@13508
   303
paulson@13508
   304
lemma ok_Guard: "[| ok evs R s; Guard n Ks (spies evs); x:fst R; is_Says x |]
paulson@13508
   305
==> apm s (msg x):parts (spies evs) & apm s (msg x):guard n Ks"
paulson@13508
   306
apply (unfold ok_def is_Says_def, clarify)
paulson@13508
   307
apply (drule_tac x="Says A B X" in spec, simp)
paulson@13508
   308
by (drule Says_imp_spies, auto intro: parts_parts)
paulson@13508
   309
paulson@13508
   310
lemma ok_parts_not_new: "[| Y:parts (spies evs); Nonce (nonce s n):parts {Y};
paulson@13508
   311
ok evs R s |] ==> n ~:newn R"
paulson@13508
   312
by (auto simp: ok_def dest: not_used_not_spied parts_parts)
paulson@13508
   313
paulson@13508
   314
subsection{*unicity*}
paulson@13508
   315
haftmann@35416
   316
definition uniq :: "proto => secfun => bool" where
paulson@13508
   317
"uniq p secret == ALL evs R R' n n' Ks s s'. R:p --> R':p -->
paulson@13508
   318
n:newn R --> n':newn R' --> nonce s n = nonce s' n' -->
paulson@13508
   319
Nonce (nonce s n):parts {apm' s R} --> Nonce (nonce s n):parts {apm' s' R'} -->
paulson@13508
   320
apm' s R:guard (nonce s n) Ks --> apm' s' R':guard (nonce s n) Ks -->
paulson@13508
   321
evs:tr p --> Nonce (nonce s n) ~:analz (spies evs) -->
paulson@13508
   322
secret R n s Ks:parts (spies evs) --> secret R' n' s' Ks:parts (spies evs) -->
paulson@13508
   323
secret R n s Ks = secret R' n' s' Ks"
paulson@13508
   324
paulson@13508
   325
lemma uniqD: "[| uniq p secret; evs: tr p; R:p; R':p; n:newn R; n':newn R';
paulson@13508
   326
nonce s n = nonce s' n'; Nonce (nonce s n) ~:analz (spies evs);
paulson@13508
   327
Nonce (nonce s n):parts {apm' s R}; Nonce (nonce s n):parts {apm' s' R'};
paulson@13508
   328
secret R n s Ks:parts (spies evs); secret R' n' s' Ks:parts (spies evs);
paulson@13508
   329
apm' s R:guard (nonce s n) Ks; apm' s' R':guard (nonce s n) Ks |] ==>
paulson@13508
   330
secret R n s Ks = secret R' n' s' Ks"
paulson@13508
   331
by (unfold uniq_def, blast)
paulson@13508
   332
haftmann@35416
   333
definition ord :: "proto => (rule => rule => bool) => bool" where
haftmann@22426
   334
"ord p inff == ALL R R'. R:p --> R':p --> ~ inff R R' --> inff R' R"
paulson@13508
   335
haftmann@22426
   336
lemma ordD: "[| ord p inff; ~ inff R R'; R:p; R':p |] ==> inff R' R"
paulson@13508
   337
by (unfold ord_def, blast)
paulson@13508
   338
haftmann@35416
   339
definition uniq' :: "proto => (rule => rule => bool) => secfun => bool" where
haftmann@22426
   340
"uniq' p inff secret == ALL evs R R' n n' Ks s s'. R:p --> R':p -->
haftmann@22426
   341
inff R R' --> n:newn R --> n':newn R' --> nonce s n = nonce s' n' -->
paulson@13508
   342
Nonce (nonce s n):parts {apm' s R} --> Nonce (nonce s n):parts {apm' s' R'} -->
paulson@13508
   343
apm' s R:guard (nonce s n) Ks --> apm' s' R':guard (nonce s n) Ks -->
paulson@13508
   344
evs:tr p --> Nonce (nonce s n) ~:analz (spies evs) -->
paulson@13508
   345
secret R n s Ks:parts (spies evs) --> secret R' n' s' Ks:parts (spies evs) -->
paulson@13508
   346
secret R n s Ks = secret R' n' s' Ks"
paulson@13508
   347
haftmann@22426
   348
lemma uniq'D: "[| uniq' p inff secret; evs: tr p; inff R R'; R:p; R':p; n:newn R;
paulson@13508
   349
n':newn R'; nonce s n = nonce s' n'; Nonce (nonce s n) ~:analz (spies evs);
paulson@13508
   350
Nonce (nonce s n):parts {apm' s R}; Nonce (nonce s n):parts {apm' s' R'};
paulson@13508
   351
secret R n s Ks:parts (spies evs); secret R' n' s' Ks:parts (spies evs);
paulson@13508
   352
apm' s R:guard (nonce s n) Ks; apm' s' R':guard (nonce s n) Ks |] ==>
paulson@13508
   353
secret R n s Ks = secret R' n' s' Ks"
paulson@13508
   354
by (unfold uniq'_def, blast)
paulson@13508
   355
haftmann@22426
   356
lemma uniq'_imp_uniq: "[| uniq' p inff secret; ord p inff |] ==> uniq p secret"
paulson@13508
   357
apply (unfold uniq_def)
paulson@13508
   358
apply (rule allI)+
haftmann@22426
   359
apply (case_tac "inff R R'")
paulson@13508
   360
apply (blast dest: uniq'D)
paulson@13508
   361
by (auto dest: ordD uniq'D intro: sym)
paulson@13508
   362
paulson@13508
   363
subsection{*Needham-Schroeder-Lowe*}
paulson@13508
   364
haftmann@35416
   365
definition a :: agent where "a == Friend 0"
haftmann@35416
   366
definition b :: agent where "b == Friend 1"
haftmann@35416
   367
definition a' :: agent where "a' == Friend 2"
haftmann@35416
   368
definition b' :: agent where "b' == Friend 3"
haftmann@35416
   369
definition Na :: nat where "Na == 0"
haftmann@35416
   370
definition Nb :: nat where "Nb == 1"
paulson@13508
   371
wenzelm@20768
   372
abbreviation
wenzelm@21404
   373
  ns1 :: rule where
wenzelm@20768
   374
  "ns1 == ({}, Says a b (Crypt (pubK b) {|Nonce Na, Agent a|}))"
paulson@13508
   375
wenzelm@21404
   376
abbreviation
wenzelm@21404
   377
  ns2 :: rule where
wenzelm@20768
   378
  "ns2 == ({Says a' b (Crypt (pubK b) {|Nonce Na, Agent a|})},
wenzelm@20768
   379
    Says b a (Crypt (pubK a) {|Nonce Na, Nonce Nb, Agent b|}))"
paulson@13508
   380
wenzelm@21404
   381
abbreviation
wenzelm@21404
   382
  ns3 :: rule where
wenzelm@20768
   383
  "ns3 == ({Says a b (Crypt (pubK b) {|Nonce Na, Agent a|}),
wenzelm@20768
   384
    Says b' a (Crypt (pubK a) {|Nonce Na, Nonce Nb, Agent b|})},
wenzelm@20768
   385
    Says a b (Crypt (pubK b) (Nonce Nb)))"
paulson@13508
   386
berghofe@23746
   387
inductive_set ns :: proto where
berghofe@23746
   388
  [iff]: "ns1:ns"
berghofe@23746
   389
| [iff]: "ns2:ns"
berghofe@23746
   390
| [iff]: "ns3:ns"
paulson@13508
   391
wenzelm@20768
   392
abbreviation (input)
wenzelm@21404
   393
  ns3a :: event where
wenzelm@20768
   394
  "ns3a == Says a b (Crypt (pubK b) {|Nonce Na, Agent a|})"
paulson@13508
   395
wenzelm@21404
   396
abbreviation (input)
wenzelm@21404
   397
  ns3b :: event where
wenzelm@20768
   398
  "ns3b == Says b' a (Crypt (pubK a) {|Nonce Na, Nonce Nb, Agent b|})"
paulson@13508
   399
haftmann@35416
   400
definition keys :: "keyfun" where
paulson@13508
   401
"keys R' s' n evs == {priK' s' a, priK' s' b}"
paulson@13508
   402
paulson@13508
   403
lemma "monoton ns keys"
paulson@13508
   404
by (simp add: keys_def monoton_def)
paulson@13508
   405
haftmann@35416
   406
definition secret :: "secfun" where
paulson@13508
   407
"secret R n s Ks ==
paulson@13508
   408
(if R=ns1 then apm s (Crypt (pubK b) {|Nonce Na, Agent a|})
paulson@13508
   409
else if R=ns2 then apm s (Crypt (pubK a) {|Nonce Na, Nonce Nb, Agent b|})
paulson@13508
   410
else Number 0)"
paulson@13508
   411
haftmann@35416
   412
definition inf :: "rule => rule => bool" where
paulson@13508
   413
"inf R R' == (R=ns1 | (R=ns2 & R'~=ns1) | (R=ns3 & R'=ns3))"
paulson@13508
   414
paulson@13508
   415
lemma inf_is_ord [iff]: "ord ns inf"
paulson@13508
   416
apply (unfold ord_def inf_def)
paulson@13508
   417
apply (rule allI)+
berghofe@23746
   418
apply (rule impI)
berghofe@23746
   419
apply (simp add: split_paired_all)
paulson@13508
   420
by (rule impI, erule ns.cases, simp_all)+
paulson@13508
   421
paulson@13508
   422
subsection{*general properties*}
paulson@13508
   423
paulson@13508
   424
lemma ns_has_only_Says' [iff]: "has_only_Says' ns"
paulson@13508
   425
apply (unfold has_only_Says'_def)
paulson@13508
   426
apply (rule allI, rule impI)
berghofe@23746
   427
apply (simp add: split_paired_all)
paulson@13508
   428
by (erule ns.cases, auto)
paulson@13508
   429
paulson@13508
   430
lemma newn_ns1 [iff]: "newn ns1 = {Na}"
paulson@13508
   431
by (simp add: newn_def)
paulson@13508
   432
paulson@13508
   433
lemma newn_ns2 [iff]: "newn ns2 = {Nb}"
paulson@13508
   434
by (auto simp: newn_def Na_def Nb_def)
paulson@13508
   435
paulson@13508
   436
lemma newn_ns3 [iff]: "newn ns3 = {}"
paulson@13508
   437
by (auto simp: newn_def)
paulson@13508
   438
paulson@13508
   439
lemma ns_wdef [iff]: "wdef ns"
paulson@13508
   440
by (auto simp: wdef_def elim: ns.cases)
paulson@13508
   441
paulson@13508
   442
subsection{*guardedness for NSL*}
paulson@13508
   443
paulson@13508
   444
lemma "uniq ns secret ==> preserv ns keys n Ks"
paulson@13508
   445
apply (unfold preserv_def)
paulson@13508
   446
apply (rule allI)+
paulson@13508
   447
apply (rule impI, rule impI, rule impI, rule impI, rule impI)
paulson@13508
   448
apply (erule fresh_ruleD, simp, simp, simp, simp)
paulson@13508
   449
apply (rule allI)+
paulson@13508
   450
apply (rule impI, rule impI, rule impI)
berghofe@23746
   451
apply (simp add: split_paired_all)
paulson@13508
   452
apply (erule ns.cases)
paulson@13508
   453
(* fresh with NS1 *)
paulson@13508
   454
apply (rule impI, rule impI, rule impI, rule impI, rule impI, rule impI)
paulson@13508
   455
apply (erule ns.cases)
paulson@13508
   456
(* NS1 *)
paulson@13508
   457
apply clarsimp
paulson@13508
   458
apply (frule newn_neq_used, simp, simp)
paulson@13508
   459
apply (rule No_Nonce, simp)
paulson@13508
   460
(* NS2 *)
paulson@13508
   461
apply clarsimp
paulson@13508
   462
apply (frule newn_neq_used, simp, simp)
paulson@13508
   463
apply (case_tac "nonce sa Na = nonce s Na")
paulson@13508
   464
apply (frule Guard_safe, simp)
paulson@13508
   465
apply (frule Crypt_guard_invKey, simp)
paulson@13508
   466
apply (frule ok_Guard, simp, simp, simp, clarsimp)
paulson@13508
   467
apply (frule_tac K="pubK' s b" in Crypt_guard_invKey, simp)
paulson@13508
   468
apply (frule_tac R=ns1 and R'=ns1 and Ks=Ks and s=sa and s'=s in uniqD, simp+)
paulson@13508
   469
apply (simp add: secret_def, simp add: secret_def, force, force)
paulson@13508
   470
apply (simp add: secret_def keys_def, blast)
paulson@13508
   471
apply (rule No_Nonce, simp)
paulson@13508
   472
(* NS3 *)
paulson@13508
   473
apply clarsimp
paulson@13508
   474
apply (case_tac "nonce sa Na = nonce s Nb")
paulson@13508
   475
apply (frule Guard_safe, simp)
paulson@13508
   476
apply (frule Crypt_guard_invKey, simp)
paulson@13508
   477
apply (frule_tac x=ns3b in ok_Guard, simp, simp, simp, clarsimp)
paulson@13508
   478
apply (frule_tac K="pubK' s a" in Crypt_guard_invKey, simp)
paulson@13508
   479
apply (frule_tac R=ns1 and R'=ns2 and Ks=Ks and s=sa and s'=s in uniqD, simp+)
paulson@13508
   480
apply (simp add: secret_def, simp add: secret_def, force, force)
paulson@13508
   481
apply (simp add: secret_def, rule No_Nonce, simp)
paulson@13508
   482
(* fresh with NS2 *)
paulson@13508
   483
apply (rule impI, rule impI, rule impI, rule impI, rule impI, rule impI)
paulson@13508
   484
apply (erule ns.cases)
paulson@13508
   485
(* NS1 *)
paulson@13508
   486
apply clarsimp
paulson@13508
   487
apply (frule newn_neq_used, simp, simp)
paulson@13508
   488
apply (rule No_Nonce, simp)
paulson@13508
   489
(* NS2 *)
paulson@13508
   490
apply clarsimp
paulson@13508
   491
apply (frule newn_neq_used, simp, simp)
paulson@13508
   492
apply (case_tac "nonce sa Nb = nonce s Na")
paulson@13508
   493
apply (frule Guard_safe, simp)
paulson@13508
   494
apply (frule Crypt_guard_invKey, simp)
paulson@13508
   495
apply (frule ok_Guard, simp, simp, simp, clarsimp)
paulson@13508
   496
apply (frule_tac K="pubK' s b" in Crypt_guard_invKey, simp)
paulson@13508
   497
apply (frule_tac R=ns2 and R'=ns1 and Ks=Ks and s=sa and s'=s in uniqD, simp+)
paulson@13508
   498
apply (simp add: secret_def, simp add: secret_def, force, force)
paulson@13508
   499
apply (simp add: secret_def, rule No_Nonce, simp)
paulson@13508
   500
(* NS3 *)
paulson@13508
   501
apply clarsimp
paulson@13508
   502
apply (case_tac "nonce sa Nb = nonce s Nb")
paulson@13508
   503
apply (frule Guard_safe, simp)
paulson@13508
   504
apply (frule Crypt_guard_invKey, simp)
paulson@13508
   505
apply (frule_tac x=ns3b in ok_Guard, simp, simp, simp, clarsimp)
paulson@13508
   506
apply (frule_tac K="pubK' s a" in Crypt_guard_invKey, simp)
paulson@13508
   507
apply (frule_tac R=ns2 and R'=ns2 and Ks=Ks and s=sa and s'=s in uniqD, simp+)
paulson@13508
   508
apply (simp add: secret_def, simp add: secret_def, force, force)
paulson@13508
   509
apply (simp add: secret_def keys_def, blast)
paulson@13508
   510
apply (rule No_Nonce, simp)
paulson@13508
   511
(* fresh with NS3 *)
paulson@13508
   512
by simp
paulson@13508
   513
paulson@13508
   514
subsection{*unicity for NSL*}
paulson@13508
   515
paulson@13508
   516
lemma "uniq' ns inf secret"
paulson@13508
   517
apply (unfold uniq'_def)
paulson@13508
   518
apply (rule allI)+
berghofe@23746
   519
apply (simp add: split_paired_all)
paulson@13508
   520
apply (rule impI, erule ns.cases)
paulson@13508
   521
(* R = ns1 *)
paulson@13508
   522
apply (rule impI, erule ns.cases)
paulson@13508
   523
(* R' = ns1 *)
paulson@13508
   524
apply (rule impI, rule impI, rule impI, rule impI)
paulson@13508
   525
apply (rule impI, rule impI, rule impI, rule impI)
paulson@13508
   526
apply (rule impI, erule tr.induct)
paulson@13508
   527
(* Nil *)
paulson@13508
   528
apply (simp add: secret_def)
paulson@13508
   529
(* Fake *)
paulson@13508
   530
apply (clarify, simp add: secret_def)
paulson@13508
   531
apply (drule notin_analz_insert)
paulson@13508
   532
apply (drule Crypt_insert_synth, simp, simp, simp)
paulson@13508
   533
apply (drule Crypt_insert_synth, simp, simp, simp, simp)
paulson@13508
   534
(* Proto *)
berghofe@23746
   535
apply (erule_tac P="ok evsa R sa" in rev_mp)
berghofe@23746
   536
apply (simp add: split_paired_all)
paulson@13508
   537
apply (erule ns.cases)
paulson@13508
   538
(* ns1 *)
paulson@13508
   539
apply (clarify, simp add: secret_def)
paulson@13508
   540
apply (erule disjE, erule disjE, clarsimp)
paulson@13508
   541
apply (drule ok_parts_not_new, simp, simp, simp)
paulson@13508
   542
apply (clarify, drule ok_parts_not_new, simp, simp, simp)
paulson@13508
   543
(* ns2 *)
paulson@13508
   544
apply (simp add: secret_def)
paulson@13508
   545
(* ns3 *)
paulson@13508
   546
apply (simp add: secret_def)
paulson@13508
   547
(* R' = ns2 *)
paulson@13508
   548
apply (rule impI, rule impI, rule impI, rule impI)
paulson@13508
   549
apply (rule impI, rule impI, rule impI, rule impI)
paulson@13508
   550
apply (rule impI, erule tr.induct)
paulson@13508
   551
(* Nil *)
paulson@13508
   552
apply (simp add: secret_def)
paulson@13508
   553
(* Fake *)
paulson@13508
   554
apply (clarify, simp add: secret_def)
paulson@13508
   555
apply (drule notin_analz_insert)
paulson@13508
   556
apply (drule Crypt_insert_synth, simp, simp, simp)
paulson@13508
   557
apply (drule_tac n="nonce s' Nb" in Crypt_insert_synth, simp, simp, simp, simp)
paulson@13508
   558
(* Proto *)
berghofe@23746
   559
apply (erule_tac P="ok evsa R sa" in rev_mp)
berghofe@23746
   560
apply (simp add: split_paired_all)
paulson@13508
   561
apply (erule ns.cases)
paulson@13508
   562
(* ns1 *)
paulson@13508
   563
apply (clarify, simp add: secret_def)
paulson@13508
   564
apply (drule_tac s=sa and n=Na in ok_parts_not_new, simp, simp, simp)
paulson@13508
   565
(* ns2 *)
paulson@13508
   566
apply (clarify, simp add: secret_def)
paulson@13508
   567
apply (drule_tac s=sa and n=Nb in ok_parts_not_new, simp, simp, simp)
paulson@13508
   568
(* ns3 *)
paulson@13508
   569
apply (simp add: secret_def)
paulson@13508
   570
(* R' = ns3 *)
paulson@13508
   571
apply simp
paulson@13508
   572
(* R = ns2 *)
paulson@13508
   573
apply (rule impI, erule ns.cases)
paulson@13508
   574
(* R' = ns1 *)
paulson@13508
   575
apply (simp only: inf_def, blast)
paulson@13508
   576
(* R' = ns2 *)
paulson@13508
   577
apply (rule impI, rule impI, rule impI, rule impI)
paulson@13508
   578
apply (rule impI, rule impI, rule impI, rule impI)
paulson@13508
   579
apply (rule impI, erule tr.induct)
paulson@13508
   580
(* Nil *)
paulson@13508
   581
apply (simp add: secret_def)
paulson@13508
   582
(* Fake *)
paulson@13508
   583
apply (clarify, simp add: secret_def)
paulson@13508
   584
apply (drule notin_analz_insert)
paulson@13508
   585
apply (drule_tac n="nonce s' Nb" in Crypt_insert_synth, simp, simp, simp)
paulson@13508
   586
apply (drule_tac n="nonce s' Nb" in Crypt_insert_synth, simp, simp, simp, simp)
paulson@13508
   587
(* Proto *)
berghofe@23746
   588
apply (erule_tac P="ok evsa R sa" in rev_mp)
berghofe@23746
   589
apply (simp add: split_paired_all)
paulson@13508
   590
apply (erule ns.cases)
paulson@13508
   591
(* ns1 *)
paulson@13508
   592
apply (simp add: secret_def)
paulson@13508
   593
(* ns2 *)
paulson@13508
   594
apply (clarify, simp add: secret_def)
paulson@13508
   595
apply (erule disjE, erule disjE, clarsimp, clarsimp)
paulson@13508
   596
apply (drule_tac s=sa and n=Nb in ok_parts_not_new, simp, simp, simp)
paulson@13508
   597
apply (erule disjE, clarsimp)
paulson@13508
   598
apply (drule_tac s=sa and n=Nb in ok_parts_not_new, simp, simp, simp)
paulson@13508
   599
by (simp_all add: secret_def)
paulson@13508
   600
paulson@13508
   601
end