author  paulson 
Thu, 08 Jan 1998 18:10:34 +0100  
changeset 4537  4e835bd9fada 
parent 4522  0218c486cf07 
child 5359  bd539b72d484 
permissions  rwrr 
2002  1 
(* Title: HOL/Auth/OtwayRees_Bad 
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 

8 
The FAULTY version omitting encryption of Nonce NB, as suggested on page 247 of 

9 
Burrows, Abadi and Needham. A Logic of Authentication. 

10 
Proc. Royal Soc. 426 (1989) 

11 
*) 

12 

13 
OtwayRees_Bad = Shared + 

14 

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

15 
consts otway :: event list set 
2052  16 

2002  17 
inductive otway 
18 
intrs 

19 
(*Initial trace is empty*) 

20 
Nil "[]: otway" 

21 

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

3683  25 
Fake "[ evs: otway; B ~= Spy; X: synth (analz (spies evs)) ] 
2032  26 
==> Says Spy B X # evs : otway" 
2002  27 

28 
(*Alice initiates a protocol run*) 

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

29 
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

30 
==> 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

31 
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

32 
# evs1 : otway" 
2002  33 

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

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

36 
We modify the published protocol by NOT encrypting NB.*) 

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

37 
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

38 
Says A' B {Nonce NA, Agent A, Agent B, X} : set evs2 ] 
2002  39 
==> Says B Server 
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

40 
{Nonce NA, Agent A, Agent B, X, Nonce NB, 
2284
80ebd1a213fd
Swapped arguments of Crypt (for clarity and because it is conventional)
paulson
parents:
2131
diff
changeset

41 
Crypt (shrK B) {Nonce NA, Agent A, Agent B}} 
3659
eddedfe2f3f8
Renamed "evs" to "evs1", "evs2", etc. in protocol inductive definition
paulson
parents:
3519
diff
changeset

42 
# evs2 : otway" 
2002  43 

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

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

46 
forwarding to Alice.*) 

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

47 
OR3 "[ evs3: otway; B ~= Server; Key KAB ~: used evs3; 
2002  48 
Says B' Server 
49 
{Nonce NA, Agent A, Agent B, 

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

50 
Crypt (shrK A) {Nonce NA, Agent A, Agent B}, 
2002  51 
Nonce NB, 
2284
80ebd1a213fd
Swapped arguments of Crypt (for clarity and because it is conventional)
paulson
parents:
2131
diff
changeset

52 
Crypt (shrK B) {Nonce NA, Agent A, Agent B}} 
3659
eddedfe2f3f8
Renamed "evs" to "evs1", "evs2", etc. in protocol inductive definition
paulson
parents:
3519
diff
changeset

53 
: set evs3 ] 
2002  54 
==> Says Server B 
55 
{Nonce NA, 

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

56 
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

57 
Crypt (shrK B) {Nonce NB, Key KAB}} 
3659
eddedfe2f3f8
Renamed "evs" to "evs1", "evs2", etc. in protocol inductive definition
paulson
parents:
3519
diff
changeset

58 
# evs3 : otway" 
2002  59 

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

61 
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

62 
OR4 "[ evs4: otway; A ~= B; 
4522
0218c486cf07
Restored the ciphertext in OR4 in order to make the spec closer to that in
paulson
parents:
3683
diff
changeset

63 
Says B Server {Nonce NA, Agent A, Agent B, X', Nonce NB, 
0218c486cf07
Restored the ciphertext in OR4 in order to make the spec closer to that in
paulson
parents:
3683
diff
changeset

64 
Crypt (shrK B) {Nonce NA, Agent A, Agent B}} 
3659
eddedfe2f3f8
Renamed "evs" to "evs1", "evs2", etc. in protocol inductive definition
paulson
parents:
3519
diff
changeset

65 
: set evs4; 
2837
dee1c7f1f576
Trivial renamings (for consistency with CSFW papers)
paulson
parents:
2516
diff
changeset

66 
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

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

68 
==> Says B A {Nonce NA, X} # evs4 : otway" 
2002  69 

2131  70 
(*This message models possible leaks of session keys. The nonces 
71 
identify the protocol run.*) 

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

72 
Oops "[ evso: otway; B ~= Spy; 
2284
80ebd1a213fd
Swapped arguments of Crypt (for clarity and because it is conventional)
paulson
parents:
2131
diff
changeset

73 
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

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

75 
==> Notes Spy {Nonce NA, Nonce NB, Key K} # evso : otway" 
2002  76 

77 
end 