src/HOL/UNITY/Simple/NSP_Bad.thy
author obua
Mon Apr 10 16:00:34 2006 +0200 (2006-04-10)
changeset 19404 9bf2cdc9e8e8
parent 18556 dc39832e9280
child 21588 cd0dc678a205
permissions -rw-r--r--
Moved stuff from Ring_and_Field to Matrix
paulson@11195
     1
(*  Title:      HOL/Auth/NSP_Bad
paulson@11195
     2
    ID:         $Id$
paulson@11195
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
paulson@11195
     4
    Copyright   1996  University of Cambridge
paulson@11195
     5
paulson@14203
     6
ML{*add_path "$ISABELLE_HOME/src/HOL/Auth"*}
paulson@11195
     7
paulson@11195
     8
Original file is ../Auth/NS_Public_Bad
paulson@11195
     9
*)
paulson@11195
    10
paulson@14203
    11
header{*Analyzing the Needham-Schroeder Public-Key Protocol in UNITY*}
paulson@14203
    12
paulson@18556
    13
theory NSP_Bad imports "../Auth/Public" "../UNITY_Main" begin
paulson@11195
    14
paulson@14203
    15
text{*This is the flawed version, vulnerable to Lowe's attack.
paulson@14203
    16
From page 260 of
paulson@14203
    17
  Burrows, Abadi and Needham.  A Logic of Authentication.
paulson@14203
    18
  Proc. Royal Soc. 426 (1989).
paulson@14203
    19
*}
paulson@14203
    20
paulson@14203
    21
types state = "event list"
paulson@11195
    22
paulson@11195
    23
constdefs
paulson@14203
    24
paulson@11195
    25
  (*The spy MAY say anything he CAN say.  We do not expect him to
paulson@11195
    26
    invent new nonces here, but he can also use NS1.  Common to
paulson@11195
    27
    all similar protocols.*)
paulson@11195
    28
  Fake :: "(state*state) set"
paulson@11195
    29
    "Fake == {(s,s').
paulson@14203
    30
	      \<exists>B X. s' = Says Spy B X # s
paulson@14203
    31
		    & X \<in> synth (analz (spies s))}"
paulson@14203
    32
paulson@11195
    33
  (*The numeric suffixes on A identify the rule*)
paulson@11195
    34
paulson@11195
    35
  (*Alice initiates a protocol run, sending a nonce to Bob*)
paulson@11195
    36
  NS1 :: "(state*state) set"
paulson@11195
    37
    "NS1 == {(s1,s').
paulson@14203
    38
	     \<exists>A1 B NA.
paulson@11195
    39
	         s' = Says A1 B (Crypt (pubK B) {|Nonce NA, Agent A1|}) # s1
paulson@14203
    40
	       & Nonce NA \<notin> used s1}"
paulson@14203
    41
paulson@11195
    42
  (*Bob responds to Alice's message with a further nonce*)
paulson@11195
    43
  NS2 :: "(state*state) set"
paulson@11195
    44
    "NS2 == {(s2,s').
paulson@14203
    45
	     \<exists>A' A2 B NA NB.
paulson@11195
    46
	         s' = Says B A2 (Crypt (pubK A2) {|Nonce NA, Nonce NB|}) # s2
paulson@14203
    47
               & Says A' B (Crypt (pubK B) {|Nonce NA, Agent A2|}) \<in> set s2
paulson@14203
    48
	       & Nonce NB \<notin> used s2}"
paulson@14203
    49
paulson@11195
    50
  (*Alice proves her existence by sending NB back to Bob.*)
paulson@11195
    51
  NS3 :: "(state*state) set"
paulson@11195
    52
    "NS3 == {(s3,s').
paulson@14203
    53
	     \<exists>A3 B' B NA NB.
paulson@11195
    54
	         s' = Says A3 B (Crypt (pubK B) (Nonce NB)) # s3
paulson@14203
    55
               & Says A3  B (Crypt (pubK B) {|Nonce NA, Agent A3|}) \<in> set s3
