src/HOL/Auth/Guard/Guard_Yahalom.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/Guard_Yahalom.thy
wenzelm@41775
     2
    Author:     Frederic Blanqui, University of Cambridge Computer Laboratory
wenzelm@41775
     3
    Copyright   2002  University of Cambridge
wenzelm@41775
     4
*)
wenzelm@17394
     5
wenzelm@58889
     6
section{*Yahalom Protocol*}
wenzelm@17394
     7
paulson@39216
     8
theory Guard_Yahalom imports "../Shared" Guard_Shared begin
wenzelm@17394
     9
wenzelm@17394
    10
subsection{*messages used in the protocol*}
wenzelm@17394
    11
wenzelm@20768
    12
abbreviation (input)
wenzelm@21404
    13
  ya1 :: "agent => agent => nat => event" where
wenzelm@20768
    14
  "ya1 A B NA == Says A B {|Agent A, Nonce NA|}"
wenzelm@17394
    15
wenzelm@21404
    16
abbreviation (input)
wenzelm@21404
    17
  ya1' :: "agent => agent => agent => nat => event" where
wenzelm@20768
    18
  "ya1' A' A B NA == Says A' B {|Agent A, Nonce NA|}"
wenzelm@17394
    19
wenzelm@21404
    20
abbreviation (input)
wenzelm@21404
    21
  ya2 :: "agent => agent => nat => nat => event" where
wenzelm@20768
    22
  "ya2 A B NA NB == Says B Server {|Agent B, Ciph B {|Agent A, Nonce NA, Nonce NB|}|}"
wenzelm@17394
    23
wenzelm@21404
    24
abbreviation (input)
wenzelm@21404
    25
  ya2' :: "agent => agent => agent => nat => nat => event" where
wenzelm@20768
    26
  "ya2' B' A B NA NB == Says B' Server {|Agent B, Ciph B {|Agent A, Nonce NA, Nonce NB|}|}"
wenzelm@17394
    27
wenzelm@21404
    28
abbreviation (input)
wenzelm@21404
    29
  ya3 :: "agent => agent => nat => nat => key => event" where
wenzelm@20768
    30
  "ya3 A B NA NB K ==
wenzelm@20768
    31
    Says Server A {|Ciph A {|Agent B, Key K, Nonce NA, Nonce NB|},
wenzelm@17394
    32
                    Ciph B {|Agent A, Key K|}|}"
wenzelm@17394
    33
wenzelm@21404
    34
abbreviation (input)
wenzelm@21404
    35
  ya3':: "agent => msg => agent => agent => nat => nat => key => event" where
wenzelm@20768
    36
  "ya3' S Y A B NA NB K ==
wenzelm@20768
    37
    Says S A {|Ciph A {|Agent B, Key K, Nonce NA, Nonce NB|}, Y|}"
wenzelm@17394
    38
wenzelm@21404
    39
abbreviation (input)
wenzelm@21404
    40
  ya4 :: "agent => agent => nat => nat => msg => event" where
wenzelm@20768
    41
  "ya4 A B K NB Y == Says A B {|Y, Crypt K (Nonce NB)|}"
wenzelm@17394
    42
wenzelm@21404
    43
abbreviation (input)
wenzelm@21404
    44
  ya4' :: "agent => agent => nat => nat => msg => event" where
wenzelm@20768
    45
  "ya4' A' B K NB Y == Says A' B {|Y, Crypt K (Nonce NB)|}"
wenzelm@17394
    46
wenzelm@17394
    47
wenzelm@17394
    48
subsection{*definition of the protocol*}
wenzelm@17394
    49
berghofe@23746
    50
inductive_set ya :: "event list set"
berghofe@23746
    51
where
wenzelm@17394
    52
berghofe@23746
    53
  Nil: "[]:ya"
wenzelm@17394
    54
berghofe@23746
    55
| Fake: "[| evs:ya; X:synth (analz (spies evs)) |] ==> Says Spy B X # evs:ya"
wenzelm@17394
    56
