src/HOL/Auth/Guard/Guard_NS_Public.thy
author wenzelm
Wed Sep 14 23:14:57 2005 +0200 (2005-09-14)
changeset 17394 a8c9ed3f9818
child 20768 1d478c2d621f
permissions -rw-r--r--
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm@17394
     1
(******************************************************************************
wenzelm@17394
     2
incorporating Lowe's fix (inclusion of B's identity in round 2)
wenzelm@17394
     3
wenzelm@17394
     4
date: march 2002
wenzelm@17394
     5
author: Frederic Blanqui
wenzelm@17394
     6
email: blanqui@lri.fr
wenzelm@17394
     7
webpage: http://www.lri.fr/~blanqui/
wenzelm@17394
     8
wenzelm@17394
     9
University of Cambridge, Computer Laboratory
wenzelm@17394
    10
William Gates Building, JJ Thomson Avenue
wenzelm@17394
    11
Cambridge CB3 0FD, United Kingdom
wenzelm@17394
    12
******************************************************************************)
wenzelm@17394
    13
wenzelm@17394
    14
header{*Needham-Schroeder-Lowe Public-Key Protocol*}
wenzelm@17394
    15
wenzelm@17394
    16
theory Guard_NS_Public imports Guard_Public begin
wenzelm@17394
    17
wenzelm@17394
    18
subsection{*messages used in the protocol*}
wenzelm@17394
    19
wenzelm@17394
    20
syntax ns1 :: "agent => agent => nat => event"
wenzelm@17394
    21
wenzelm@17394
    22
translations "ns1 A B NA" => "Says A B (Crypt (pubK B) {|Nonce NA, Agent A|})"
wenzelm@17394
    23
wenzelm@17394
    24
syntax ns1' :: "agent => agent => agent => nat => event"
wenzelm@17394
    25
wenzelm@17394
    26
translations "ns1' A' A B NA"
wenzelm@17394
    27
=> "Says A' B (Crypt (pubK B) {|Nonce NA, Agent A|})"
wenzelm@17394
    28
wenzelm@17394
    29
syntax ns2 :: "agent => agent => nat => nat => event"
wenzelm@17394
    30
wenzelm@17394
    31
translations "ns2 B A NA NB"
wenzelm@17394
    32
=> "Says B A (Crypt (pubK A) {|Nonce NA, Nonce NB, Agent B|})"
wenzelm@17394
    33
wenzelm@17394
    34
syntax ns2' :: "agent => agent => agent => nat => nat => event"
wenzelm@17394
    35
wenzelm@17394
    36
translations "ns2' B' B A NA NB"
wenzelm@17394
    37
=> "Says B' A (Crypt (pubK A) {|Nonce NA, Nonce NB, Agent B|})"
wenzelm@17394
    38
wenzelm@17394
    39
syntax ns3 :: "agent => agent => nat => event"
wenzelm@17394
    40
wenzelm@17394
    41
translations "ns3 A B NB" => "Says A B (Crypt (pubK B) (Nonce NB))"
wenzelm@17394
    42
wenzelm@17394
    43
subsection{*definition of the protocol*}
wenzelm@17394
    44
wenzelm@17394
    45
consts nsp :: "event list set"
wenzelm@17394
    46
wenzelm@17394
    47
inductive nsp
wenzelm@17394
    48
intros
wenzelm@17394
    49
wenzelm@17394
    50
Nil: "[]:nsp"
wenzelm@17394
    51
wenzelm@17394
    52
Fake: "[| evs:nsp; X:synth (analz (spies evs)) |] ==> Says Spy B X # evs : nsp"
wenzelm@17394
    53
wenzelm@17394
    54
NS1: "[| evs1:nsp; Nonce NA ~:used evs1 |] ==> ns1 A B NA # evs1 : nsp"
wenzelm@17394
    55
wenzelm@17394
    56
NS2: "[| evs2:nsp; Nonce NB ~:used evs2; ns1' A' A B NA:set evs2 |] ==>
wenzelm@17394
    57
