author  paulson 
Fri, 11 Jul 1997 13:26:15 +0200  
changeset 3512  9dcb4daa15e8 
parent 3465  e85c24717cad 
child 3519  ab0a9fbed4c0 
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*) 

2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

31 
OR1 "[ evs: otway lost; A ~= B; B ~= Server; Nonce NA ~: used evs ] 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

32 
==> Says A B {Nonce NA, Agent A, Agent B, 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

33 
Crypt (shrK A) {Nonce NA, Agent A, Agent B} } 
2032  34 
# evs : otway lost" 
1941  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. 

2105  38 
Note that NB is encrypted.*) 
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

39 
OR2 "[ evs: otway lost; B ~= Server; Nonce NB ~: used evs; 
3465  40 
Says A' B {Nonce NA, Agent A, Agent B, X} : set evs ] 
1976  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, 
2451
ce85a2aafc7a
Extensive tidying and simplification, largely stemming from
paulson
parents:
2378
diff
changeset

43 
Crypt (shrK B) 
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

44 
{Nonce NA, Nonce NB, Agent A, Agent B}} 
2032  45 
# evs : otway lost" 
1941  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.*) 

2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

50 
OR3 "[ evs: otway lost; B ~= Server; Key KAB ~: used evs; 
1941  51 
Says B' Server 
52 
{Nonce NA, Agent A, Agent B, 

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

53 
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

54 
Crypt (shrK B) {Nonce NA, Nonce NB, Agent A, Agent B}} 
3465  55 
: set evs ] 
1976  56 
==> Says Server B 
1941  57 
{Nonce NA, 
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

58 
Crypt (shrK A) {Nonce NA, Key KAB}, 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

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

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

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

2135  64 
OR4 "[ evs: otway lost; A ~= B; 
2014
5be4c8ca7b25
Correction of protocol; addition of Reveal message; proofs of
paulson
parents:
1976
diff
changeset

65 
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

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

67 
{Nonce NA, Nonce NB, Agent A, Agent B}} 
3465  68 
: set evs; 
2837
dee1c7f1f576
Trivial renamings (for consistency with CSFW papers)
paulson
parents:
2516
diff
changeset

69 
Says S' B {Nonce NA, X, Crypt (shrK B) {Nonce NB, Key K}} 
3465  70 
: set evs ] 
2032  71 
==> Says B A {Nonce NA, X} # evs : otway lost" 
1941  72 

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

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

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

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

80 
end 