paulson@14203
    56
	       & Says B' A3 (Crypt (pubK A3) {|Nonce NA, Nonce NB|}) \<in> set s3}"
paulson@14203
    57
paulson@14203
    58
paulson@14203
    59
constdefs
paulson@14203
    60
  Nprg :: "state program"
paulson@14203
    61
    (*Initial trace is empty*)
paulson@14203
    62
    "Nprg == mk_total_program({[]}, {Fake, NS1, NS2, NS3}, UNIV)"
paulson@14203
    63
paulson@14203
    64
declare spies_partsEs [elim]
paulson@14203
    65
declare analz_into_parts [dest]
paulson@14203
    66
declare Fake_parts_insert_in_Un  [dest]
paulson@14203
    67
paulson@14203
    68
text{*For other theories, e.g. Mutex and Lift, using [iff] slows proofs down.
paulson@14203
    69
  Here, it facilitates re-use of the Auth proofs.*}
paulson@14203
    70
paulson@14203
    71
declare Fake_def [THEN def_act_simp, iff]
paulson@14203
    72
declare NS1_def [THEN def_act_simp, iff]
paulson@14203
    73
declare NS2_def [THEN def_act_simp, iff]
paulson@14203
    74
declare NS3_def [THEN def_act_simp, iff]
paulson@14203
    75
paulson@14203
    76
declare Nprg_def [THEN def_prg_Init, simp]
paulson@14203
    77
paulson@14203
    78
paulson@14203
    79
text{*A "possibility property": there are traces that reach the end.
paulson@14203
    80
  Replace by LEADSTO proof!*}
paulson@14203
    81
lemma "A \<noteq> B ==>
paulson@14203
    82
       \<exists>NB. \<exists>s \<in> reachable Nprg. Says A B (Crypt (pubK B) (Nonce NB)) \<in> set s"
paulson@14203
    83
apply (intro exI bexI)
paulson@14203
    84
apply (rule_tac [2] act = "totalize_act NS3" in reachable.Acts)
paulson@14203
    85
apply (rule_tac [3] act = "totalize_act NS2" in reachable.Acts)
paulson@14203
    86
apply (rule_tac [4] act = "totalize_act NS1" in reachable.Acts)
paulson@14203
    87
apply (rule_tac [5] reachable.Init)
paulson@14203
    88
apply (simp_all (no_asm_simp) add: Nprg_def totalize_act_def)
paulson@14203
    89
apply auto
paulson@14203
    90
done
paulson@14203
    91
paulson@14203
    92
paulson@14203
    93
subsection{*Inductive Proofs about @{term ns_public}*}
paulson@14203
    94
paulson@14203
    95
lemma ns_constrainsI:
paulson@14203
    96
     "(!!act s s'. [| act \<in> {Id, Fake, NS1, NS2, NS3};
