author | wenzelm |
Mon, 28 Aug 2000 14:09:33 +0200 | |
changeset 9697 | c5fc121c2067 |
parent 6295 | 351b3c2b0d83 |
child 10064 | 1a77667b21ef |
permissions | -rw-r--r-- |
5430 | 1 |
(* Title: HOL/Auth/NSP_Bad |
2 |
ID: $Id$ |
|
3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
4 |
Copyright 1996 University of Cambridge |
|
5 |
||
6216 | 6 |
add_path "../Auth"; use_thy"NSP_Bad"; |
5430 | 7 |
|
8 |
Security protocols in UNITY: Needham-Schroeder, public keys (flawed version). |
|
9 |
||
10 |
Original file is ../Auth/NS_Public_Bad |
|
11 |
*) |
|
12 |
||
13 |
NSP_Bad = Public + Constrains + |
|
14 |
||
15 |
types state = event list |
|
16 |
||
17 |
constdefs |
|
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 :: "(state*state) set" |
|
23 |
"Fake == {(s,s'). |
|
24 |
EX B X. s' = Says Spy B X # s |
|
5460 | 25 |
& X: synth (analz (spies s))}" |
5430 | 26 |
|
27 |
(*The numeric suffixes on A identify the rule*) |
|
28 |
||
29 |
(*Alice initiates a protocol run, sending a nonce to Bob*) |
|
30 |
NS1 :: "(state*state) set" |
|
31 |
"NS1 == {(s1,s'). |
|
32 |
EX A1 B NA. |
|
33 |
s' = Says A1 B (Crypt (pubK B) {|Nonce NA, Agent A1|}) # s1 |
|
5460 | 34 |
& Nonce NA ~: used s1}" |
5430 | 35 |
|
36 |
(*Bob responds to Alice's message with a further nonce*) |
|
37 |
NS2 :: "(state*state) set" |
|
38 |
"NS2 == {(s2,s'). |
|
39 |
EX A' A2 B NA NB. |
|
40 |
s' = Says B A2 (Crypt (pubK A2) {|Nonce NA, Nonce NB|}) # s2 |
|
41 |
& Says A' B (Crypt (pubK B) {|Nonce NA, Agent A2|}) : set s2 |
|
5460 | 42 |
& Nonce NB ~: used s2}" |
5430 | 43 |
|
44 |
(*Alice proves her existence by sending NB back to Bob.*) |
|
45 |
NS3 :: "(state*state) set" |
|
46 |
"NS3 == {(s3,s'). |
|
47 |
EX A3 B' B NA NB. |
|
48 |
s' = Says A3 B (Crypt (pubK B) (Nonce NB)) # s3 |
|
49 |
& Says A3 B (Crypt (pubK B) {|Nonce NA, Agent A3|}) : set s3 |
|
50 |
& Says B' A3 (Crypt (pubK A3) {|Nonce NA, Nonce NB|}) : set s3}" |
|
51 |
||
52 |
||
53 |
||
54 |
constdefs |
|
55 |
Nprg :: state program |
|
56 |
(*Initial trace is empty*) |
|
6295
351b3c2b0d83
removed the infernal States, eqStates, compatible, etc.
paulson
parents:
6216
diff
changeset
|
57 |
"Nprg == mk_program({[]}, {Fake, NS1, NS2, NS3})" |
5430 | 58 |
|
59 |
end |