ns2 B A NA NB # evs2:nsp"
wenzelm@17394
    58
wenzelm@17394
    59
NS3: "[| evs3:nsp; ns1 A B NA:set evs3; ns2' B' B A NA NB:set evs3 |] ==>
wenzelm@17394
    60
ns3 A B NB # evs3:nsp"
wenzelm@17394
    61
wenzelm@17394
    62
subsection{*declarations for tactics*}
wenzelm@17394
    63
wenzelm@17394
    64
declare knows_Spy_partsEs [elim]
wenzelm@17394
    65
declare Fake_parts_insert [THEN subsetD, dest]
wenzelm@17394
    66
declare initState.simps [simp del]
wenzelm@17394
    67
wenzelm@17394
    68
subsection{*general properties of nsp*}
wenzelm@17394
    69
wenzelm@17394
    70
lemma nsp_has_no_Gets: "evs:nsp ==> ALL A X. Gets A X ~:set evs"
wenzelm@17394
    71
by (erule nsp.induct, auto)
wenzelm@17394
    72
wenzelm@17394
    73
lemma nsp_is_Gets_correct [iff]: "Gets_correct nsp"
wenzelm@17394
    74
by (auto simp: Gets_correct_def dest: nsp_has_no_Gets)
wenzelm@17394
    75
wenzelm@17394
    76
lemma nsp_is_one_step [iff]: "one_step nsp"
wenzelm@17394
    77
by (unfold one_step_def, clarify, ind_cases "ev#evs:nsp", auto)
wenzelm@17394
    78
wenzelm@17394
    79
lemma nsp_has_only_Says' [rule_format]: "evs:nsp ==>
wenzelm@17394
    80
ev:set evs --> (EX A B X. ev=Says A B X)"
wenzelm@17394
    81
by (erule nsp.induct, auto)
wenzelm@17394
    82
wenzelm@17394
    83
lemma nsp_has_only_Says [iff]: "has_only_Says nsp"
wenzelm@17394
    84
