1(*  Title:      HOL/Auth/NS_Public_Bad.thy
2    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
3    Copyright   1996  University of Cambridge
4
5Inductive relation "ns_public" for the Needham-Schroeder Public-Key protocol.
6Flawed version, vulnerable to Lowe's attack.
7
8From page 260 of
9  Burrows, Abadi and Needham.  A Logic of Authentication.
10  Proc. Royal Soc. 426 (1989)
11*)
12
13section\<open>Verifying the Needham-Schroeder Public-Key Protocol\<close>
14
15theory NS_Public_Bad imports Public begin
16
17inductive_set ns_public :: "event list set"
18  where
19         (*Initial trace is empty*)
20   Nil:  "[] \<in> ns_public"
21
22         (*The spy MAY say anything he CAN say.  We do not expect him to
23           invent new nonces here, but he can also use NS1.  Common to
24           all similar protocols.*)
25 | Fake: "\<lbrakk>evsf \<in> ns_public;  X \<in> synth (analz (spies evsf))\<rbrakk>
26          \<Longrightarrow> Says Spy B X  # evsf \<in> ns_public"
27
28         (*Alice initiates a protocol run, sending a nonce to Bob*)
29 | NS1:  "\<lbrakk>evs1 \<in> ns_public;  Nonce NA \<notin> used evs1\<rbrakk>
30          \<Longrightarrow> Says A B (Crypt (pubEK B) \<lbrace>Nonce NA, Agent A\<rbrace>)
31                # evs1  \<in>  ns_public"
32
33         (*Bob responds to Alice's message with a further nonce*)
34 | NS2:  "\<lbrakk>evs2 \<in> ns_public;  Nonce NB \<notin> used evs2;
35           Says A' B (Crypt (pubEK B) \<lbrace>Nonce NA, Agent A\<rbrace>) \<in> set evs2\<rbrakk>
36          \<Longrightarrow> Says B A (Crypt (pubEK A) \<lbrace>Nonce NA, Nonce NB\<rbrace>)
37                # evs2  \<in>  ns_public"
38
39         (*Alice proves her existence by sending NB back to Bob.*)
40 | NS3:  "\<lbrakk>evs3 \<in> ns_public;
41           Says A  B (Crypt (pubEK B) \<lbrace>Nonce NA, Agent A\<rbrace>) \<in> set evs3;
42           Says B' A (Crypt (pubEK A) \<lbrace>Nonce NA, Nonce NB\<rbrace>) \<in> set evs3\<rbrakk>
43          \<Longrightarrow> Says A B (Crypt (pubEK B) (Nonce NB)) # evs3 \<in> ns_public"
44
45declare knows_Spy_partsEs [elim]
46declare analz_into_parts [dest]
47declare Fake_parts_insert_in_Un [dest]
48
49(*A "possibility property": there are traces that reach the end*)
50lemma "\<exists>NB. \<exists>evs \<in> ns_public. Says A B (Crypt (pubEK B) (Nonce NB)) \<in> set evs"
51apply (intro exI bexI)
52apply (rule_tac [2] ns_public.Nil [THEN ns_public.NS1, THEN ns_public.NS2, 
53                                   THEN ns_public.NS3])
54by possibility
55
56
57(**** Inductive proofs about ns_public ****)
58
59(** Theorems of the form X \<notin> parts (spies evs) imply that NOBODY
60    sends messages containing X! **)
61
62(*Spy never sees another agent's private key! (unless it's bad at start)*)
63lemma Spy_see_priEK [simp]: 
64      "evs \<in> ns_public \<Longrightarrow> (Key (priEK A) \<in> parts (spies evs)) = (A \<in> bad)"
65by (erule ns_public.induct, auto)
66
67lemma Spy_analz_priEK [simp]: 
68      "evs \<in> ns_public \<Longrightarrow> (Key (priEK A) \<in> analz (spies evs)) = (A \<in> bad)"
69by auto
70
71
72(*** Authenticity properties obtained from NS2 ***)
73
74(*It is impossible to re-use a nonce in both NS1 and NS2, provided the nonce
75  is secret.  (Honest users generate fresh nonces.)*)
76lemma no_nonce_NS1_NS2 [rule_format]: 
77      "evs \<in> ns_public 
78       \<Longrightarrow> Crypt (pubEK C) \<lbrace>NA', Nonce NA\<rbrace> \<in> parts (spies evs) \<longrightarrow>
79           Crypt (pubEK B) \<lbrace>Nonce NA, Agent A\<rbrace> \<in> parts (spies evs) \<longrightarrow>  
80           Nonce NA \<in> analz (spies evs)"
81apply (erule ns_public.induct, simp_all)
82apply (blast intro: analz_insertI)+
83done
84
85
86(*Unicity for NS1: nonce NA identifies agents A and B*)
87lemma unique_NA: 
88     "\<lbrakk>Crypt(pubEK B)  \<lbrace>Nonce NA, Agent A \<rbrace> \<in> parts(spies evs);  
89       Crypt(pubEK B') \<lbrace>Nonce NA, Agent A'\<rbrace> \<in> parts(spies evs);  
90       Nonce NA \<notin> analz (spies evs); evs \<in> ns_public\<rbrakk>
91      \<Longrightarrow> A=A' \<and> B=B'"
92apply (erule rev_mp, erule rev_mp, erule rev_mp)   
93apply (erule ns_public.induct, simp_all)
94(*Fake, NS1*)
95apply (blast intro!: analz_insertI)+
96done
97
98
99(*Secrecy: Spy does not see the nonce sent in msg NS1 if A and B are secure
100  The major premise "Says A B ..." makes it a dest-rule, so we use
101  (erule rev_mp) rather than rule_format. *)
102theorem Spy_not_see_NA: 
103      "\<lbrakk>Says A B (Crypt(pubEK B) \<lbrace>Nonce NA, Agent A\<rbrace>) \<in> set evs;
104        A \<notin> bad;  B \<notin> bad;  evs \<in> ns_public\<rbrakk>                     
105       \<Longrightarrow> Nonce NA \<notin> analz (spies evs)"
106apply (erule rev_mp)   
107apply (erule ns_public.induct, simp_all, spy_analz)
108apply (blast dest: unique_NA intro: no_nonce_NS1_NS2)+
109done
110
111
112(*Authentication for A: if she receives message 2 and has used NA
113  to start a run, then B has sent message 2.*)
114lemma A_trusts_NS2_lemma [rule_format]: 
115   "\<lbrakk>A \<notin> bad;  B \<notin> bad;  evs \<in> ns_public\<rbrakk>                     
116    \<Longrightarrow> Crypt (pubEK A) \<lbrace>Nonce NA, Nonce NB\<rbrace> \<in> parts (spies evs) \<longrightarrow>
117        Says A B (Crypt(pubEK B) \<lbrace>Nonce NA, Agent A\<rbrace>) \<in> set evs \<longrightarrow>
118        Says B A (Crypt(pubEK A) \<lbrace>Nonce NA, Nonce NB\<rbrace>) \<in> set evs"
119apply (erule ns_public.induct)
120apply (auto dest: Spy_not_see_NA unique_NA)
121done
122
123theorem A_trusts_NS2: 
124     "\<lbrakk>Says A  B (Crypt(pubEK B) \<lbrace>Nonce NA, Agent A\<rbrace>) \<in> set evs;   
125       Says B' A (Crypt(pubEK A) \<lbrace>Nonce NA, Nonce NB\<rbrace>) \<in> set evs;
126       A \<notin> bad;  B \<notin> bad;  evs \<in> ns_public\<rbrakk>                     
127      \<Longrightarrow> Says B A (Crypt(pubEK A) \<lbrace>Nonce NA, Nonce NB\<rbrace>) \<in> set evs"
128by (blast intro: A_trusts_NS2_lemma)
129
130
131(*If the encrypted message appears then it originated with Alice in NS1*)
132lemma B_trusts_NS1 [rule_format]:
133     "evs \<in> ns_public                                         
134      \<Longrightarrow> Crypt (pubEK B) \<lbrace>Nonce NA, Agent A\<rbrace> \<in> parts (spies evs) \<longrightarrow>
135          Nonce NA \<notin> analz (spies evs) \<longrightarrow>
136          Says A B (Crypt (pubEK B) \<lbrace>Nonce NA, Agent A\<rbrace>) \<in> set evs"
137apply (erule ns_public.induct, simp_all)
138(*Fake*)
139apply (blast intro!: analz_insertI)
140done
141
142
143
144(*** Authenticity properties obtained from NS2 ***)
145
146(*Unicity for NS2: nonce NB identifies nonce NA and agent A
147  [proof closely follows that for unique_NA] *)
148lemma unique_NB [dest]: 
149     "\<lbrakk>Crypt(pubEK A)  \<lbrace>Nonce NA, Nonce NB\<rbrace> \<in> parts(spies evs);
150       Crypt(pubEK A') \<lbrace>Nonce NA', Nonce NB\<rbrace> \<in> parts(spies evs);
151       Nonce NB \<notin> analz (spies evs); evs \<in> ns_public\<rbrakk>
152     \<Longrightarrow> A=A' \<and> NA=NA'"
153apply (erule rev_mp, erule rev_mp, erule rev_mp)   
154apply (erule ns_public.induct, simp_all)
155(*Fake, NS2*)
156apply (blast intro!: analz_insertI)+
157done
158
159
160(*NB remains secret PROVIDED Alice never responds with round 3*)
161theorem Spy_not_see_NB [dest]:
162     "\<lbrakk>Says B A (Crypt (pubEK A) \<lbrace>Nonce NA, Nonce NB\<rbrace>) \<in> set evs;   
163       \<forall>C. Says A C (Crypt (pubEK C) (Nonce NB)) \<notin> set evs;       
164       A \<notin> bad;  B \<notin> bad;  evs \<in> ns_public\<rbrakk>                      
165     \<Longrightarrow> Nonce NB \<notin> analz (spies evs)"
166apply (erule rev_mp, erule rev_mp)
167apply (erule ns_public.induct, simp_all, spy_analz)
168apply (simp_all add: all_conj_distrib) (*speeds up the next step*)
169apply (blast intro: no_nonce_NS1_NS2)+
170done
171
172
173(*Authentication for B: if he receives message 3 and has used NB
174  in message 2, then A has sent message 3--to somebody....*)
175
176lemma B_trusts_NS3_lemma [rule_format]:
177     "\<lbrakk>A \<notin> bad;  B \<notin> bad;  evs \<in> ns_public\<rbrakk>                    
178      \<Longrightarrow> Crypt (pubEK B) (Nonce NB) \<in> parts (spies evs) \<longrightarrow>
179          Says B A  (Crypt (pubEK A) \<lbrace>Nonce NA, Nonce NB\<rbrace>) \<in> set evs \<longrightarrow>
180          (\<exists>C. Says A C (Crypt (pubEK C) (Nonce NB)) \<in> set evs)"
181apply (erule ns_public.induct, auto)
182by (blast intro: no_nonce_NS1_NS2)+
183
184theorem B_trusts_NS3:
185     "\<lbrakk>Says B A  (Crypt (pubEK A) \<lbrace>Nonce NA, Nonce NB\<rbrace>) \<in> set evs;
186       Says A' B (Crypt (pubEK B) (Nonce NB)) \<in> set evs;             
187       A \<notin> bad;  B \<notin> bad;  evs \<in> ns_public\<rbrakk>                    
188      \<Longrightarrow> \<exists>C. Says A C (Crypt (pubEK C) (Nonce NB)) \<in> set evs"
189by (blast intro: B_trusts_NS3_lemma)
190
191
192(*Can we strengthen the secrecy theorem Spy_not_see_NB?  NO*)
193lemma "\<lbrakk>A \<notin> bad;  B \<notin> bad;  evs \<in> ns_public\<rbrakk>            
194       \<Longrightarrow> Says B A (Crypt (pubEK A) \<lbrace>Nonce NA, Nonce NB\<rbrace>) \<in> set evs  
195           \<longrightarrow> Nonce NB \<notin> analz (spies evs)"
196apply (erule ns_public.induct, simp_all, spy_analz)
197(*NS1: by freshness*)
198apply blast
199(*NS2: by freshness and unicity of NB*)
200apply (blast intro: no_nonce_NS1_NS2)
201(*NS3: unicity of NB identifies A and NA, but not B*)
202apply clarify
203apply (frule_tac A' = A in 
204       Says_imp_knows_Spy [THEN parts.Inj, THEN unique_NB], auto)
205apply (rename_tac evs3 B' C)
206txt\<open>This is the attack!
207@{subgoals[display,indent=0,margin=65]}
208\<close>
209oops
210
211(*
212THIS IS THE ATTACK!
213Level 8
214!!evs. \<lbrakk>A \<notin> bad; B \<notin> bad; evs \<in> ns_public\<rbrakk>
215       \<Longrightarrow> Says B A (Crypt (pubEK A) \<lbrace>Nonce NA, Nonce NB\<rbrace>) \<in> set evs \<longrightarrow>
216           Nonce NB \<notin> analz (spies evs)
217 1. !!C B' evs3.
218       \<lbrakk>A \<notin> bad; B \<notin> bad; evs3 \<in> ns_public
219        Says A C (Crypt (pubEK C) \<lbrace>Nonce NA, Agent A\<rbrace>) \<in> set evs3;
220        Says B' A (Crypt (pubEK A) \<lbrace>Nonce NA, Nonce NB\<rbrace>) \<in> set evs3; 
221        C \<in> bad;
222        Says B A (Crypt (pubEK A) \<lbrace>Nonce NA, Nonce NB\<rbrace>) \<in> set evs3;
223        Nonce NB \<notin> analz (spies evs3)\<rbrakk>
224       \<Longrightarrow> False
225*)
226
227end
228