author | paulson |
Wed, 24 May 2000 18:44:19 +0200 | |
changeset 8954 | 4fbdda40bb5f |
parent 5434 | 9b4bed3f394c |
child 11104 | f2024fed9f0c |
permissions | -rw-r--r-- |
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 Needham-Schroeder Shared-Key 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 NB-1 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 |