berghofe@23746
    57
| YA1: "[| evs1:ya; Nonce NA ~:used evs1 |] ==> ya1 A B NA # evs1:ya"
wenzelm@17394
    58
berghofe@23746
    59
| YA2: "[| evs2:ya; ya1' A' A B NA:set evs2; Nonce NB ~:used evs2 |]
berghofe@23746
    60
  ==> ya2 A B NA NB # evs2:ya"
wenzelm@17394
    61
berghofe@23746
    62
| YA3: "[| evs3:ya; ya2' B' A B NA NB:set evs3; Key K ~:used evs3 |]
berghofe@23746
    63
  ==> ya3 A B NA NB K # evs3:ya"
wenzelm@17394
    64
berghofe@23746
    65
| YA4: "[| evs4:ya; ya1 A B NA:set evs4; ya3' S Y A B NA NB K:set evs4 |]
berghofe@23746
    66
  ==> ya4 A B K NB Y # evs4:ya"
wenzelm@17394
    67
wenzelm@17394
    68
subsection{*declarations for tactics*}
wenzelm@17394
    69
wenzelm@17394
    70
declare knows_Spy_partsEs [elim]
wenzelm@17394
    71
declare Fake_parts_insert [THEN subsetD, dest]
wenzelm@17394
    72
declare initState.simps [simp del]
wenzelm@17394
    73
wenzelm@17394
    74
subsection{*general properties of ya*}
wenzelm@17394
    75
wenzelm@17394
    76
lemma ya_has_no_Gets: "evs:ya ==> ALL A X. Gets A X ~:set evs"
wenzelm@17394
    77
by (erule ya.induct, auto)
wenzelm@17394
    78
wenzelm@17394
    79
lemma ya_is_Gets_correct [iff]: "Gets_correct ya"
wenzelm@17394
    80
by (auto simp: Gets_correct_def dest: ya_has_no_Gets)
wenzelm@17394
    81
wenzelm@17394
    82
lemma ya_is_one_step [iff]: "one_step ya"
berghofe@23746
    83
by (unfold one_step_def, clarify, ind_cases "ev#evs:ya" for ev evs, auto)
wenzelm@17394
    84
wenzelm@17394
    85
lemma ya_has_only_Says' [rule_format]: "evs:ya ==>
wenzelm@17394
    86
ev:set evs --> (EX A B X. ev=Says A B X)"
wenzelm@17394
    87
by (erule ya.induct, auto)
wenzelm@17394
    88
wenzelm@17394
    89
lemma ya_has_only_Says [iff]: "has_only_Says ya"
wenzelm@17394
    90
