author  nipkow 
Fri, 24 Nov 2000 16:49:27 +0100  
changeset 10519  ade64af4c57c 
parent 6333  b1dec44d0018 
child 11185  1b737b4c2108 
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.*) 

6308
76f3865a2b1d
Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents:
5434
diff
changeset

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

6308
76f3865a2b1d
Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents:
5434
diff
changeset

28 
(*A message that has been sent can be received by the 
76f3865a2b1d
Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents:
5434
diff
changeset

29 
intended recipient.*) 
76f3865a2b1d
Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents:
5434
diff
changeset

30 
Reception "[ evsr: otway; Says A B X : set evsr ] 
76f3865a2b1d
Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents:
5434
diff
changeset

31 
==> Gets B X # evsr : otway" 
76f3865a2b1d
Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents:
5434
diff
changeset

32 

2002  33 
(*Alice initiates a protocol run*) 
5434
9b4bed3f394c
Got rid of not_Says_to_self and most uses of ~= in definitions and theorems
paulson
parents:
5359
diff
changeset

34 
OR1 "[ evs1: otway; Nonce NA ~: used evs1 ] 
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

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

36 
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

37 
# evs1 : otway" 
2002  38 

6333  39 
(*Bob's response to Alice's message. 
40 
This variant of the protocol does NOT encrypt NB.*) 

5434
9b4bed3f394c
Got rid of not_Says_to_self and most uses of ~= in definitions and theorems
paulson
parents:
5359
diff
changeset

41 
OR2 "[ evs2: otway; Nonce NB ~: used evs2; 
6308
76f3865a2b1d
Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents:
5434
diff
changeset

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

44 
{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

45 
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

46 
# evs2 : otway" 
2002  47 

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

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

50 
forwarding to Alice.*) 

5434
9b4bed3f394c
Got rid of not_Says_to_self and most uses of ~= in definitions and theorems
paulson
parents:
5359
diff
changeset

51 
OR3 "[ evs3: otway; Key KAB ~: used evs3; 
6308
76f3865a2b1d
Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents:
5434
diff
changeset

52 
Gets Server 
2002  53 
{Nonce NA, Agent A, Agent B, 
2284
80ebd1a213fd
Swapped arguments of Crypt (for clarity and because it is conventional)
paulson
parents:
2131
diff
changeset

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

56 
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

57 
: set evs3 ] 
2002  58 
==> Says Server B 
59 
{Nonce NA, 

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

60 
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

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

62 
# evs3 : otway" 
2002  63 

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

5434
9b4bed3f394c
Got rid of not_Says_to_self and most uses of ~= in definitions and theorems
paulson
parents:
5359
diff
changeset

65 
those in the message he previously sent the Server. 
9b4bed3f394c
Got rid of not_Says_to_self and most uses of ~= in definitions and theorems
paulson
parents:
5359
diff
changeset

66 
Need B ~= Server because we allow messages to self.*) 
6308
76f3865a2b1d
Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents:
5434
diff
changeset

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

68 
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

69 
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

70 
: set evs4; 
6308
76f3865a2b1d
Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents:
5434
diff
changeset

71 
Gets 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

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

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

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

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

78 
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

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

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

82 
end 