paulson@14203
    97
                      (s,s') \<in> act;  s \<in> A |] ==> s' \<in> A')
paulson@14203
    98
      ==> Nprg \<in> A co A'"
paulson@14203
    99
apply (simp add: Nprg_def mk_total_program_def)
paulson@14203
   100
apply (rule constrainsI, auto)
paulson@14203
   101
done
paulson@14203
   102
paulson@14203
   103
paulson@14203
   104
text{*This ML code does the inductions directly.*}
paulson@14203
   105
ML{*
paulson@14203
   106
val ns_constrainsI = thm "ns_constrainsI";
paulson@14203
   107
paulson@14203
   108
fun ns_constrains_tac(cs,ss) i =
paulson@14203
   109
   SELECT_GOAL
paulson@14203
   110
      (EVERY [REPEAT (etac Always_ConstrainsI 1),
paulson@14203
   111
	      REPEAT (resolve_tac [StableI, stableI,
paulson@14203
   112
				   constrains_imp_Constrains] 1),
paulson@14203
   113
	      rtac ns_constrainsI 1,
paulson@14203
   114
	      full_simp_tac ss 1,
paulson@14203
   115
	      REPEAT (FIRSTGOAL (etac disjE)),
paulson@14203
   116
	      ALLGOALS (clarify_tac (cs delrules [impI,impCE])),
paulson@14203
   117
	      REPEAT (FIRSTGOAL analz_mono_contra_tac),
paulson@14203
   118
	      ALLGOALS (asm_simp_tac ss)]) i;
paulson@14203
   119
paulson@14203
   120
(*Tactic for proving secrecy theorems*)
paulson@14203
   121
fun ns_induct_tac(cs,ss) =
paulson@14203
   122
  (SELECT_GOAL o EVERY)
paulson@14203
   123
     [rtac AlwaysI 1,
paulson@14203
   124
      force_tac (cs,ss) 1,
paulson@14203
   125
      (*"reachable" gets in here*)
paulson@14203
   126
      rtac (Always_reachable RS Always_ConstrainsI RS StableI) 1,
paulson@14203
   127
      ns_constrains_tac(cs,ss) 1];
paulson@14203
   128
*}
paulson@14203
   129
paulson@14203
   130
method_setup ns_induct = {*
paulson@14203
   131
    Method.ctxt_args (fn ctxt =>
paulson@14203
   132
        Method.METHOD (fn facts =>
wenzelm@15032
   133
            ns_induct_tac (local_clasimpset_of ctxt) 1)) *}
paulson@14203
   134
    "for inductive reasoning about the Needham-Schroeder protocol"
paulson@14203
   135
paulson@14203
   136
text{*Converts invariants into statements about reachable states*}
paulson@14203
   137
lemmas Always_Collect_reachableD =
paulson@14203
   138
     Always_includes_reachable [THEN subsetD, THEN CollectD]
paulson@14203
   139
paulson@14203
   140
text{*Spy never sees another agent's private key! (unless it's bad at start)*}
paulson@14203
   141
lemma Spy_see_priK:
paulson@14203
   142
     "Nprg \<in> Always {s. (Key (priK A) \<in> parts (spies s)) = (A \<in> bad)}"
paulson@14203
   143
apply ns_induct
paulson@14203
   144
apply blast
paulson@14203
   145
done
paulson@14203
   146
declare Spy_see_priK [THEN Always_Collect_reachableD, simp]
paulson@14203
   147
paulson@14203
   148
lemma Spy_analz_priK:
paulson@14203
   149
     "Nprg \<in> Always {s. (Key (priK A) \<in> analz (spies s)) = (A \<in> bad)}"
paulson@14203
   150
by (rule Always_reachable [THEN Always_weaken], auto)
paulson@14203
   151
declare Spy_analz_priK [THEN Always_Collect_reachableD, simp]
paulson@14203
   152
paulson@14203
   153
paulson@14203
   154
subsection{*Authenticity properties obtained from NS2*}
paulson@14203
   155
paulson@14203
   156
text{*It is impossible to re-use a nonce in both NS1 and NS2 provided the
paulson@14203
   157
     nonce is secret.  (Honest users generate fresh nonces.)*}
paulson@14203
   158
lemma no_nonce_NS1_NS2:
paulson@14203
   159
 "Nprg
