author  paulson 
Thu, 08 Jan 1998 18:10:34 +0100  
changeset 4537  4e835bd9fada 
parent 3683  aafe719dff14 
child 5359  bd539b72d484 
permissions  rwrr 
2090  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 

8 
Simplified version with minimal encryption but explicit messages 

9 

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

10 
Note that the formalization does not even assume that nonces are fresh. 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

11 
This is because the protocol does not rely on uniqueness of nonces for 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

12 
security, only for freshness, and the proof script does not prove freshness 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

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

14 

2090  15 
From page 11 of 
16 
Abadi and Needham. Prudent Engineering Practice for Cryptographic Protocols. 

17 
IEEE Trans. SE 22 (1), 1996 

18 
*) 

19 

20 
OtwayRees_AN = Shared + 

21 

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

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

23 
inductive "otway" 
2090  24 
intrs 
25 
(*Initial trace is empty*) 

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

26 
Nil "[]: otway" 
2090  27 

28 
(*The spy MAY say anything he CAN say. We do not expect him to 

29 
invent new nonces here, but he can also use NS1. Common to 

30 
all similar protocols.*) 

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

31 
Fake "[ evs: otway; B ~= Spy; 
3683  32 
X: synth (analz (spies evs)) ] 
3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3466
diff
changeset

33 
==> Says Spy B X # evs : otway" 
2090  34 

35 
(*Alice initiates a protocol run*) 

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

36 
OR1 "[ evs1: otway; A ~= B; B ~= Server ] 
eddedfe2f3f8
Renamed "evs" to "evs1", "evs2", etc. in protocol inductive definition
paulson
parents:
3519
diff
changeset

37 
==> Says A B {Agent A, Agent B, Nonce NA} # evs1 : otway" 
2090  38 

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

40 
the sender is, hence the A' in the sender field.*) 

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

41 
OR2 "[ evs2: otway; B ~= Server; 
eddedfe2f3f8
Renamed "evs" to "evs1", "evs2", etc. in protocol inductive definition
paulson
parents:
3519
diff
changeset

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

43 
==> Says B Server {Agent A, Agent B, Nonce NA, Nonce NB} 
3659
eddedfe2f3f8
Renamed "evs" to "evs1", "evs2", etc. in protocol inductive definition
paulson
parents:
3519
diff
changeset

44 
# evs2 : otway" 
2090  45 

46 
(*The Server receives Bob's message. Then he sends a new 

47 
session key to Bob with a packet for forwarding to Alice.*) 

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

48 
OR3 "[ evs3: otway; B ~= Server; A ~= B; Key KAB ~: used evs3; 
2090  49 
Says B' Server {Agent A, Agent B, Nonce NA, Nonce NB} 
3659
eddedfe2f3f8
Renamed "evs" to "evs1", "evs2", etc. in protocol inductive definition
paulson
parents:
3519
diff
changeset

50 
: set evs3 ] 
2090  51 
==> Says Server B 
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

52 
{Crypt (shrK A) {Nonce NA, Agent A, Agent B, Key KAB}, 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

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

54 
# evs3 : otway" 
2090  55 

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

57 
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

58 
OR4 "[ evs4: otway; A ~= B; 
eddedfe2f3f8
Renamed "evs" to "evs1", "evs2", etc. in protocol inductive definition
paulson
parents:
3519
diff
changeset

59 
Says B Server {Agent A, Agent B, Nonce NA, Nonce NB} : set evs4; 
2837
dee1c7f1f576
Trivial renamings (for consistency with CSFW papers)
paulson
parents:
2516
diff
changeset

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

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

62 
==> Says B A X # evs4 : otway" 
2090  63 

2131  64 
(*This message models possible leaks of session keys. The nonces 
65 
identify the protocol run. B is not assumed to know shrK A.*) 

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

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

68 
{Crypt (shrK A) {Nonce NA, Agent A, Agent B, Key K}, 
80ebd1a213fd
Swapped arguments of Crypt (for clarity and because it is conventional)
paulson
parents:
2131
diff
changeset

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

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

71 
==> Notes Spy {Nonce NA, Nonce NB, Key K} # evso : otway" 
2090  72 

73 
end 