author  nipkow 
Fri, 24 Nov 2000 16:49:27 +0100  
changeset 10519  ade64af4c57c 
parent 6333  b1dec44d0018 
child 11185  1b737b4c2108 
permissions  rwrr 
6308
76f3865a2b1d
Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents:
5434
diff
changeset

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

2 
Inductive relation "otway" for the OtwayRees protocol 
76f3865a2b1d
Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents:
5434
diff
changeset

3 
extended by Gets primitive. 
1941  4 

2014
5be4c8ca7b25
Correction of protocol; addition of Reveal message; proofs of
paulson
parents:
1976
diff
changeset

5 
Version that encrypts Nonce NB 
5be4c8ca7b25
Correction of protocol; addition of Reveal message; proofs of
paulson
parents:
1976
diff
changeset

6 

1941  7 
*) 
8 

9 
OtwayRees = Shared + 

10 

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

11 

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

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

13 
inductive "otway" 
1941  14 
intrs 
15 
(*Initial trace is empty*) 

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

16 
Nil "[]: otway" 
1941  17 

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

18 
(** These rules allow agents to send messages to themselves **) 
9b4bed3f394c
Got rid of not_Says_to_self and most uses of ~= in definitions and theorems
paulson
parents:
5359
diff
changeset

19 

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

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

23 
Fake "[ evsa: otway; X: synth (analz (knows Spy evsa)) ] 
76f3865a2b1d
Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents:
5434
diff
changeset

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

25 

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

26 
(*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

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

28 
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

29 
==> Gets B X # evsr : otway" 
1941  30 

31 
(*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

32 
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

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

34 
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

35 
# evs1 : otway" 
1941  36 

6333  37 
(*Bob's response to Alice's message. Note that NB is encrypted.*) 
5434
9b4bed3f394c
Got rid of not_Says_to_self and most uses of ~= in definitions and theorems
paulson
parents:
5359
diff
changeset

38 
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

39 
Gets B {Nonce NA, Agent A, Agent B, X} : set evs2 ] 
1976  40 
==> Says B Server 
2014
5be4c8ca7b25
Correction of protocol; addition of Reveal message; proofs of
paulson
parents:
1976
diff
changeset

41 
{Nonce NA, Agent A, Agent B, X, 
2451
ce85a2aafc7a
Extensive tidying and simplification, largely stemming from
paulson
parents:
2378
diff
changeset

42 
Crypt (shrK B) 
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

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

44 
# evs2 : otway" 
1941  45 

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

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

48 
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

49 
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

50 
Gets Server 
1941  51 
{Nonce NA, Agent A, Agent B, 
2284
80ebd1a213fd
Swapped arguments of Crypt (for clarity and because it is conventional)
paulson
parents:
2135
diff
changeset

52 
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

53 
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

54 
: set evs3 ] 
1976  55 
==> Says Server B 
1941  56 
{Nonce NA, 
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

57 
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

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

59 
# evs3 : otway" 
1941  60 

61 
(*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

62 
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

63 
Need B ~= Server because we allow messages to self.*) 
9b4bed3f394c
Got rid of not_Says_to_self and most uses of ~= in definitions and theorems
paulson
parents:
5359
diff
changeset

64 
OR4 "[ evs4: otway; B ~= Server; 
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; 
6308
76f3865a2b1d
Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents:
5434
diff
changeset

69 
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

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.*) 

5359  75 
Oops "[ evso: otway; 
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 