paulson@14203
   160
  \<in> Always {s. Crypt (pubK C) {|NA', Nonce NA|} \<in> parts (spies s) -->
paulson@14203
   161
                Crypt (pubK B) {|Nonce NA, Agent A|} \<in> parts (spies s) -->
paulson@14203
   162
                Nonce NA \<in> analz (spies s)}"
paulson@14203
   163
apply ns_induct
paulson@14203
   164
apply (blast intro: analz_insertI)+
paulson@14203
   165
done
paulson@14203
   166
paulson@14203
   167
text{*Adding it to the claset slows down proofs...*}
paulson@14203
   168
lemmas no_nonce_NS1_NS2_reachable =
paulson@14203
   169
       no_nonce_NS1_NS2 [THEN Always_Collect_reachableD, rule_format]
paulson@14203
   170
paulson@14203
   171
paulson@14203
   172
text{*Unicity for NS1: nonce NA identifies agents A and B*}
paulson@14203
   173
lemma unique_NA_lemma:
paulson@14203
   174
     "Nprg
paulson@14203
   175
  \<in> Always {s. Nonce NA \<notin> analz (spies s) -->
paulson@14203
   176
                Crypt(pubK B) {|Nonce NA, Agent A|} \<in> parts(spies s) -->
paulson@14203
   177
                Crypt(pubK B') {|Nonce NA, Agent A'|} \<in> parts(spies s) -->
paulson@14203
   178
                A=A' & B=B'}"
paulson@14203
   179
apply ns_induct
paulson@14203
   180
apply auto
paulson@14203
   181
txt{*Fake, NS1 are non-trivial*}
paulson@14203
   182
done
paulson@14203
   183
paulson@14203
   184
text{*Unicity for NS1: nonce NA identifies agents A and B*}
paulson@14203
   185
lemma unique_NA:
paulson@14203
   186
     "[| Crypt(pubK B)  {|Nonce NA, Agent A|} \<in> parts(spies s);
paulson@14203
   187
         Crypt(pubK B') {|Nonce NA, Agent A'|} \<in> parts(spies s);
paulson@14203
   188
         Nonce NA \<notin> analz (spies s);
paulson@14203
   189
         s \<in> reachable Nprg |]
paulson@14203
   190
      ==> A=A' & B=B'"
paulson@14203
   191
by (blast dest: unique_NA_lemma [THEN Always_Collect_reachableD])
paulson@14203
   192
paulson@14203
   193
paulson@14203
   194
text{*Secrecy: Spy does not see the nonce sent in msg NS1 if A and B are secure*}
paulson@14203
   195
lemma Spy_not_see_NA:
paulson@14203
   196
     "[| A \<notin> bad;  B \<notin> bad |]
paulson@14203
   197
  ==> Nprg \<in> Always
paulson@14203
   198
              {s. Says A B (Crypt(pubK B) {|Nonce NA, Agent A|}) \<in> set s
paulson@14203
   199
                  --> Nonce NA \<notin> analz (spies s)}"
paulson@14203
   200
apply ns_induct
paulson@14203
   201
txt{*NS3*}
paulson@14203
   202
prefer 4 apply (blast intro: no_nonce_NS1_NS2_reachable)
paulson@14203
   203
txt{*NS2*}
paulson@14203
   204
prefer 3 apply (blast dest: unique_NA)
paulson@14203
   205
txt{*NS1*}
paulson@14203
   206
prefer 2 apply blast
paulson@14203
   207
txt{*Fake*}
paulson@14203
   208
apply spy_analz
paulson@14203
   209
done
paulson@14203
   210
paulson@14203
   211
paulson@14203
   212
text{*Authentication for A: if she receives message 2 and has used NA
paulson@14203
   213
  to start a run, then B has sent message 2.*}
paulson@14203
   214
lemma A_trusts_NS2:
paulson@14203
   215
 "[| A \<notin> bad;  B \<notin> bad |]
paulson@14203
   216
  ==> Nprg \<in> Always
paulson@14203
   217
              {s. Says A B (Crypt(pubK B) {|Nonce NA, Agent A|}) \<in> set s &
paulson@14203
   218
                  Crypt(pubK A) {|Nonce NA, Nonce NB|} \<in> parts (knows Spy s)
paulson@14203
   219
         --> Says B A (Crypt(pubK A) {|Nonce NA, Nonce NB|}) \<in> set s}"
paulson@14203
   220
  (*insert an invariant for use in some of the subgoals*)
paulson@14203
   221
apply (insert Spy_not_see_NA [of A B NA], simp, ns_induct)
paulson@14203
   222
apply (auto dest: unique_NA)
paulson@14203
   223
done
paulson@14203
   224
paulson@14203
   225
paulson@14203
   226
text{*If the encrypted message appears then it originated with Alice in NS1*}
paulson@14203
   227
