|
1 (* Title: HOL/Auth/OtwayRees |
|
2 ID: $Id$ |
|
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
4 Copyright 1996 University of Cambridge |
|
5 |
|
6 Inductive relation "yahalom" for the Yahalom protocol. |
|
7 |
|
8 From page 257 of |
|
9 Burrows, Abadi and Needham. A Logic of Authentication. |
|
10 Proc. Royal Soc. 426 (1989) |
|
11 *) |
|
12 |
|
13 OtwayRees = Shared + |
|
14 |
|
15 consts yahalom :: "event list set" |
|
16 inductive yahalom |
|
17 intrs |
|
18 (*Initial trace is empty*) |
|
19 Nil "[]: yahalom" |
|
20 |
|
21 (*The enemy MAY say anything he CAN say. We do not expect him to |
|
22 invent new nonces here, but he can also use NS1. Common to |
|
23 all similar protocols.*) |
|
24 Fake "[| evs: yahalom; B ~= Enemy; X: synth (analz (sees Enemy evs)) |] |
|
25 ==> Says Enemy B X # evs : yahalom" |
|
26 |
|
27 (*Alice initiates a protocol run*) |
|
28 YM1 "[| evs: yahalom; A ~= B |] |
|
29 ==> Says A B {|Nonce (newN evs), Agent A |} # evs : yahalom" |
|
30 |
|
31 (*Bob's response to Alice's message. Bob doesn't know who |
|
32 the sender is, hence the A' in the sender field. |
|
33 We modify the published protocol by NOT encrypting NB.*) |
|
34 YM2 "[| evs: yahalom; B ~= Server; |
|
35 Says A' B {|Nonce NA, Agent A|} : set_of_list evs |] |
|
36 ==> Says B Server |
|
37 {|Agent B, |
|
38 Crypt {|Agent A, Nonce NA, Nonce (newN evs)|} (shrK B)|} |
|
39 # evs : yahalom" |
|
40 |
|
41 (*The Server receives Bob's message. He responds by sending a |
|
42 new session key to Alice, with a packet for forwarding to Bob.*) |
|
43 YM3 "[| evs: yahalom; B ~= Server; |
|
44 Says B' Server |
|
45 {|Nonce NA, Agent A, Agent B, |
|
46 Crypt {|Nonce NA, Agent A, Agent B|} (shrK A), |
|
47 Nonce NB, |
|
48 Crypt {|Nonce NA, Agent A, Agent B|} (shrK B)|} |
|
49 : set_of_list evs |] |
|
50 ==> Says Server B |
|
51 {|Nonce NA, |
|
52 Crypt {|Nonce NA, Key (newK evs)|} (shrK A), |
|
53 Crypt {|Nonce NB, Key (newK evs)|} (shrK B)|} |
|
54 # evs : yahalom" |
|
55 |
|
56 (*Bob receives the Server's (?) message and compares the Nonces with |
|
57 those in the message he previously sent the Server.*) |
|
58 YM4 "[| evs: yahalom; A ~= B; |
|
59 Says S B {|Nonce NA, X, Crypt {|Nonce NB, Key K|} (shrK B)|} |
|
60 : set_of_list evs; |
|
61 Says B Server {|Nonce NA, Agent A, Agent B, X', Nonce NB, X''|} |
|
62 : set_of_list evs |] |
|
63 ==> (Says B A {|Nonce NA, X|}) # evs : yahalom" |
|
64 |
|
65 (*Alice checks her Nonce, then sends a dummy message to Bob, |
|
66 using the new session key.*) |
|
67 YM5 "[| evs: yahalom; |
|
68 Says B' A {|Nonce NA, Crypt {|Nonce NA, Key K|} (shrK A)|} |
|
69 : set_of_list evs; |
|
70 Says A B {|Nonce NA, Agent A, Agent B, X|} : set_of_list evs |] |
|
71 ==> Says A B (Crypt (Agent A) K) # evs : yahalom" |
|
72 |
|
73 end |