author | paulson |
Fri, 19 Jun 1998 10:34:33 +0200 | |
changeset 5053 | 75d20f367e94 |
parent 3683 | aafe719dff14 |
child 5434 | 9b4bed3f394c |
permissions | -rw-r--r-- |
2318 | 1 |
(* Title: HOL/Auth/NS_Public_Bad |
2 |
ID: $Id$ |
|
3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
4 |
Copyright 1996 University of Cambridge |
|
5 |
||
6 |
Inductive relation "ns_public" for the Needham-Schroeder Public-Key protocol. |
|
7 |
Flawed version, vulnerable to Lowe's attack. |
|
8 |
||
9 |
From page 260 of |
|
10 |
Burrows, Abadi and Needham. A Logic of Authentication. |
|
11 |
Proc. Royal Soc. 426 (1989) |
|
12 |
*) |
|
13 |
||
14 |
NS_Public_Bad = Public + |
|
15 |
||
3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3465
diff
changeset
|
16 |
consts ns_public :: event list set |
2549 | 17 |
|
2318 | 18 |
inductive ns_public |
19 |
intrs |
|
20 |
(*Initial trace is empty*) |
|
21 |
Nil "[]: ns_public" |
|
22 |
||
23 |
(*The spy MAY say anything he CAN say. We do not expect him to |
|
24 |
invent new nonces here, but he can also use NS1. Common to |
|
25 |
all similar protocols.*) |
|
26 |
Fake "[| evs: ns_public; B ~= Spy; |
|
3683 | 27 |
X: synth (analz (spies evs)) |] |
2318 | 28 |
==> Says Spy B X # evs : ns_public" |
29 |
||
30 |
(*Alice initiates a protocol run, sending a nonce to Bob*) |
|
3659
eddedfe2f3f8
Renamed "evs" to "evs1", "evs2", etc. in protocol inductive definition
paulson
parents:
3541
diff
changeset
|
31 |
NS1 "[| evs1: ns_public; A ~= B; Nonce NA ~: used evs1 |] |
2497 | 32 |
==> Says A B (Crypt (pubK B) {|Nonce NA, Agent A|}) |
3659
eddedfe2f3f8
Renamed "evs" to "evs1", "evs2", etc. in protocol inductive definition
paulson
parents:
3541
diff
changeset
|
33 |
# evs1 : ns_public" |
2318 | 34 |
|
35 |
(*Bob responds to Alice's message with a further nonce*) |
|
3659
eddedfe2f3f8
Renamed "evs" to "evs1", "evs2", etc. in protocol inductive definition
paulson
parents:
3541
diff
changeset
|
36 |
NS2 "[| evs2: ns_public; A ~= B; Nonce NB ~: used evs2; |
eddedfe2f3f8
Renamed "evs" to "evs1", "evs2", etc. in protocol inductive definition
paulson
parents:
3541
diff
changeset
|
37 |
Says A' B (Crypt (pubK B) {|Nonce NA, Agent A|}) : set evs2 |] |
2497 | 38 |
==> Says B A (Crypt (pubK A) {|Nonce NA, Nonce NB|}) |
3659
eddedfe2f3f8
Renamed "evs" to "evs1", "evs2", etc. in protocol inductive definition
paulson
parents:
3541
diff
changeset
|
39 |
# evs2 : ns_public" |
2318 | 40 |
|
41 |
(*Alice proves her existence by sending NB back to Bob.*) |
|
3659
eddedfe2f3f8
Renamed "evs" to "evs1", "evs2", etc. in protocol inductive definition
paulson
parents:
3541
diff
changeset
|
42 |
NS3 "[| evs3: ns_public; |
eddedfe2f3f8
Renamed "evs" to "evs1", "evs2", etc. in protocol inductive definition
paulson
parents:
3541
diff
changeset
|
43 |
Says A B (Crypt (pubK B) {|Nonce NA, Agent A|}) : set evs3; |
eddedfe2f3f8
Renamed "evs" to "evs1", "evs2", etc. in protocol inductive definition
paulson
parents:
3541
diff
changeset
|
44 |
Says B' A (Crypt (pubK A) {|Nonce NA, Nonce NB|}) : set evs3 |] |
eddedfe2f3f8
Renamed "evs" to "evs1", "evs2", etc. in protocol inductive definition
paulson
parents:
3541
diff
changeset
|
45 |
==> Says A B (Crypt (pubK B) (Nonce NB)) # evs3 : ns_public" |
2318 | 46 |
|
47 |
(**Oops message??**) |
|
48 |
||
49 |
end |