2090
|
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
|