author  paulson 
Thu, 08 Jan 1998 18:10:34 +0100  
changeset 4537  4e835bd9fada 
parent 3683  aafe719dff14 
child 5359  bd539b72d484 
permissions  rwrr 
1934  1 
(* Title: HOL/Auth/NS_Shared 
2 
ID: $Id$ 

3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 

4 
Copyright 1996 University of Cambridge 

5 

6 
Inductive relation "ns_shared" for NeedhamSchroeder SharedKey protocol. 

7 

8 
From page 247 of 

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

10 
Proc. Royal Soc. 426 (1989) 

11 
*) 

12 

13 
NS_Shared = Shared + 

14 

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

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

16 
inductive "ns_shared" 
1934  17 
intrs 
18 
(*Initial trace is empty*) 

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

19 
Nil "[]: ns_shared" 
1934  20 

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

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

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

26 
==> Says Spy B X # evs : ns_shared" 
1934  27 

1965  28 
(*Alice initiates a protocol run, requesting to talk to any B*) 
3659
eddedfe2f3f8
Renamed "evs" to "evs1", "evs2", etc. in protocol inductive definition
paulson
parents:
3519
diff
changeset

29 
NS1 "[ evs1: ns_shared; A ~= Server; Nonce NA ~: used evs1 ] 
eddedfe2f3f8
Renamed "evs" to "evs1", "evs2", etc. in protocol inductive definition
paulson
parents:
3519
diff
changeset

30 
==> Says A Server {Agent A, Agent B, Nonce NA} # evs1 
3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3465
diff
changeset

31 
: ns_shared" 
1934  32 

33 
(*Server's response to Alice's message. 

34 
!! It may respond more than once to A's request !! 

35 
Server doesn't know who the true sender is, hence the A' in 

36 
the sender field.*) 

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

37 
NS2 "[ evs2: ns_shared; A ~= B; A ~= Server; Key KAB ~: used evs2; 
eddedfe2f3f8
Renamed "evs" to "evs1", "evs2", etc. in protocol inductive definition
paulson
parents:
3519
diff
changeset

38 
Says A' Server {Agent A, Agent B, Nonce NA} : set evs2 ] 
2451
ce85a2aafc7a
Extensive tidying and simplification, largely stemming from
paulson
parents:
2378
diff
changeset

39 
==> Says Server A 
ce85a2aafc7a
Extensive tidying and simplification, largely stemming from
paulson
parents:
2378
diff
changeset

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

41 
{Nonce NA, Agent B, Key KAB, 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

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

43 
# evs2 : ns_shared" 
1934  44 

45 
(*We can't assume S=Server. Agent A "remembers" her nonce. 

1997  46 
Can inductively show A ~= Server*) 
3659
eddedfe2f3f8
Renamed "evs" to "evs1", "evs2", etc. in protocol inductive definition
paulson
parents:
3519
diff
changeset

47 
NS3 "[ evs3: ns_shared; A ~= B; 
2284
80ebd1a213fd
Swapped arguments of Crypt (for clarity and because it is conventional)
paulson
parents:
2131
diff
changeset

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

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

50 
Says A Server {Agent A, Agent B, Nonce NA} : set evs3 ] 
eddedfe2f3f8
Renamed "evs" to "evs1", "evs2", etc. in protocol inductive definition
paulson
parents:
3519
diff
changeset

51 
==> Says A B X # evs3 : ns_shared" 
1934  52 

53 
(*Bob's nonce exchange. He does not know who the message came 

54 
from, but responds to A because she is mentioned inside.*) 

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

55 
NS4 "[ evs4: ns_shared; A ~= B; Nonce NB ~: used evs4; 
eddedfe2f3f8
Renamed "evs" to "evs1", "evs2", etc. in protocol inductive definition
paulson
parents:
3519
diff
changeset

56 
Says A' B (Crypt (shrK B) {Key K, Agent A}) : set evs4 ] 
eddedfe2f3f8
Renamed "evs" to "evs1", "evs2", etc. in protocol inductive definition
paulson
parents:
3519
diff
changeset

57 
==> Says B A (Crypt K (Nonce NB)) # evs4 
3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3465
diff
changeset

58 
: ns_shared" 
1934  59 

2069  60 
(*Alice responds with Nonce NB if she has seen the key before. 
61 
Maybe should somehow check Nonce NA again. 

62 
We do NOT send NB1 or similar as the Spy cannot spoof such things. 

63 
Letting the Spy add or subtract 1 lets him send ALL nonces. 

64 
Instead we distinguish the messages by sending the nonce twice.*) 

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

65 
NS5 "[ evs5: ns_shared; A ~= B; 
eddedfe2f3f8
Renamed "evs" to "evs1", "evs2", etc. in protocol inductive definition
paulson
parents:
3519
diff
changeset

66 
Says B' A (Crypt K (Nonce NB)) : set evs5; 
2284
80ebd1a213fd
Swapped arguments of Crypt (for clarity and because it is conventional)
paulson
parents:
2131
diff
changeset

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

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

69 
==> Says A B (Crypt K {Nonce NB, Nonce NB}) # evs5 : ns_shared" 
2069  70 

71 
(*This message models possible leaks of session keys. 

2131  72 
The two Nonces identify the protocol run: the rule insists upon 
73 
the true senders in order to make them accurate.*) 

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

74 
Oops "[ evso: ns_shared; A ~= Spy; 
eddedfe2f3f8
Renamed "evs" to "evs1", "evs2", etc. in protocol inductive definition
paulson
parents:
3519
diff
changeset

75 
Says B A (Crypt K (Nonce NB)) : set evso; 
2284
80ebd1a213fd
Swapped arguments of Crypt (for clarity and because it is conventional)
paulson
parents:
2131
diff
changeset

76 
Says Server A (Crypt (shrK A) {Nonce NA, Agent B, Key K, X}) 
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 : ns_shared" 
1934  79 

80 
end 