author  nipkow 
Fri, 24 Nov 2000 16:49:27 +0100  
changeset 10519  ade64af4c57c 
parent 5434  9b4bed3f394c 
child 11104  f2024fed9f0c 
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.*) 

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

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

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

1965  27 
(*Alice initiates a protocol run, requesting to talk to any B*) 
5434
9b4bed3f394c
Got rid of not_Says_to_self and most uses of ~= in definitions and theorems
paulson
parents:
5359
diff
changeset

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

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

30 
: ns_shared" 
1934  31 

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

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

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

35 
the sender field.*) 

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

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

37 
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

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

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

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

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

42 
# evs2 : ns_shared" 
1934  43 

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

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

45 
Need A ~= 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

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

47 
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

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

49 
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

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

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

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

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

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

55 
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

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

57 
: ns_shared" 
1934  58 

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

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

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

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

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

64 
NS5 "[ evs5: ns_shared; 
3659
eddedfe2f3f8
Renamed "evs" to "evs1", "evs2", etc. in protocol inductive definition
paulson
parents:
3519
diff
changeset

65 
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

66 
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

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

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

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

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

5359  73 
Oops "[ evso: ns_shared; 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

74 
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

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

76 
==> Notes Spy {Nonce NA, Nonce NB, Key K} # evso : ns_shared" 
1934  77 

78 
end 