1(*  Title:      HOL/Auth/WooLam.thy
2    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
3    Copyright   1996  University of Cambridge
4*)
5
6section\<open>The Woo-Lam Protocol\<close>
7
8theory WooLam imports Public begin
9
10text\<open>Simplified version from page 11 of
11  Abadi and Needham (1996). 
12  Prudent Engineering Practice for Cryptographic Protocols.
13  IEEE Trans. S.E. 22(1), pages 6-15.
14
15Note: this differs from the Woo-Lam protocol discussed by Lowe (1996):
16  Some New Attacks upon Security Protocols.
17  Computer Security Foundations Workshop
18\<close>
19
20inductive_set woolam :: "event list set"
21  where
22         (*Initial trace is empty*)
23   Nil:  "[] \<in> woolam"
24
25         (** These rules allow agents to send messages to themselves **)
26
27         (*The spy MAY say anything he CAN say.  We do not expect him to
28           invent new nonces here, but he can also use NS1.  Common to
29           all similar protocols.*)
30 | Fake: "[| evsf \<in> woolam;  X \<in> synth (analz (spies evsf)) |]
31          ==> Says Spy B X  # evsf \<in> woolam"
32
33         (*Alice initiates a protocol run*)
34 | WL1:  "evs1 \<in> woolam ==> Says A B (Agent A) # evs1 \<in> woolam"
35
36         (*Bob responds to Alice's message with a challenge.*)
37 | WL2:  "[| evs2 \<in> woolam;  Says A' B (Agent A) \<in> set evs2 |]
38          ==> Says B A (Nonce NB) # evs2 \<in> woolam"
39
40         (*Alice responds to Bob's challenge by encrypting NB with her key.
41           B is *not* properly determined -- Alice essentially broadcasts
42           her reply.*)
43 | WL3:  "[| evs3 \<in> woolam;
44             Says A  B (Agent A)  \<in> set evs3;
45             Says B' A (Nonce NB) \<in> set evs3 |]
46          ==> Says A B (Crypt (shrK A) (Nonce NB)) # evs3 \<in> woolam"
47
48         (*Bob forwards Alice's response to the Server.  NOTE: usually
49           the messages are shown in chronological order, for clarity.
50           But here, exchanging the two events would cause the lemma
51           WL4_analz_spies to pick up the wrong assumption!*)
52 | WL4:  "[| evs4 \<in> woolam;
53             Says A'  B X         \<in> set evs4;
54             Says A'' B (Agent A) \<in> set evs4 |]
55          ==> Says B Server \<lbrace>Agent A, Agent B, X\<rbrace> # evs4 \<in> woolam"
56
57         (*Server decrypts Alice's response for Bob.*)
58 | WL5:  "[| evs5 \<in> woolam;
59             Says B' Server \<lbrace>Agent A, Agent B, Crypt (shrK A) (Nonce NB)\<rbrace>
60               \<in> set evs5 |]
61          ==> Says Server B (Crypt (shrK B) \<lbrace>Agent A, Nonce NB\<rbrace>)
62                 # evs5 \<in> woolam"
63
64
65declare Says_imp_knows_Spy [THEN analz.Inj, dest]
66declare parts.Body  [dest]
67declare analz_into_parts [dest]
68declare Fake_parts_insert_in_Un  [dest]
69
70
71(*A "possibility property": there are traces that reach the end*)
72lemma "\<exists>NB. \<exists>evs \<in> woolam.
73             Says Server B (Crypt (shrK B) \<lbrace>Agent A, Nonce NB\<rbrace>) \<in> set evs"
74apply (intro exI bexI)
75apply (rule_tac [2] woolam.Nil
76                    [THEN woolam.WL1, THEN woolam.WL2, THEN woolam.WL3,
77                     THEN woolam.WL4, THEN woolam.WL5], possibility)
78done
79
80(*Could prove forwarding lemmas for WL4, but we do not need them!*)
81
82(**** Inductive proofs about woolam ****)
83
84(** Theorems of the form X \<notin> parts (spies evs) imply that NOBODY
85    sends messages containing X! **)
86
87(*Spy never sees a good agent's shared key!*)
88lemma Spy_see_shrK [simp]:
89     "evs \<in> woolam ==> (Key (shrK A) \<in> parts (spies evs)) = (A \<in> bad)"
90by (erule woolam.induct, force, simp_all, blast+)
91
92lemma Spy_analz_shrK [simp]:
93     "evs \<in> woolam ==> (Key (shrK A) \<in> analz (spies evs)) = (A \<in> bad)"
94by auto
95
96lemma Spy_see_shrK_D [dest!]:
97     "[|Key (shrK A) \<in> parts (knows Spy evs);  evs \<in> woolam|] ==> A \<in> bad"
98by (blast dest: Spy_see_shrK)
99
100
101(**** Autheticity properties for Woo-Lam ****)
102
103(*** WL4 ***)
104
105(*If the encrypted message appears then it originated with Alice*)
106lemma NB_Crypt_imp_Alice_msg:
107     "[| Crypt (shrK A) (Nonce NB) \<in> parts (spies evs);
108         A \<notin> bad;  evs \<in> woolam |]
109      ==> \<exists>B. Says A B (Crypt (shrK A) (Nonce NB)) \<in> set evs"
110by (erule rev_mp, erule woolam.induct, force, simp_all, blast+)
111
112(*Guarantee for Server: if it gets a message containing a certificate from
113  Alice, then she originated that certificate.  But we DO NOT know that B
114  ever saw it: the Spy may have rerouted the message to the Server.*)
115lemma Server_trusts_WL4 [dest]:
116     "[| Says B' Server \<lbrace>Agent A, Agent B, Crypt (shrK A) (Nonce NB)\<rbrace>
117           \<in> set evs;
118         A \<notin> bad;  evs \<in> woolam |]
119      ==> \<exists>B. Says A B (Crypt (shrK A) (Nonce NB)) \<in> set evs"
120by (blast intro!: NB_Crypt_imp_Alice_msg)
121
122
123(*** WL5 ***)
124
125(*Server sent WL5 only if it received the right sort of message*)
126lemma Server_sent_WL5 [dest]:
127     "[| Says Server B (Crypt (shrK B) \<lbrace>Agent A, NB\<rbrace>) \<in> set evs;
128         evs \<in> woolam |]
129      ==> \<exists>B'. Says B' Server \<lbrace>Agent A, Agent B, Crypt (shrK A) NB\<rbrace>
130             \<in> set evs"
131by (erule rev_mp, erule woolam.induct, force, simp_all, blast+)
132
133(*If the encrypted message appears then it originated with the Server!*)
134lemma NB_Crypt_imp_Server_msg [rule_format]:
135     "[| Crypt (shrK B) \<lbrace>Agent A, NB\<rbrace> \<in> parts (spies evs);
136         B \<notin> bad;  evs \<in> woolam |]
137      ==> Says Server B (Crypt (shrK B) \<lbrace>Agent A, NB\<rbrace>) \<in> set evs"
138by (erule rev_mp, erule woolam.induct, force, simp_all, blast+)
139
140(*Guarantee for B.  If B gets the Server's certificate then A has encrypted
141  the nonce using her key.  This event can be no older than the nonce itself.
142  But A may have sent the nonce to some other agent and it could have reached
143  the Server via the Spy.*)
144lemma B_trusts_WL5:
145     "[| Says S B (Crypt (shrK B) \<lbrace>Agent A, Nonce NB\<rbrace>) \<in> set evs;
146         A \<notin> bad;  B \<notin> bad;  evs \<in> woolam  |]
147      ==> \<exists>B. Says A B (Crypt (shrK A) (Nonce NB)) \<in> set evs"
148by (blast dest!: NB_Crypt_imp_Server_msg)
149
150
151(*B only issues challenges in response to WL1.  Not used.*)
152lemma B_said_WL2:
153     "[| Says B A (Nonce NB) \<in> set evs;  B \<noteq> Spy;  evs \<in> woolam |]
154      ==> \<exists>A'. Says A' B (Agent A) \<in> set evs"
155by (erule rev_mp, erule woolam.induct, force, simp_all, blast+)
156
157
158(**CANNOT be proved because A doesn't know where challenges come from...*)
159lemma "[| A \<notin> bad;  B \<noteq> Spy;  evs \<in> woolam |]
160  ==> Crypt (shrK A) (Nonce NB) \<in> parts (spies evs) \<and>
161      Says B A (Nonce NB) \<in> set evs
162      \<longrightarrow> Says A B (Crypt (shrK A) (Nonce NB)) \<in> set evs"
163apply (erule rev_mp, erule woolam.induct, force, simp_all, blast, auto)
164oops
165
166end
167