author | paulson |
Mon, 23 Sep 1996 18:21:31 +0200 | |
changeset 2014 | 5be4c8ca7b25 |
parent 1976 | 1cff1f4fdb8a |
child 2032 | 1bbf1bdcaf56 |
permissions | -rw-r--r-- |
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 |
||
2014
5be4c8ca7b25
Correction of protocol; addition of Reveal message; proofs of
paulson
parents:
1976
diff
changeset
|
8 |
Version that encrypts Nonce NB |
5be4c8ca7b25
Correction of protocol; addition of Reveal message; proofs of
paulson
parents:
1976
diff
changeset
|
9 |
|
1941 | 10 |
From page 244 of |
11 |
Burrows, Abadi and Needham. A Logic of Authentication. |
|
12 |
Proc. Royal Soc. 426 (1989) |
|
13 |
*) |
|
14 |
||
15 |
OtwayRees = Shared + |
|
16 |
||
17 |
consts otway :: "event list set" |
|
18 |
inductive otway |
|
19 |
intrs |
|
20 |
(*Initial trace is empty*) |
|
21 |
Nil "[]: otway" |
|
22 |
||
23 |
(*The enemy 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.*) |
|
1976 | 26 |
Fake "[| evs: otway; B ~= Enemy; X: synth (analz (sees Enemy evs)) |] |
27 |
==> Says Enemy B X # evs : otway" |
|
1941 | 28 |
|
29 |
(*Alice initiates a protocol run*) |
|
2014
5be4c8ca7b25
Correction of protocol; addition of Reveal message; proofs of
paulson
parents:
1976
diff
changeset
|
30 |
OR1 "[| evs: otway; A ~= B; B ~= Server |] |
1976 | 31 |
==> Says A B {|Nonce (newN evs), Agent A, Agent B, |
2014
5be4c8ca7b25
Correction of protocol; addition of Reveal message; proofs of
paulson
parents:
1976
diff
changeset
|
32 |
Crypt {|Nonce (newN evs), Agent A, Agent B|} |
5be4c8ca7b25
Correction of protocol; addition of Reveal message; proofs of
paulson
parents:
1976
diff
changeset
|
33 |
(shrK A) |} |
1941 | 34 |
# evs : otway" |
35 |
||
36 |
(*Bob's response to Alice's message. Bob doesn't know who |
|
37 |
the sender is, hence the A' in the sender field. |
|
38 |
We modify the published protocol by NOT encrypting NB.*) |
|
39 |
OR2 "[| evs: otway; B ~= Server; |
|
1976 | 40 |
Says A' B {|Nonce NA, Agent A, Agent B, X|} : set_of_list evs |] |
41 |
==> Says B Server |
|
2014
5be4c8ca7b25
Correction of protocol; addition of Reveal message; proofs of
paulson
parents:
1976
diff
changeset
|
42 |
{|Nonce NA, Agent A, Agent B, X, |
5be4c8ca7b25
Correction of protocol; addition of Reveal message; proofs of
paulson
parents:
1976
diff
changeset
|
43 |
Crypt {|Nonce NA, Nonce (newN evs), |
5be4c8ca7b25
Correction of protocol; addition of Reveal message; proofs of
paulson
parents:
1976
diff
changeset
|
44 |
Agent A, Agent B|} (shrK B)|} |
1941 | 45 |
# evs : otway" |
46 |
||
47 |
(*The Server receives Bob's message and checks that the three NAs |
|
48 |
match. Then he sends a new session key to Bob with a packet for |
|
49 |
forwarding to Alice.*) |
|
50 |
OR3 "[| evs: otway; B ~= Server; |
|
51 |
Says B' Server |
|
52 |
{|Nonce NA, Agent A, Agent B, |
|
53 |
Crypt {|Nonce NA, Agent A, Agent B|} (shrK A), |
|
2014
5be4c8ca7b25
Correction of protocol; addition of Reveal message; proofs of
paulson
parents:
1976
diff
changeset
|
54 |
Crypt {|Nonce NA, Nonce NB, Agent A, Agent B|} (shrK B)|} |
1976 | 55 |
: set_of_list evs |] |
56 |
==> Says Server B |
|
1941 | 57 |
{|Nonce NA, |
58 |
Crypt {|Nonce NA, Key (newK evs)|} (shrK A), |
|
59 |
Crypt {|Nonce NB, Key (newK evs)|} (shrK B)|} |
|
60 |
# evs : otway" |
|
61 |
||
62 |
(*Bob receives the Server's (?) message and compares the Nonces with |
|
63 |
those in the message he previously sent the Server.*) |
|
2014
5be4c8ca7b25
Correction of protocol; addition of Reveal message; proofs of
paulson
parents:
1976
diff
changeset
|
64 |
OR4 "[| evs: otway; A ~= B; B ~= Server; |
1941 | 65 |
Says S B {|Nonce NA, X, Crypt {|Nonce NB, Key K|} (shrK B)|} |
66 |
: set_of_list evs; |
|
2014
5be4c8ca7b25
Correction of protocol; addition of Reveal message; proofs of
paulson
parents:
1976
diff
changeset
|
67 |
Says B Server {|Nonce NA, Agent A, Agent B, X', |
5be4c8ca7b25
Correction of protocol; addition of Reveal message; proofs of
paulson
parents:
1976
diff
changeset
|
68 |
Crypt {|Nonce NA, Nonce NB, Agent A, Agent B|} |
5be4c8ca7b25
Correction of protocol; addition of Reveal message; proofs of
paulson
parents:
1976
diff
changeset
|
69 |
(shrK B)|} |
1976 | 70 |
: set_of_list evs |] |
2014
5be4c8ca7b25
Correction of protocol; addition of Reveal message; proofs of
paulson
parents:
1976
diff
changeset
|
71 |
==> Says B A {|Nonce NA, X|} # evs : otway" |
1941 | 72 |
|
2014
5be4c8ca7b25
Correction of protocol; addition of Reveal message; proofs of
paulson
parents:
1976
diff
changeset
|
73 |
(*This message models possible leaks of session keys. Alice's Nonce |
5be4c8ca7b25
Correction of protocol; addition of Reveal message; proofs of
paulson
parents:
1976
diff
changeset
|
74 |
identifies the protocol run.*) |
5be4c8ca7b25
Correction of protocol; addition of Reveal message; proofs of
paulson
parents:
1976
diff
changeset
|
75 |
Reveal "[| evs: otway; A ~= Enemy; |
5be4c8ca7b25
Correction of protocol; addition of Reveal message; proofs of
paulson
parents:
1976
diff
changeset
|
76 |
Says B' A {|Nonce NA, Crypt {|Nonce NA, Key K|} (shrK A)|} |
5be4c8ca7b25
Correction of protocol; addition of Reveal message; proofs of
paulson
parents:
1976
diff
changeset
|
77 |
: set_of_list evs; |
5be4c8ca7b25
Correction of protocol; addition of Reveal message; proofs of
paulson
parents:
1976
diff
changeset
|
78 |
Says A B {|Nonce NA, Agent A, Agent B, |
5be4c8ca7b25
Correction of protocol; addition of Reveal message; proofs of
paulson
parents:
1976
diff
changeset
|
79 |
Crypt {|Nonce NA, Agent A, Agent B|} (shrK A)|} |
5be4c8ca7b25
Correction of protocol; addition of Reveal message; proofs of
paulson
parents:
1976
diff
changeset
|
80 |
: set_of_list evs |] |
5be4c8ca7b25
Correction of protocol; addition of Reveal message; proofs of
paulson
parents:
1976
diff
changeset
|
81 |
==> Says A Enemy {|Nonce NA, Key K|} # evs : otway" |
1941 | 82 |
|
83 |
end |