author | paulson |
Thu, 19 Dec 1996 11:58:39 +0100 | |
changeset 2451 | ce85a2aafc7a |
parent 2318 | 6d3f7c7f70b0 |
child 2497 | 47de509bdd55 |
permissions | -rw-r--r-- |
2318 | 1 |
(* Title: HOL/Auth/NS_Public |
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 |
Version incorporating Lowe's fix (inclusion of B's identify in round 2). |
|
8 |
*) |
|
9 |
||
10 |
NS_Public = Public + |
|
11 |
||
12 |
consts lost :: agent set (*No need for it to be a variable*) |
|
13 |
ns_public :: event list set |
|
14 |
inductive ns_public |
|
15 |
intrs |
|
16 |
(*Initial trace is empty*) |
|
17 |
Nil "[]: ns_public" |
|
18 |
||
19 |
(*The spy MAY say anything he CAN say. We do not expect him to |
|
20 |
invent new nonces here, but he can also use NS1. Common to |
|
21 |
all similar protocols.*) |
|
22 |
Fake "[| evs: ns_public; B ~= Spy; |
|
23 |
X: synth (analz (sees lost Spy evs)) |] |
|
24 |
==> Says Spy B X # evs : ns_public" |
|
25 |
||
26 |
(*Alice initiates a protocol run, sending a nonce to Bob*) |
|
27 |
NS1 "[| evs: ns_public; A ~= B |] |
|
2451
ce85a2aafc7a
Extensive tidying and simplification, largely stemming from
paulson
parents:
2318
diff
changeset
|
28 |
==> Says A B (Crypt (pubK B) {|Nonce (newN(length evs)), Agent A|}) |
ce85a2aafc7a
Extensive tidying and simplification, largely stemming from
paulson
parents:
2318
diff
changeset
|
29 |
# evs : ns_public" |
2318 | 30 |
|
31 |
(*Bob responds to Alice's message with a further nonce*) |
|
32 |
NS2 "[| evs: ns_public; A ~= B; |
|
33 |
Says A' B (Crypt (pubK B) {|Nonce NA, Agent A|}) |
|
34 |
: set_of_list evs |] |
|
2451
ce85a2aafc7a
Extensive tidying and simplification, largely stemming from
paulson
parents:
2318
diff
changeset
|
35 |
==> Says B A (Crypt (pubK A) {|Nonce NA, Nonce (newN(length evs)), |
ce85a2aafc7a
Extensive tidying and simplification, largely stemming from
paulson
parents:
2318
diff
changeset
|
36 |
Agent B|}) |
ce85a2aafc7a
Extensive tidying and simplification, largely stemming from
paulson
parents:
2318
diff
changeset
|
37 |
# evs : ns_public" |
2318 | 38 |
|
39 |
(*Alice proves her existence by sending NB back to Bob.*) |
|
40 |
NS3 "[| evs: ns_public; A ~= B; |
|
41 |
Says B' A (Crypt (pubK A) {|Nonce NA, Nonce NB, Agent B|}) |
|
42 |
: set_of_list evs; |
|
43 |
Says A B (Crypt (pubK B) {|Nonce NA, Agent A|}) |
|
44 |
: set_of_list evs |] |
|
45 |
==> Says A B (Crypt (pubK B) (Nonce NB)) # evs : ns_public" |
|
46 |
||
47 |
(**Oops message??**) |
|
48 |
||
49 |
rules |
|
50 |
(*Spy has access to his own key for spoof messages*) |
|
51 |
Spy_in_lost "Spy: lost" |
|
52 |
||
53 |
end |