author  paulson 
Thu, 19 Dec 1996 11:58:39 +0100  
changeset 2451  ce85a2aafc7a 
parent 2378  fc103154ad8f 
child 2516  4d68fbe6378b 
permissions  rwrr 
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 OtwayRees 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 

2378  17 
consts otway :: agent set => event list set 
2032  18 
inductive "otway lost" 
1941  19 
intrs 
20 
(*Initial trace is empty*) 

2032  21 
Nil "[]: otway lost" 
1941  22 

2032  23 
(*The spy MAY say anything he CAN say. We do not expect him to 
1941  24 
invent new nonces here, but he can also use NS1. Common to 
25 
all similar protocols.*) 

2032  26 
Fake "[ evs: otway lost; B ~= Spy; 
27 
X: synth (analz (sees lost Spy evs)) ] 

28 
==> Says Spy B X # evs : otway lost" 

1941  29 

30 
(*Alice initiates a protocol run*) 

2032  31 
OR1 "[ evs: otway lost; A ~= B; B ~= Server ] 
2451
ce85a2aafc7a
Extensive tidying and simplification, largely stemming from
paulson
parents:
2378
diff
changeset

32 
==> Says A B {Nonce (newN(length evs)), Agent A, Agent B, 
2284
80ebd1a213fd
Swapped arguments of Crypt (for clarity and because it is conventional)
paulson
parents:
2135
diff
changeset

33 
Crypt (shrK A) 
2451
ce85a2aafc7a
Extensive tidying and simplification, largely stemming from
paulson
parents:
2378
diff
changeset

34 
{Nonce (newN(length evs)), Agent A, Agent B} } 
2032  35 
# evs : otway lost" 
1941  36 

37 
(*Bob's response to Alice's message. Bob doesn't know who 

38 
the sender is, hence the A' in the sender field. 

2105  39 
Note that NB is encrypted.*) 
2032  40 
OR2 "[ evs: otway lost; B ~= Server; 
1976  41 
Says A' B {Nonce NA, Agent A, Agent B, X} : set_of_list evs ] 
42 
==> Says B Server 

2014
5be4c8ca7b25
Correction of protocol; addition of Reveal message; proofs of
paulson
parents:
1976
diff
changeset

43 
{Nonce NA, Agent A, Agent B, X, 
2451
ce85a2aafc7a
Extensive tidying and simplification, largely stemming from
paulson
parents:
2378
diff
changeset

44 
Crypt (shrK B) 
ce85a2aafc7a
Extensive tidying and simplification, largely stemming from
paulson
parents:
2378
diff
changeset

45 
{Nonce NA, Nonce(newN(length evs)), Agent A, Agent B}} 
2032  46 
# evs : otway lost" 
1941  47 

48 
(*The Server receives Bob's message and checks that the three NAs 

49 
match. Then he sends a new session key to Bob with a packet for 

50 
forwarding to Alice.*) 

2032  51 
OR3 "[ evs: otway lost; B ~= Server; 
1941  52 
Says B' Server 
53 
{Nonce NA, Agent A, Agent B, 

2284
80ebd1a213fd
Swapped arguments of Crypt (for clarity and because it is conventional)
paulson
parents:
2135
diff
changeset

54 
Crypt (shrK A) {Nonce NA, Agent A, Agent B}, 
80ebd1a213fd
Swapped arguments of Crypt (for clarity and because it is conventional)
paulson
parents:
2135
diff
changeset

55 
Crypt (shrK B) {Nonce NA, Nonce NB, Agent A, Agent B}} 
1976  56 
: set_of_list evs ] 
57 
==> Says Server B 

1941  58 
{Nonce NA, 
2451
ce85a2aafc7a
Extensive tidying and simplification, largely stemming from
paulson
parents:
2378
diff
changeset

59 
Crypt (shrK A) {Nonce NA, Key (newK(length evs))}, 
ce85a2aafc7a
Extensive tidying and simplification, largely stemming from
paulson
parents:
2378
diff
changeset

60 
Crypt (shrK B) {Nonce NB, Key (newK(length evs))}} 
2032  61 
# evs : otway lost" 
1941  62 

63 
(*Bob receives the Server's (?) message and compares the Nonces with 

64 
those in the message he previously sent the Server.*) 

2135  65 
OR4 "[ evs: otway lost; A ~= B; 
2284
80ebd1a213fd
Swapped arguments of Crypt (for clarity and because it is conventional)
paulson
parents:
2135
diff
changeset

66 
Says S B {Nonce NA, X, Crypt (shrK B) {Nonce NB, Key K}} 
1941  67 
: set_of_list evs; 
2014
5be4c8ca7b25
Correction of protocol; addition of Reveal message; proofs of
paulson
parents:
1976
diff
changeset

68 
Says B Server {Nonce NA, Agent A, Agent B, X', 
2284
80ebd1a213fd
Swapped arguments of Crypt (for clarity and because it is conventional)
paulson
parents:
2135
diff
changeset

69 
Crypt (shrK B) 
80ebd1a213fd
Swapped arguments of Crypt (for clarity and because it is conventional)
paulson
parents:
2135
diff
changeset

70 
{Nonce NA, Nonce NB, Agent A, Agent B}} 
1976  71 
: set_of_list evs ] 
2032  72 
==> Says B A {Nonce NA, X} # evs : otway lost" 
1941  73 

2135  74 
(*This message models possible leaks of session keys. The nonces 
75 
identify the protocol run.*) 

76 
Oops "[ evs: otway lost; B ~= Spy; 

2284
80ebd1a213fd
Swapped arguments of Crypt (for clarity and because it is conventional)
paulson
parents:
2135
diff
changeset

77 
Says Server B {Nonce NA, X, Crypt (shrK B) {Nonce NB, Key K}} 
2064  78 
: set_of_list evs ] 
2135  79 
==> Says B Spy {Nonce NA, Nonce NB, Key K} # evs : otway lost" 
1941  80 

81 
end 