author  paulson 
Tue, 09 Mar 1999 11:01:39 +0100  
changeset 6308  76f3865a2b1d 
parent 5434  9b4bed3f394c 
child 6333  b1dec44d0018 
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 

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

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

2105  39 
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

40 
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

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

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

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

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

46 
# evs2 : otway" 
1941  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 
1941  53 
{Nonce NA, Agent A, Agent B, 
2284
80ebd1a213fd
Swapped arguments of Crypt (for clarity and because it is conventional)
paulson
parents:
2135
diff
changeset

54 
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

55 
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

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

59 
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

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

61 
# evs3 : otway" 
1941  62 

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

64 
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

65 
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

66 
OR4 "[ evs4: otway; B ~= Server; 
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', 
2284
80ebd1a213fd
Swapped arguments of Crypt (for clarity and because it is conventional)
paulson
parents:
2135
diff
changeset

68 
Crypt (shrK B) 
80ebd1a213fd
Swapped arguments of Crypt (for clarity and because it is conventional)
paulson
parents:
2135
diff
changeset

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

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" 
1941  74 

2135  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:
2135
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:
3683
diff
changeset

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

82 
end 