lemma B_trusts_NS1:
paulson@14203
   228
     "Nprg \<in> Always
paulson@14203
   229
              {s. Nonce NA \<notin> analz (spies s) -->
paulson@14203
   230
                  Crypt (pubK B) {|Nonce NA, Agent A|} \<in> parts (spies s)
paulson@14203
   231
         --> Says A B (Crypt (pubK B) {|Nonce NA, Agent A|}) \<in> set s}"
paulson@14203
   232
apply ns_induct
paulson@14203
   233
apply blast
paulson@14203
   234
done
paulson@14203
   235
paulson@14203
   236
paulson@14203
   237
subsection{*Authenticity properties obtained from NS2*}
paulson@14203
   238
paulson@14203
   239
text{*Unicity for NS2: nonce NB identifies nonce NA and agent A.
paulson@14203
   240
   Proof closely follows that of @{text unique_NA}.*}
paulson@14203
   241
lemma unique_NB_lemma:
paulson@14203
   242
 "Nprg
paulson@14203
   243
  \<in> Always {s. Nonce NB \<notin> analz (spies s)  -->
paulson@14203
   244
                Crypt (pubK A) {|Nonce NA, Nonce NB|} \<in> parts (spies s) -->
paulson@14203
   245
                Crypt(pubK A'){|Nonce NA', Nonce NB|} \<in> parts(spies s) -->
paulson@14203
   246
                A=A' & NA=NA'}"
paulson@14203
   247
apply ns_induct
paulson@14203
   248
apply auto
paulson@14203
   249
txt{*Fake, NS2 are non-trivial*}
paulson@14203
   250
done
paulson@14203
   251
paulson@14203
   252
lemma unique_NB:
paulson@14203
   253
     "[| Crypt(pubK A) {|Nonce NA, Nonce NB|} \<in> parts(spies s);
paulson@14203
   254
         Crypt(pubK A'){|Nonce NA', Nonce NB|} \<in> parts(spies s);
paulson@14203
   255
         Nonce NB \<notin> analz (spies s);
paulson@14203
   256
         s \<in> reachable Nprg |]
paulson@14203
   257
      ==> A=A' & NA=NA'"
paulson@14203
   258
apply (blast dest: unique_NB_lemma [THEN Always_Collect_reachableD])
paulson@14203
   259
done
paulson@14203
   260
paulson@14203
   261
paulson@14203
   262
text{*NB remains secret PROVIDED Alice never responds with round 3*}
paulson@14203
   263
lemma Spy_not_see_NB:
paulson@14203
   264
     "[| A \<notin> bad;  B \<notin> bad |]
paulson@14203
   265
  ==> Nprg \<in> Always
paulson@14203
   266
              {s. Says B A (Crypt (pubK A) {|Nonce NA, Nonce NB|}) \<in> set s &
paulson@14203
   267
                  (ALL C. Says A C (Crypt (pubK C) (Nonce NB)) \<notin> set s)
paulson@14203
   268
                  --> Nonce NB \<notin> analz (spies s)}"
paulson@14203
   269
apply ns_induct
paulson@14203
   270
apply (simp_all (no_asm_simp) add: all_conj_distrib)
paulson@14203
   271
txt{*NS3: because NB determines A*}
paulson@14203
   272
prefer 4 apply (blast dest: unique_NB)
paulson@14203
   273
txt{*NS2: by freshness and unicity of NB*}
paulson@14203
   274
prefer 3 apply (blast intro: no_nonce_NS1_NS2_reachable)
paulson@14203
   275
txt{*NS1: by freshness*}
paulson@14203
   276
prefer 2 apply blast
paulson@14203
   277
txt{*Fake*}
paulson@14203
   278
apply spy_analz
paulson@14203
   279
done
paulson@11195
   280
paulson@11195
   281
paulson@11195
   282
paulson@14203
   283
text{*Authentication for B: if he receives message 3 and has used NB
paulson@14203
   284
  in message 2, then A has sent message 3--to somebody....*}
