1941
|
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 |
From page 244 of
|
|
9 |
Burrows, Abadi and Needham. A Logic of Authentication.
|
|
10 |
Proc. Royal Soc. 426 (1989)
|
|
11 |
*)
|
|
12 |
|
|
13 |
OtwayRees = Shared +
|
|
14 |
|
|
15 |
consts otway :: "event list set"
|
|
16 |
inductive otway
|
|
17 |
intrs
|
|
18 |
(*Initial trace is empty*)
|
|
19 |
Nil "[]: otway"
|
|
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: otway; B ~= Enemy; X: synth (analz (sees Enemy evs))
|
|
25 |
|] ==> Says Enemy B X # evs : otway"
|
|
26 |
|
|
27 |
(*Alice initiates a protocol run*)
|
|
28 |
OR1 "[| evs: otway; A ~= B
|
|
29 |
|] ==> Says A B {|Nonce (newN evs), Agent A, Agent B,
|
|
30 |
Crypt {|Nonce (newN evs), Agent A, Agent B|}
|
|
31 |
(shrK A) |}
|
|
32 |
# evs : otway"
|
|
33 |
|
|
34 |
(*Bob's response to Alice's message. Bob doesn't know who
|
|
35 |
the sender is, hence the A' in the sender field.
|
|
36 |
We modify the published protocol by NOT encrypting NB.*)
|
|
37 |
OR2 "[| evs: otway; B ~= Server;
|
|
38 |
Says A' B {|Nonce NA, Agent A, Agent B, X|} : set_of_list evs
|
|
39 |
|] ==> Says B Server
|
|
40 |
{|Nonce NA, Agent A, Agent B, X, Nonce (newN evs),
|
|
41 |
Crypt {|Nonce NA, Agent A, Agent B|} (shrK B)|}
|
|
42 |
# evs : otway"
|
|
43 |
|
|
44 |
(*The Server receives Bob's message and checks that the three NAs
|
|
45 |
match. Then he sends a new session key to Bob with a packet for
|
|
46 |
forwarding to Alice.*)
|
|
47 |
OR3 "[| evs: otway; B ~= Server;
|
|
48 |
Says B' Server
|
|
49 |
{|Nonce NA, Agent A, Agent B,
|
|
50 |
Crypt {|Nonce NA, Agent A, Agent B|} (shrK A),
|
|
51 |
Nonce NB,
|
|
52 |
Crypt {|Nonce NA, Agent A, Agent B|} (shrK B)|}
|
|
53 |
: set_of_list evs
|
|
54 |
|] ==> Says Server B
|
|
55 |
{|Nonce NA,
|
|
56 |
Crypt {|Nonce NA, Key (newK evs)|} (shrK A),
|
|
57 |
Crypt {|Nonce NB, Key (newK evs)|} (shrK B)|}
|
|
58 |
# evs : otway"
|
|
59 |
|
|
60 |
(*Bob receives the Server's (?) message and compares the Nonces with
|
|
61 |
those in the message he previously sent the Server.*)
|
|
62 |
OR4 "[| evs: otway; A ~= B;
|
|
63 |
Says S B {|Nonce NA, X, Crypt {|Nonce NB, Key K|} (shrK B)|}
|
|
64 |
: set_of_list evs;
|
|
65 |
Says B Server {|Nonce NA, Agent A, Agent B, X', Nonce NB, X''|}
|
|
66 |
: set_of_list evs
|
|
67 |
|] ==> (Says B A {|Nonce NA, X|}) # evs : otway"
|
|
68 |
|
|
69 |
(*Alice checks her Nonce, then sends a dummy message to Bob,
|
|
70 |
using the new session key.*)
|
|
71 |
OR5 "[| evs: otway;
|
|
72 |
Says B' A {|Nonce NA, Crypt {|Nonce NA, Key K|} (shrK A)|}
|
|
73 |
: set_of_list evs;
|
|
74 |
Says A B {|Nonce NA, Agent A, Agent B, X|} : set_of_list evs
|
|
75 |
|] ==> Says A B (Crypt (Agent A) K) # evs : otway"
|
|
76 |
|
|
77 |
end
|