by (auto simp: has_only_Says_def dest: nsp_has_only_Says')
wenzelm@17394
    85
wenzelm@17394
    86
lemma nsp_is_regular [iff]: "regular nsp"
wenzelm@17394
    87
apply (simp only: regular_def, clarify)
wenzelm@17394
    88
by (erule nsp.induct, auto simp: initState.simps knows.simps)
wenzelm@17394
    89
wenzelm@17394
    90
subsection{*nonce are used only once*}
wenzelm@17394
    91
wenzelm@17394
    92
lemma NA_is_uniq [rule_format]: "evs:nsp ==>
wenzelm@17394
    93
Crypt (pubK B) {|Nonce NA, Agent A|}:parts (spies evs)
wenzelm@17394
    94
--> Crypt (pubK B') {|Nonce NA, Agent A'|}:parts (spies evs)
wenzelm@17394
    95
--> Nonce NA ~:analz (spies evs) --> A=A' & B=B'"
wenzelm@17394
    96
apply (erule nsp.induct, simp_all)
wenzelm@17394
    97
by (blast intro: analz_insertI)+
wenzelm@17394
    98
wenzelm@17394
    99
lemma no_Nonce_NS1_NS2 [rule_format]: "evs:nsp ==>
wenzelm@17394
   100
Crypt (pubK B') {|Nonce NA', Nonce NA, Agent A'|}:parts (spies evs)
wenzelm@17394
   101
--> Crypt (pubK B) {|Nonce NA, Agent A|}:parts (spies evs)
wenzelm@17394
   102
--> Nonce NA:analz (spies evs)"
wenzelm@17394
   103
apply (erule nsp.induct, simp_all)
wenzelm@17394
   104
by (blast intro: analz_insertI)+
wenzelm@17394
   105
wenzelm@17394
   106
lemma no_Nonce_NS1_NS2' [rule_format]:
wenzelm@17394
   107
"[| Crypt (pubK B') {|Nonce NA', Nonce NA, Agent A'|}:parts (spies evs);
wenzelm@17394
   108
Crypt (pubK B) {|Nonce NA, Agent A|}:parts (spies evs); evs:nsp |]
wenzelm@17394
   109
==> Nonce NA:analz (spies evs)"
wenzelm@17394
   110
by (rule no_Nonce_NS1_NS2, auto)
wenzelm@17394
   111
 
wenzelm@17394
   112
lemma NB_is_uniq [rule_format]: "evs:nsp ==>
wenzelm@17394
   113
Crypt (pubK A) {|Nonce NA, Nonce NB, Agent B|}:parts (spies evs)
wenzelm@17394
   114
--> Crypt (pubK A') {|Nonce NA', Nonce NB, Agent B'|}:parts (spies evs)
wenzelm@17394
   115
--> Nonce NB ~:analz (spies evs) --> A=A' & B=B' & NA=NA'"
wenzelm@17394
   116
apply (erule nsp.induct, simp_all)
wenzelm@17394
   117
by (blast intro: analz_insertI)+
wenzelm@17394
   118
wenzelm@17394
   119
subsection{*guardedness of NA*}
wenzelm@17394
   120
wenzelm@17394
   121
lemma ns1_imp_Guard [rule_format]: "[| evs:nsp; A ~:bad; B ~:bad |] ==>
wenzelm@17394
   122
ns1 A B NA:set evs --> Guard NA {priK A,priK B} (spies evs)"
wenzelm@17394
   123
apply (erule nsp.induct)
wenzelm@17394
   124
(* Nil *)
wenzelm@17394
   125
apply simp_all
wenzelm@17394
   126
(* Fake *)
wenzelm@17394
   127
apply safe
wenzelm@17394
   128
apply (erule in_synth_Guard, erule Guard_analz, simp)
wenzelm@17394
   129
(* NS1 *)
wenzelm@17394
   130
apply blast
wenzelm@17394
   131
apply blast
wenzelm@17394
   132
apply blast
wenzelm@17394
   133
apply (drule Nonce_neq, simp+, rule No_Nonce, simp)
wenzelm@17394
   134
(* NS2 *)
wenzelm@17394
   135
apply (frule_tac A=A in Nonce_neq, simp+)
wenzelm@17394
   136
apply (case_tac "NAa=NA")
wenzelm@17394
   137
apply (drule Guard_Nonce_analz, simp+)
wenzelm@17394
   138
apply (drule Says_imp_knows_Spy)+
wenzelm@17394
   139
apply (drule_tac B=B and A'=Aa in NA_is_uniq, auto)
wenzelm@17394
   140
(* NS3 *)
wenzelm@17394
   141
apply (case_tac "NB=NA", clarify)
wenzelm@17394
   142
apply (drule Guard_Nonce_analz, simp+)
wenzelm@17394
   143
apply (drule Says_imp_knows_Spy)+
wenzelm@17394
   144
by (drule no_Nonce_NS1_NS2, auto)
wenzelm@17394
   145
wenzelm@17394
   146
subsection{*guardedness of NB*}
wenzelm@17394
   147
wenzelm@17394
   148
lemma ns2_imp_Guard [rule_format]: "[| evs:nsp; A ~:bad; B ~:bad |] ==>
wenzelm@17394
   149
ns2 B A NA NB:set evs --> Guard NB {priK A,priK B} (spies evs)" 
wenzelm@17394
   150
apply (erule nsp.induct)
wenzelm@17394
   151
(* Nil *)
wenzelm@17394
   152
apply simp_all
wenzelm@17394
   153
(* Fake *)
wenzelm@17394
   154
apply safe
wenzelm@17394
   155
apply (erule in_synth_Guard, erule Guard_analz, simp)
wenzelm@17394
   156
(* NS1 *)
wenzelm@17394
   157
apply (frule Nonce_neq, simp+, blast, rule No_Nonce, simp)
wenzelm@17394
   158
(* NS2 *)
wenzelm@17394
   159
apply blast
wenzelm@17394
   160
apply blast
wenzelm@17394
   161
apply blast
wenzelm@17394
   162
apply (frule_tac A=B and n=NB in Nonce_neq, simp+)
wenzelm@17394
   163
apply (case_tac "NAa=NB")
wenzelm@17394
   164
apply (drule Guard_Nonce_analz, simp+)
wenzelm@17394
   165
apply (drule Says_imp_knows_Spy)+
wenzelm@17394
   166
apply (drule no_Nonce_NS1_NS2, auto)
wenzelm@17394
   167
(* NS3 *)
wenzelm@17394
   168
apply (case_tac "NBa=NB", clarify)
wenzelm@17394
   169
apply (drule Guard_Nonce_analz, simp+)
wenzelm@17394
   170
apply (drule Says_imp_knows_Spy)+
wenzelm@17394
   171
by (drule_tac A=Aa and A'=A in NB_is_uniq, auto)
wenzelm@17394
   172
wenzelm@17394
   173
subsection{*Agents' Authentication*}
wenzelm@17394
   174
wenzelm@17394
   175
lemma B_trusts_NS1: "[| evs:nsp; A ~:bad; B ~:bad |] ==>
wenzelm@17394
   176
Crypt (pubK B) {|Nonce NA, Agent A|}:parts (spies evs)
wenzelm@17394
   177
--> Nonce NA ~:analz (spies evs) --> ns1 A B NA:set evs"
wenzelm@17394
   178
apply (erule nsp.induct, simp_all)
wenzelm@17394
   179
by (blast intro: analz_insertI)+
wenzelm@17394
   180
wenzelm@17394
   181
lemma A_trusts_NS2: "[| evs:nsp; A ~:bad; B ~:bad |] ==> ns1 A B NA:set evs
wenzelm@17394
   182
--> Crypt (pubK A) {|Nonce NA, Nonce NB, Agent B|}:parts (spies evs)
wenzelm@17394
   183
--> ns2 B A NA NB:set evs"
wenzelm@17394
   184
apply (erule nsp.induct, simp_all, safe)
wenzelm@17394
   185
apply (frule_tac B=B in ns1_imp_Guard, simp+)
wenzelm@17394
   186
apply (drule Guard_Nonce_analz, simp+, blast)
wenzelm@17394
   187
apply (frule_tac B=B in ns1_imp_Guard, simp+)
wenzelm@17394
   188
apply (drule Guard_Nonce_analz, simp+, blast)
wenzelm@17394
   189
apply (frule_tac B=B in ns1_imp_Guard, simp+)
wenzelm@17394
   190
by (drule Guard_Nonce_analz, simp+, blast+)
wenzelm@17394
   191
wenzelm@17394
   192
lemma B_trusts_NS3: "[| evs:nsp; A ~:bad; B ~:bad |] ==> ns2 B A NA NB:set evs
wenzelm@17394
   193
--> Crypt (pubK B) (Nonce NB):parts (spies evs) --> ns3 A B NB:set evs"
wenzelm@17394
   194
apply (erule nsp.induct, simp_all, safe)
wenzelm@17394
   195
apply (frule_tac B=B in ns2_imp_Guard, simp+)
wenzelm@17394
   196
apply (drule Guard_Nonce_analz, simp+, blast)
wenzelm@17394
   197
apply (frule_tac B=B in ns2_imp_Guard, simp+)
wenzelm@17394
   198
apply (drule Guard_Nonce_analz, simp+, blast)
wenzelm@17394
   199
apply (frule_tac B=B in ns2_imp_Guard, simp+)
wenzelm@17394
   200
apply (drule Guard_Nonce_analz, simp+, blast, blast)
wenzelm@17394
   201
apply (frule_tac B=B in ns2_imp_Guard, simp+)
wenzelm@17394
   202
by (drule Guard_Nonce_analz, auto dest: Says_imp_knows_Spy NB_is_uniq)
wenzelm@17394
   203
wenzelm@17394
   204
end