author | nipkow |
Thu, 26 Jun 1997 13:20:50 +0200 | |
changeset 3465 | e85c24717cad |
parent 2516 | 4d68fbe6378b |
child 3519 | ab0a9fbed4c0 |
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 |
||
2378 | 15 |
consts ns_shared :: agent set => event list set |
2032 | 16 |
inductive "ns_shared lost" |
1934 | 17 |
intrs |
18 |
(*Initial trace is empty*) |
|
2032 | 19 |
Nil "[]: ns_shared lost" |
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.*) |
|
2032 | 24 |
Fake "[| evs: ns_shared lost; B ~= Spy; |
25 |
X: synth (analz (sees lost Spy evs)) |] |
|
26 |
==> Says Spy B X # evs : ns_shared lost" |
|
1934 | 27 |
|
1965 | 28 |
(*Alice initiates a protocol run, requesting to talk to any B*) |
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset
|
29 |
NS1 "[| evs: ns_shared lost; A ~= Server; Nonce NA ~: used evs |] |
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset
|
30 |
==> Says A Server {|Agent A, Agent B, Nonce NA|} # evs |
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset
|
31 |
: ns_shared lost" |
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.*) |
|
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset
|
37 |
NS2 "[| evs: ns_shared lost; A ~= B; A ~= Server; Key KAB ~: used evs; |
3465 | 38 |
Says A' Server {|Agent A, Agent B, Nonce NA|} : set evs |] |
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|})|}) |
2284
80ebd1a213fd
Swapped arguments of Crypt (for clarity and because it is conventional)
paulson
parents:
2131
diff
changeset
|
43 |
# evs : ns_shared lost" |
1934 | 44 |
|
45 |
(*We can't assume S=Server. Agent A "remembers" her nonce. |
|
1997 | 46 |
Can inductively show A ~= Server*) |
2032 | 47 |
NS3 "[| evs: ns_shared lost; 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|}) |
3465 | 49 |
: set evs; |
50 |
Says A Server {|Agent A, Agent B, Nonce NA|} : set evs |] |
|
2032 | 51 |
==> Says A B X # evs : ns_shared lost" |
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.*) |
|
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset
|
55 |
NS4 "[| evs: ns_shared lost; A ~= B; Nonce NB ~: used evs; |
3465 | 56 |
Says A' B (Crypt (shrK B) {|Key K, Agent A|}) : set evs |] |
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset
|
57 |
==> Says B A (Crypt K (Nonce NB)) # evs |
2451
ce85a2aafc7a
Extensive tidying and simplification, largely stemming from
paulson
parents:
2378
diff
changeset
|
58 |
: ns_shared lost" |
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 NB-1 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.*) |
|
2032 | 65 |
NS5 "[| evs: ns_shared lost; A ~= B; |
3465 | 66 |
Says B' A (Crypt K (Nonce NB)) : set evs; |
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|}) |
3465 | 68 |
: set evs |] |
2284
80ebd1a213fd
Swapped arguments of Crypt (for clarity and because it is conventional)
paulson
parents:
2131
diff
changeset
|
69 |
==> Says A B (Crypt K {|Nonce NB, Nonce NB|}) # evs : ns_shared lost" |
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.*) |
|
74 |
Oops "[| evs: ns_shared lost; A ~= Spy; |
|
3465 | 75 |
Says B A (Crypt K (Nonce NB)) : set evs; |
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|}) |
3465 | 77 |
: set evs |] |
2069 | 78 |
==> Says A Spy {|Nonce NA, Nonce NB, Key K|} # evs : ns_shared lost" |
1934 | 79 |
|
80 |
end |