author  paulson 
Thu, 08 Jan 1998 18:10:34 +0100  
changeset 4537  4e835bd9fada 
parent 3683  aafe719dff14 
child 5359  bd539b72d484 
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; 
3683  27 
X: synth (analz (spies evs)) ] 
3519
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*) 

3659
eddedfe2f3f8
Renamed "evs" to "evs1", "evs2", etc. in protocol inductive definition
paulson
parents:
3519
diff
changeset

31 
OR1 "[ evs1: otway; A ~= B; B ~= Server; Nonce NA ~: used evs1 ] 
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} } 
3659
eddedfe2f3f8
Renamed "evs" to "evs1", "evs2", etc. in protocol inductive definition
paulson
parents:
3519
diff
changeset

34 
# evs1 : 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.*) 
3659
eddedfe2f3f8
Renamed "evs" to "evs1", "evs2", etc. in protocol inductive definition
paulson
parents:
3519
diff
changeset

39 
OR2 "[ evs2: otway; B ~= Server; Nonce NB ~: used evs2; 
eddedfe2f3f8
Renamed "evs" to "evs1", "evs2", etc. in protocol inductive definition
paulson
parents:
3519
diff
changeset

40 
Says A' B {Nonce NA, Agent A, Agent B, X} : set evs2 ] 
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}} 
3659
eddedfe2f3f8
Renamed "evs" to "evs1", "evs2", etc. in protocol inductive definition
paulson
parents:
3519
diff
changeset

45 
# evs2 : 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.*) 

3659
eddedfe2f3f8
Renamed "evs" to "evs1", "evs2", etc. in protocol inductive definition
paulson
parents:
3519
diff
changeset

50 
OR3 "[ evs3: otway; B ~= Server; Key KAB ~: used evs3; 
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}} 
3659
eddedfe2f3f8
Renamed "evs" to "evs1", "evs2", etc. in protocol inductive definition
paulson
parents:
3519
diff
changeset

55 
: set evs3 ] 
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}} 
3659
eddedfe2f3f8
Renamed "evs" to "evs1", "evs2", etc. in protocol inductive definition
paulson
parents:
3519
diff
changeset

60 
# evs3 : 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.*) 

3659
eddedfe2f3f8
Renamed "evs" to "evs1", "evs2", etc. in protocol inductive definition
paulson
parents:
3519
diff
changeset

64 
OR4 "[ evs4: 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}} 
3659
eddedfe2f3f8
Renamed "evs" to "evs1", "evs2", etc. in protocol inductive definition
paulson
parents:
3519
diff
changeset

68 
: set evs4; 
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}} 
3659
eddedfe2f3f8
Renamed "evs" to "evs1", "evs2", etc. in protocol inductive definition
paulson
parents:
3519
diff
changeset

70 
: set evs4 ] 
eddedfe2f3f8
Renamed "evs" to "evs1", "evs2", etc. in protocol inductive definition
paulson
parents:
3519
diff
changeset

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

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

3659
eddedfe2f3f8
Renamed "evs" to "evs1", "evs2", etc. in protocol inductive definition
paulson
parents:
3519
diff
changeset

75 
Oops "[ evso: 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}} 
3659
eddedfe2f3f8
Renamed "evs" to "evs1", "evs2", etc. in protocol inductive definition
paulson
parents:
3519
diff
changeset

77 
: set evso ] 
4537
4e835bd9fada
Expressed most Oops rules using Notes instead of Says, and other tidying
paulson
parents:
3683
diff
changeset

78 
==> Notes Spy {Nonce NA, Nonce NB, Key K} # evso : otway" 
1941  79 

80 
end 