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 |
|
|
16 |
consts lost :: agent set (*No need for it to be a variable*)
|
|
17 |
ns_public :: event list set
|
|
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;
|
|
27 |
X: synth (analz (sees lost Spy evs)) |]
|
|
28 |
==> Says Spy B X # evs : ns_public"
|
|
29 |
|
|
30 |
(*Alice initiates a protocol run, sending a nonce to Bob*)
|
|
31 |
NS1 "[| evs: ns_public; A ~= B |]
|
|
32 |
==> Says A B (Crypt (pubK B) {|Nonce (newN evs), Agent A|}) # evs
|
|
33 |
: ns_public"
|
|
34 |
|
|
35 |
(*Bob responds to Alice's message with a further nonce*)
|
|
36 |
NS2 "[| evs: ns_public; A ~= B;
|
|
37 |
Says A' B (Crypt (pubK B) {|Nonce NA, Agent A|})
|
|
38 |
: set_of_list evs |]
|
|
39 |
==> Says B A (Crypt (pubK A) {|Nonce NA, Nonce (newN evs)|}) # evs
|
|
40 |
: ns_public"
|
|
41 |
|
|
42 |
(*Alice proves her existence by sending NB back to Bob.*)
|
|
43 |
NS3 "[| evs: ns_public; A ~= B;
|
|
44 |
Says B' A (Crypt (pubK A) {|Nonce NA, Nonce NB|})
|
|
45 |
: set_of_list evs;
|
|
46 |
Says A B (Crypt (pubK B) {|Nonce NA, Agent A|})
|
|
47 |
: set_of_list evs |]
|
|
48 |
==> Says A B (Crypt (pubK B) (Nonce NB)) # evs : ns_public"
|
|
49 |
|
|
50 |
(**Oops message??**)
|
|
51 |
|
|
52 |
rules
|
|
53 |
(*Spy has access to his own key for spoof messages*)
|
|
54 |
Spy_in_lost "Spy: lost"
|
|
55 |
|
|
56 |
end
|