by (auto simp: has_only_Says_def dest: ya_has_only_Says')
wenzelm@17394
    91
wenzelm@17394
    92
lemma ya_is_regular [iff]: "regular ya"
wenzelm@17394
    93
apply (simp only: regular_def, clarify)
wenzelm@17394
    94
apply (erule ya.induct, simp_all add: initState.simps knows.simps)
wenzelm@17394
    95
by (auto dest: parts_sub)
wenzelm@17394
    96
wenzelm@17394
    97
subsection{*guardedness of KAB*}
wenzelm@17394
    98
wenzelm@17394
    99
lemma Guard_KAB [rule_format]: "[| evs:ya; A ~:bad; B ~:bad |] ==>
wenzelm@17394
   100
ya3 A B NA NB K:set evs --> GuardK K {shrK A,shrK B} (spies evs)" 
wenzelm@17394
   101
apply (erule ya.induct)
wenzelm@17394
   102
(* Nil *)
wenzelm@17394
   103
apply simp_all
wenzelm@17394
   104
(* Fake *)
wenzelm@17394
   105
apply (clarify, erule in_synth_GuardK, erule GuardK_analz, simp)
wenzelm@17394
   106
(* YA1 *)
wenzelm@17394
   107
(* YA2 *)
wenzelm@17394
   108
apply safe
wenzelm@17394
   109
apply (blast dest: Says_imp_spies)
wenzelm@17394
   110
(* YA3 *)
wenzelm@17394
   111
apply blast
wenzelm@17394
   112
apply (drule_tac A=Server in Key_neq, simp+, rule No_Key, simp)
wenzelm@17394
   113
apply (drule_tac A=Server in Key_neq, simp+, rule No_Key, simp)
wenzelm@17394
   114
(* YA4 *)
wenzelm@17394
   115
apply (blast dest: Says_imp_spies in_GuardK_kparts)
wenzelm@17394
   116
by blast
wenzelm@17394
   117
wenzelm@17394
   118
subsection{*session keys are not symmetric keys*}
wenzelm@17394
   119
wenzelm@17394
   120
lemma KAB_isnt_shrK [rule_format]: "evs:ya ==>
wenzelm@17394
   121
ya3 A B NA NB K:set evs --> K ~:range shrK"
wenzelm@17394
   122
by (erule ya.induct, auto)
wenzelm@17394
   123
wenzelm@17394
   124
lemma ya3_shrK: "evs:ya ==> ya3 A B NA NB (shrK C) ~:set evs"
wenzelm@17394
   125
by (blast dest: KAB_isnt_shrK)
wenzelm@17394
   126
wenzelm@17394
   127
subsection{*ya2' implies ya1'*}
wenzelm@17394
   128
wenzelm@17394
   129
lemma ya2'_parts_imp_ya1'_parts [rule_format]:
wenzelm@17394
   130
     "[| evs:ya; B ~:bad |] ==>
wenzelm@17394
   131
      Ciph B {|Agent A, Nonce NA, Nonce NB|}:parts (spies evs) -->
wenzelm@17394
   132
      {|Agent A, Nonce NA|}:spies evs"
wenzelm@17394
   133
by (erule ya.induct, auto dest: Says_imp_spies intro: parts_parts)
wenzelm@17394
   134
wenzelm@17394
   135
lemma ya2'_imp_ya1'_parts: "[| ya2' B' A B NA NB:set evs; evs:ya; B ~:bad |]
wenzelm@17394
   136
==> {|Agent A, Nonce NA|}:spies evs"
wenzelm@17394
   137
by (blast dest: Says_imp_spies ya2'_parts_imp_ya1'_parts)
wenzelm@17394
   138
wenzelm@17394
   139
subsection{*uniqueness of NB*}
wenzelm@17394
   140
wenzelm@17394
   141
lemma NB_is_uniq_in_ya2'_parts [rule_format]: "[| evs:ya; B ~:bad; B' ~:bad |] ==>
wenzelm@17394
   142
Ciph B {|Agent A, Nonce NA, Nonce NB|}:parts (spies evs) -->
wenzelm@17394
   143
Ciph B' {|Agent A', Nonce NA', Nonce NB|}:parts (spies evs) -->
wenzelm@17394
   144
A=A' & B=B' & NA=NA'"
wenzelm@17394
   145
apply (erule ya.induct, simp_all, clarify)
wenzelm@17394
   146
apply (drule Crypt_synth_insert, simp+)
wenzelm@17394
   147
apply (drule Crypt_synth_insert, simp+, safe)
wenzelm@17394
   148
apply (drule not_used_parts_false, simp+)+
wenzelm@17394
   149
by (drule Says_not_parts, simp+)+
wenzelm@17394
   150
wenzelm@17394
   151
lemma NB_is_uniq_in_ya2': "[| ya2' C A B NA NB:set evs;
wenzelm@17394
   152
ya2' C' A' B' NA' NB:set evs; evs:ya; B ~:bad; B' ~:bad |]
wenzelm@17394
   153
==> A=A' & B=B' & NA=NA'"
wenzelm@17394
   154
