1(*  Title:      HOL/Auth/NS_Public.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.
6Version incorporating Lowe's fix (inclusion of B's identity in round 2).
7*)
8
9section\<open>Verifying the Needham-Schroeder-Lowe Public-Key Protocol\<close>
10
11theory NS_Public imports Public begin
12
13inductive_set ns_public :: "event list set"
14  where 
15         (*Initial trace is empty*)
16   Nil:  "[] \<in> ns_public"
17
18         (*The spy MAY say anything he CAN say.  We do not expect him to
19           invent new nonces here, but he can also use NS1.  Common to
20           all similar protocols.*)
21 | Fake: "\<lbrakk>evsf \<in> ns_public;  X \<in> synth (analz (spies evsf))\<rbrakk>
22          \<Longrightarrow> Says Spy B X  # evsf \<in> ns_public"
23
24         (*Alice initiates a protocol run, sending a nonce to Bob*)
25 | NS1:  "\<lbrakk>evs1 \<in> ns_public;  Nonce NA \<notin> used evs1\<rbrakk>
26          \<Longrightarrow> Says A B (Crypt (pubEK B) \<lbrace>Nonce NA, Agent A\<rbrace>)
27                 # evs1  \<in>  ns_public"
28
29         (*Bob responds to Alice's message with a further nonce*)
30 | NS2:  "\<lbrakk>evs2 \<in> ns_public;  Nonce NB \<notin> used evs2;
31           Says A' B (Crypt (pubEK B) \<lbrace>Nonce NA, Agent A\<rbrace>) \<in> set evs2\<rbrakk>
32          \<Longrightarrow> Says B A (Crypt (pubEK A) \<lbrace>Nonce NA, Nonce NB, Agent B\<rbrace>)
33                # evs2  \<in>  ns_public"
34
35         (*Alice proves her existence by sending NB back to Bob.*)
36 | NS3:  "\<lbrakk>evs3 \<in> ns_public;
37           Says A  B (Crypt (pubEK B) \<lbrace>Nonce NA, Agent A\<rbrace>) \<in> set evs3;
38           Says B' A (Crypt (pubEK A) \<lbrace>Nonce NA, Nonce NB, Agent B\<rbrace>)
39              \<in> set evs3\<rbrakk>
40          \<Longrightarrow> Says A B (Crypt (pubEK B) (Nonce NB)) # evs3 \<in> ns_public"
41
42declare knows_Spy_partsEs [elim]
43declare knows_Spy_partsEs [elim]
44declare analz_into_parts [dest]
45declare Fake_parts_insert_in_Un [dest]
46
47(*A "possibility property": there are traces that reach the end*)
48lemma "\<exists>NB. \<exists>evs \<in> ns_public. Says A B (Crypt (pubEK B) (Nonce NB)) \<in> set evs"
49apply (intro exI bexI)
50apply (rule_tac [2] ns_public.Nil [THEN ns_public.NS1, THEN ns_public.NS2, 
51                                   THEN ns_public.NS3], possibility)
52done
53
54(** Theorems of the form X \<notin> parts (spies evs) imply that NOBODY
55    sends messages containing X! **)
56
57(*Spy never sees another agent's private key! (unless it's bad at start)*)
58lemma Spy_see_priEK [simp]: 
59      "evs \<in> ns_public \<Longrightarrow> (Key (priEK A) \<in> parts (spies evs)) = (A \<in> bad)"
60by (erule ns_public.induct, auto)
61
62lemma Spy_analz_priEK [simp]: 
63      "evs \<in> ns_public \<Longrightarrow> (Key (priEK A) \<in> analz (spies evs)) = (A \<in> bad)"
64by auto
65
66subsection\<open>Authenticity properties obtained from NS2\<close>
67
68
69(*It is impossible to re-use a nonce in both NS1 and NS2, provided the nonce
70  is secret.  (Honest users generate fresh nonces.)*)
71lemma no_nonce_NS1_NS2 [rule_format]: 
72      "evs \<in> ns_public 
73       \<Longrightarrow> Crypt (pubEK C) \<lbrace>NA', Nonce NA, Agent D\<rbrace> \<in> parts (spies evs) \<longrightarrow>
74           Crypt (pubEK B) \<lbrace>Nonce NA, Agent A\<rbrace> \<in> parts (spies evs) \<longrightarrow>  
75           Nonce NA \<in> analz (spies evs)"
76apply (erule ns_public.induct, simp_all)
77apply (blast intro: analz_insertI)+
78done
79
80(*Unicity for NS1: nonce NA identifies agents A and B*)
81lemma unique_NA: 
82     "\<lbrakk>Crypt(pubEK B)  \<lbrace>Nonce NA, Agent A \<rbrace> \<in> parts(spies evs);  
83       Crypt(pubEK B') \<lbrace>Nonce NA, Agent A'\<rbrace> \<in> parts(spies evs);  
84       Nonce NA \<notin> analz (spies evs); evs \<in> ns_public\<rbrakk>
85      \<Longrightarrow> A=A' \<and> B=B'"
86apply (erule rev_mp, erule rev_mp, erule rev_mp)   
87apply (erule ns_public.induct, simp_all)
88(*Fake, NS1*)
89apply (blast intro: analz_insertI)+
90done
91
92
93(*Secrecy: Spy does not see the nonce sent in msg NS1 if A and B are secure
94  The major premise "Says A B ..." makes it a dest-rule, so we use
95  (erule rev_mp) rather than rule_format. *)
96theorem Spy_not_see_NA: 
97      "\<lbrakk>Says A B (Crypt(pubEK B) \<lbrace>Nonce NA, Agent A\<rbrace>) \<in> set evs;
98        A \<notin> bad;  B \<notin> bad;  evs \<in> ns_public\<rbrakk>                     
99       \<Longrightarrow> Nonce NA \<notin> analz (spies evs)"
100apply (erule rev_mp)   
101apply (erule ns_public.induct, simp_all, spy_analz)
102apply (blast dest: unique_NA intro: no_nonce_NS1_NS2)+
103done
104
105
106(*Authentication for A: if she receives message 2 and has used NA
107  to start a run, then B has sent message 2.*)
108lemma A_trusts_NS2_lemma [rule_format]: 
109   "\<lbrakk>A \<notin> bad;  B \<notin> bad;  evs \<in> ns_public\<rbrakk>                     
110    \<Longrightarrow> Crypt (pubEK A) \<lbrace>Nonce NA, Nonce NB, Agent B\<rbrace> \<in> parts (spies evs) \<longrightarrow>
111        Says A B (Crypt(pubEK B) \<lbrace>Nonce NA, Agent A\<rbrace>) \<in> set evs \<longrightarrow>
112        Says B A (Crypt(pubEK A) \<lbrace>Nonce NA, Nonce NB, Agent B\<rbrace>) \<in> set evs"
113apply (erule ns_public.induct, simp_all)
114(*Fake, NS1*)
115apply (blast dest: Spy_not_see_NA)+
116done
117
118theorem A_trusts_NS2: 
119     "\<lbrakk>Says A  B (Crypt(pubEK B) \<lbrace>Nonce NA, Agent A\<rbrace>) \<in> set evs;   
120       Says B' A (Crypt(pubEK A) \<lbrace>Nonce NA, Nonce NB, Agent B\<rbrace>) \<in> set evs;
121       A \<notin> bad;  B \<notin> bad;  evs \<in> ns_public\<rbrakk>                     
122      \<Longrightarrow> Says B A (Crypt(pubEK A) \<lbrace>Nonce NA, Nonce NB, Agent B\<rbrace>) \<in> set evs"
123by (blast intro: A_trusts_NS2_lemma)
124
125
126(*If the encrypted message appears then it originated with Alice in NS1*)
127lemma B_trusts_NS1 [rule_format]:
128     "evs \<in> ns_public                                         
129      \<Longrightarrow> Crypt (pubEK B) \<lbrace>Nonce NA, Agent A\<rbrace> \<in> parts (spies evs) \<longrightarrow>
130          Nonce NA \<notin> analz (spies evs) \<longrightarrow>
131          Says A B (Crypt (pubEK B) \<lbrace>Nonce NA, Agent A\<rbrace>) \<in> set evs"
132apply (erule ns_public.induct, simp_all)
133(*Fake*)
134apply (blast intro!: analz_insertI)
135done
136
137
138subsection\<open>Authenticity properties obtained from NS2\<close>
139
140(*Unicity for NS2: nonce NB identifies nonce NA and agents A, B 
141  [unicity of B makes Lowe's fix work]
142  [proof closely follows that for unique_NA] *)
143
144lemma unique_NB [dest]: 
145     "\<lbrakk>Crypt(pubEK A)  \<lbrace>Nonce NA, Nonce NB, Agent B\<rbrace> \<in> parts(spies evs);
146       Crypt(pubEK A') \<lbrace>Nonce NA', Nonce NB, Agent B'\<rbrace> \<in> parts(spies evs);
147       Nonce NB \<notin> analz (spies evs); evs \<in> ns_public\<rbrakk>
148      \<Longrightarrow> A=A' \<and> NA=NA' \<and> B=B'"
149apply (erule rev_mp, erule rev_mp, erule rev_mp)   
150apply (erule ns_public.induct, simp_all)
151(*Fake, NS2*)
152apply (blast intro: analz_insertI)+
153done
154
155
156(*Secrecy: Spy does not see the nonce sent in msg NS2 if A and B are secure*)
157theorem Spy_not_see_NB [dest]:
158     "\<lbrakk>Says B A (Crypt (pubEK A) \<lbrace>Nonce NA, Nonce NB, Agent B\<rbrace>) \<in> set evs;
159       A \<notin> bad;  B \<notin> bad;  evs \<in> ns_public\<rbrakk>
160      \<Longrightarrow> Nonce NB \<notin> analz (spies evs)"
161apply (erule rev_mp)
162apply (erule ns_public.induct, simp_all, spy_analz)
163apply (blast intro: no_nonce_NS1_NS2)+
164done
165
166
167(*Authentication for B: if he receives message 3 and has used NB
168  in message 2, then A has sent message 3.*)
169lemma B_trusts_NS3_lemma [rule_format]:
170     "\<lbrakk>A \<notin> bad;  B \<notin> bad;  evs \<in> ns_public\<rbrakk> \<Longrightarrow>
171      Crypt (pubEK B) (Nonce NB) \<in> parts (spies evs) \<longrightarrow>
172      Says B A (Crypt (pubEK A) \<lbrace>Nonce NA, Nonce NB, Agent B\<rbrace>) \<in> set evs \<longrightarrow>
173      Says A B (Crypt (pubEK B) (Nonce NB)) \<in> set evs"
174by (erule ns_public.induct, auto)
175
176theorem B_trusts_NS3:
177     "\<lbrakk>Says B A  (Crypt (pubEK A) \<lbrace>Nonce NA, Nonce NB, Agent B\<rbrace>) \<in> set evs;
178       Says A' B (Crypt (pubEK B) (Nonce NB)) \<in> set evs;             
179       A \<notin> bad;  B \<notin> bad;  evs \<in> ns_public\<rbrakk>                    
180      \<Longrightarrow> Says A B (Crypt (pubEK B) (Nonce NB)) \<in> set evs"
181by (blast intro: B_trusts_NS3_lemma)
182
183subsection\<open>Overall guarantee for B\<close>
184
185(*If NS3 has been sent and the nonce NB agrees with the nonce B joined with
186  NA, then A initiated the run using NA.*)
187theorem B_trusts_protocol:
188     "\<lbrakk>A \<notin> bad;  B \<notin> bad;  evs \<in> ns_public\<rbrakk> \<Longrightarrow>
189      Crypt (pubEK B) (Nonce NB) \<in> parts (spies evs) \<longrightarrow>
190      Says B A  (Crypt (pubEK A) \<lbrace>Nonce NA, Nonce NB, Agent B\<rbrace>) \<in> set evs \<longrightarrow>
191      Says A B (Crypt (pubEK B) \<lbrace>Nonce NA, Agent A\<rbrace>) \<in> set evs"
192by (erule ns_public.induct, auto)
193
194end
195