author  paulson 
Mon, 23 Sep 1996 18:21:31 +0200  
changeset 2014  5be4c8ca7b25 
parent 1976  1cff1f4fdb8a 
child 2032  1bbf1bdcaf56 
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 

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 