by (drule NB_is_uniq_in_ya2'_parts, auto dest: Says_imp_spies)
wenzelm@17394
   155
wenzelm@17394
   156
subsection{*ya3' implies ya2'*}
wenzelm@17394
   157
wenzelm@17394
   158
lemma ya3'_parts_imp_ya2'_parts [rule_format]: "[| evs:ya; A ~:bad |] ==>
wenzelm@17394
   159
Ciph A {|Agent B, Key K, Nonce NA, Nonce NB|}:parts (spies evs)
wenzelm@17394
   160
--> Ciph B {|Agent A, Nonce NA, Nonce NB|}:parts (spies evs)"
wenzelm@17394
   161
apply (erule ya.induct, simp_all)
wenzelm@17394
   162
apply (clarify, drule Crypt_synth_insert, simp+)
wenzelm@17394
   163
apply (blast intro: parts_sub, blast)
wenzelm@17394
   164
by (auto dest: Says_imp_spies parts_parts)
wenzelm@17394
   165
wenzelm@17394
   166
lemma ya3'_parts_imp_ya2' [rule_format]: "[| evs:ya; A ~:bad |] ==>
wenzelm@17394
   167
Ciph A {|Agent B, Key K, Nonce NA, Nonce NB|}:parts (spies evs)
wenzelm@17394
   168
--> (EX B'. ya2' B' A B NA NB:set evs)"
wenzelm@17394
   169
apply (erule ya.induct, simp_all, safe)
wenzelm@17394
   170
apply (drule Crypt_synth_insert, simp+)
wenzelm@17394
   171
apply (drule Crypt_synth_insert, simp+, blast)
wenzelm@17394
   172
apply blast
wenzelm@17394
   173
apply blast
wenzelm@17394
   174
by (auto dest: Says_imp_spies2 parts_parts)
wenzelm@17394
   175
wenzelm@17394
   176
lemma ya3'_imp_ya2': "[| ya3' S Y A B NA NB K:set evs; evs:ya; A ~:bad |]
wenzelm@17394
   177
==> (EX B'. ya2' B' A B NA NB:set evs)"
wenzelm@17394
   178
by (drule ya3'_parts_imp_ya2', auto dest: Says_imp_spies)
wenzelm@17394
   179
wenzelm@17394
   180
subsection{*ya3' implies ya3*}
wenzelm@17394
   181
wenzelm@17394
   182
lemma ya3'_parts_imp_ya3 [rule_format]: "[| evs:ya; A ~:bad |] ==>
wenzelm@17394
   183
Ciph A {|Agent B, Key K, Nonce NA, Nonce NB|}:parts(spies evs)
wenzelm@17394
   184
--> ya3 A B NA NB K:set evs"
wenzelm@17394
   185
apply (erule ya.induct, simp_all, safe)
wenzelm@17394
   186
apply (drule Crypt_synth_insert, simp+)
wenzelm@17394
   187
by (blast dest: Says_imp_spies2 parts_parts)
wenzelm@17394
   188
wenzelm@17394
   189
lemma ya3'_imp_ya3: "[| ya3' S Y A B NA NB K:set evs; evs:ya; A ~:bad |]
wenzelm@17394
   190
==> ya3 A B NA NB K:set evs"
wenzelm@17394
   191
by (blast dest: Says_imp_spies ya3'_parts_imp_ya3)
wenzelm@17394
   192
wenzelm@17394
   193
subsection{*guardedness of NB*}
wenzelm@17394
   194
haftmann@35416
   195
definition ya_keys :: "agent => agent => nat => nat => event list => key set" where
wenzelm@17394
   196
"ya_keys A B NA NB evs == {shrK A,shrK B} Un {K. ya3 A B NA NB K:set evs}"
wenzelm@17394
   197
wenzelm@17394
   198
lemma Guard_NB [rule_format]: "[| evs:ya; A ~:bad; B ~:bad |] ==>
wenzelm@17394
   199
ya2 A B NA NB:set evs --> Guard NB (ya_keys A B NA NB evs) (spies evs)"
wenzelm@17394
   200
apply (erule ya.induct)
wenzelm@17394
   201
(* Nil *)
wenzelm@17394
   202
apply (simp_all add: ya_keys_def)
wenzelm@17394
   203
(* Fake *)
wenzelm@17394
   204
apply safe
wenzelm@17394
   205
apply (erule in_synth_Guard, erule Guard_analz, simp, clarify)
wenzelm@17394
   206
apply (frule_tac B=B in Guard_KAB, simp+)
wenzelm@17394
   207
apply (drule_tac p=ya in GuardK_Key_analz, simp+)
wenzelm@17394
   208
apply (blast dest: KAB_isnt_shrK, simp)
wenzelm@17394
   209
(* YA1 *)
wenzelm@17394
   210
apply (drule_tac n=NB in Nonce_neq, simp+, rule No_Nonce, simp)
wenzelm@17394
   211
(* YA2 *)
wenzelm@17394
   212
apply blast
wenzelm@17394
   213
apply (drule Says_imp_spies)
wenzelm@17394
   214
apply (drule_tac n=NB in Nonce_neq, simp+)
wenzelm@17394
   215
apply (drule_tac n'=NAa in in_Guard_kparts_neq, simp+)
wenzelm@17394
   216
apply (rule No_Nonce, simp)
wenzelm@17394
   217
(* YA3 *)
wenzelm@17394
   218
apply (rule Guard_extand, simp, blast)
wenzelm@17394
   219
apply (case_tac "NAa=NB", clarify)
wenzelm@17394
   220
apply (frule Says_imp_spies)
nipkow@56073
   221
apply (frule in_Guard_kparts_Crypt, simp+)
wenzelm@17394
   222
apply (frule_tac A=A and B=B and NA=NA and NB=NB and C=Ba in ya3_shrK, simp)
wenzelm@17394
   223
apply (drule ya2'_imp_ya1'_parts, simp, blast, blast)
wenzelm@17394
   224
apply (case_tac "NBa=NB", clarify)
wenzelm@17394
   225
apply (frule Says_imp_spies)
nipkow@56073
   226
apply (frule in_Guard_kparts_Crypt, simp+)
wenzelm@17394
   227
apply (frule_tac A=A and B=B and NA=NA and NB=NB and C=Ba in ya3_shrK, simp)
wenzelm@17394
   228
apply (drule NB_is_uniq_in_ya2', simp+, blast, simp+)
wenzelm@17394
   229
apply (simp add: No_Nonce, blast)
wenzelm@17394
   230
(* YA4 *)
wenzelm@17394
   231
apply (blast dest: Says_imp_spies)
wenzelm@17394
   232
apply (case_tac "NBa=NB", clarify)
wenzelm@17394
   233
apply (frule_tac A=S in Says_imp_spies)
wenzelm@17394
   234
apply (frule in_Guard_kparts_Crypt, simp+)
wenzelm@17394
   235
apply (blast dest: Says_imp_spies)
wenzelm@17394
   236
apply (case_tac "NBa=NB", clarify)
wenzelm@17394
   237
apply (frule_tac A=S in Says_imp_spies)
wenzelm@17394
   238
apply (frule in_Guard_kparts_Crypt, simp+, blast, simp+)
wenzelm@17394
   239
apply (frule_tac A=A and B=B and NA=NA and NB=NB and C=Aa in ya3_shrK, simp)
wenzelm@17394
   240
apply (frule ya3'_imp_ya2', simp+, blast, clarify)
wenzelm@17394
   241
apply (frule_tac A=B' in Says_imp_spies)
nipkow@56073
   242
apply (rotate_tac -1, frule in_Guard_kparts_Crypt, simp+)
wenzelm@17394
   243
apply (frule_tac A=A and B=B and NA=NA and NB=NB and C=Ba in ya3_shrK, simp)
wenzelm@17394
   244
apply (drule NB_is_uniq_in_ya2', simp+, blast, clarify)
wenzelm@17394
   245
apply (drule ya3'_imp_ya3, simp+)
wenzelm@17394
   246
apply (simp add: Guard_Nonce)
wenzelm@17394
   247
apply (simp add: No_Nonce)
wenzelm@17394
   248
done
wenzelm@17394
   249
wenzelm@17394
   250
end