author  paulson 
Mon, 14 Jul 1997 12:47:21 +0200  
changeset 3519  ab0a9fbed4c0 
parent 3465  e85c24717cad 
child 3659  eddedfe2f3f8 
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 

3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3465
diff
changeset

17 
consts otway :: event list set 
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3465
diff
changeset

18 
inductive "otway" 
1941  19 
intrs 
20 
(*Initial trace is empty*) 

3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3465
diff
changeset

21 
Nil "[]: otway" 
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.*) 

3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3465
diff
changeset

26 
Fake "[ evs: otway; B ~= Spy; 
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3465
diff
changeset

27 
X: synth (analz (sees Spy evs)) ] 
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3465
diff
changeset

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

30 
(*Alice initiates a protocol run*) 

3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3465
diff
changeset

31 
OR1 "[ evs: otway; A ~= B; B ~= Server; Nonce NA ~: used evs ] 
2516
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} } 
3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3465
diff
changeset

34 
# evs : otway" 
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.*) 
3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3465
diff
changeset

39 
OR2 "[ evs: otway; 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}} 
3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3465
diff
changeset

45 
# evs : otway" 
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.*) 

3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3465
diff
changeset

50 
OR3 "[ evs: otway; 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}} 
3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3465
diff
changeset

60 
# evs : otway" 
1941  61 

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

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

3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3465
diff
changeset

64 
OR4 "[ evs: otway; 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 ] 
3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3465
diff
changeset

71 
==> Says B A {Nonce NA, X} # evs : otway" 
1941  72 

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

3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3465
diff
changeset

75 
Oops "[ evs: otway; 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 ] 
3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3465
diff
changeset

78 
==> Says B Spy {Nonce NA, Nonce NB, Key K} # evs : otway" 
1941  79 

80 
end 