paulson@14203
   285
lemma B_trusts_NS3:
paulson@14203
   286
     "[| A \<notin> bad;  B \<notin> bad |]
paulson@14203
   287
  ==> Nprg \<in> Always
paulson@14203
   288
              {s. Crypt (pubK B) (Nonce NB) \<in> parts (spies s) &
paulson@14203
   289
                  Says B A  (Crypt (pubK A) {|Nonce NA, Nonce NB|}) \<in> set s
paulson@14203
   290
                  --> (\<exists>C. Says A C (Crypt (pubK C) (Nonce NB)) \<in> set s)}"
paulson@14203
   291
  (*insert an invariant for use in some of the subgoals*)
paulson@14203
   292
apply (insert Spy_not_see_NB [of A B NA NB], simp, ns_induct)
paulson@14203
   293
apply (simp_all (no_asm_simp) add: ex_disj_distrib)
paulson@14203
   294
apply auto
paulson@14203
   295
txt{*NS3: because NB determines A. This use of @{text unique_NB} is robust.*}
paulson@14203
   296
apply (blast intro: unique_NB [THEN conjunct1])
paulson@14203
   297
done
paulson@14203
   298
paulson@14203
   299
paulson@14203
   300
text{*Can we strengthen the secrecy theorem?  NO*}
paulson@14203
   301
lemma "[| A \<notin> bad;  B \<notin> bad |]
paulson@14203
   302
  ==> Nprg \<in> Always
paulson@14203
   303
              {s. Says B A (Crypt (pubK A) {|Nonce NA, Nonce NB|}) \<in> set s
paulson@14203
   304
                  --> Nonce NB \<notin> analz (spies s)}"
paulson@14203
   305
apply ns_induct
paulson@14203
   306
apply auto
paulson@14203
   307
txt{*Fake*}
paulson@14203
   308
apply spy_analz
paulson@14203
   309
txt{*NS2: by freshness and unicity of NB*}
paulson@14203
   310
 apply (blast intro: no_nonce_NS1_NS2_reachable)
paulson@14203
   311
txt{*NS3: unicity of NB identifies A and NA, but not B*}
paulson@14203
   312
apply (frule_tac A'=A in Says_imp_spies [THEN parts.Inj, THEN unique_NB])
paulson@14203
   313
apply (erule Says_imp_spies [THEN parts.Inj], auto)
paulson@14203
   314
apply (rename_tac s B' C)
paulson@14203
   315
txt{*This is the attack!
paulson@14203
   316
@{subgoals[display,indent=0,margin=65]}
paulson@14203
   317
*}
paulson@14203
   318
oops
paulson@14203
   319
paulson@14203
   320
paulson@14203
   321
(*
paulson@14203
   322
THIS IS THE ATTACK!
paulson@14203
   323
[| A \<notin> bad; B \<notin> bad |]
paulson@14203
   324
==> Nprg
paulson@14203
   325
   \<in> Always
paulson@14203
   326
       {s. Says B A (Crypt (pubK A) {|Nonce NA, Nonce NB|}) \<in> set s -->
paulson@14203
   327
           Nonce NB \<notin> analz (knows Spy s)}
paulson@14203
   328
 1. !!s B' C.
paulson@14203
   329
       [| A \<notin> bad; B \<notin> bad; s \<in> reachable Nprg
paulson@14203
   330
          Says A C (Crypt (pubK C) {|Nonce NA, Agent A|}) \<in> set s;
paulson@14203
   331
          Says B' A (Crypt (pubK A) {|Nonce NA, Nonce NB|}) \<in> set s;
paulson@14203
   332
          C \<in> bad; Says B A (Crypt (pubK A) {|Nonce NA, Nonce NB|}) \<in> set s;
paulson@14203
   333
          Nonce NB \<notin> analz (knows Spy s) |]
paulson@14203
   334
       ==> False
paulson@14203
   335
*)
paulson@11195
   336
paulson@11195
   337
end