|
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 "otway" for the Otway-Rees protocol. |
|
7 |
|
8 Simplified version with minimal encryption but explicit messages |
|
9 |
|
10 From page 11 of |
|
11 Abadi and Needham. Prudent Engineering Practice for Cryptographic Protocols. |
|
12 IEEE Trans. SE 22 (1), 1996 |
|
13 *) |
|
14 |
|
15 OtwayRees_AN = Shared + |
|
16 |
|
17 consts otway :: "agent set => event list set" |
|
18 inductive "otway lost" |
|
19 intrs |
|
20 (*Initial trace is empty*) |
|
21 Nil "[]: otway lost" |
|
22 |
|
23 (*The spy MAY say anything he CAN say. We do not expect him to |
|
24 invent new nonces here, but he can also use NS1. Common to |
|
25 all similar protocols.*) |
|
26 Fake "[| evs: otway lost; B ~= Spy; |
|
27 X: synth (analz (sees lost Spy evs)) |] |
|
28 ==> Says Spy B X # evs : otway lost" |
|
29 |
|
30 (*Alice initiates a protocol run*) |
|
31 OR1 "[| evs: otway lost; A ~= B; B ~= Server |] |
|
32 ==> Says A B {|Agent A, Agent B, Nonce (newN evs)|} |
|
33 # evs : otway lost" |
|
34 |
|
35 (*Bob's response to Alice's message. Bob doesn't know who |
|
36 the sender is, hence the A' in the sender field.*) |
|
37 OR2 "[| evs: otway lost; B ~= Server; |
|
38 Says A' B {|Agent A, Agent B, Nonce NA|} : set_of_list evs |] |
|
39 ==> Says B Server {|Agent A, Agent B, Nonce NA, Nonce (newN evs)|} |
|
40 # evs : otway lost" |
|
41 |
|
42 (*The Server receives Bob's message. Then he sends a new |
|
43 session key to Bob with a packet for forwarding to Alice.*) |
|
44 OR3 "[| evs: otway lost; B ~= Server; A ~= B; |
|
45 Says B' Server {|Agent A, Agent B, Nonce NA, Nonce NB|} |
|
46 : set_of_list evs |] |
|
47 ==> Says Server B |
|
48 {|Crypt {|Nonce NA, Agent A, Agent B, Key(newK evs)|} (shrK A), |
|
49 Crypt {|Nonce NB, Agent A, Agent B, Key(newK evs)|} (shrK B)|} |
|
50 # evs : otway lost" |
|
51 |
|
52 (*Bob receives the Server's (?) message and compares the Nonces with |
|
53 those in the message he previously sent the Server.*) |
|
54 OR4 "[| evs: otway lost; A ~= B; B ~= Server; |
|
55 Says S B {|X, |
|
56 Crypt {|Nonce NB, Agent A, Agent B, Key K|} (shrK B)|} |
|
57 : set_of_list evs; |
|
58 Says B Server {|Agent A, Agent B, Nonce NA, Nonce NB|} |
|
59 : set_of_list evs |] |
|
60 ==> Says B A X # evs : otway lost" |
|
61 |
|
62 (*This message models possible leaks of session keys. Alice's Nonce |
|
63 identifies the protocol run.*) |
|
64 Revl "[| evs: otway lost; A ~= Spy; |
|
65 Says B' A (Crypt {|Nonce NA, Agent A, Agent B, Key K|} (shrK A)) |
|
66 : set_of_list evs; |
|
67 Says A B {|Agent A, Agent B, Nonce NA|} : set_of_list evs |] |
|
68 ==> Says A Spy {|Nonce NA, Key K|} # evs : otway lost" |
|
69 |
|
70 end |