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 |
|
|
6 |
loadpath := "../Auth" :: !loadpath; use_thy"NSP_Bad";
|
|
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*)
|
5596
|
57 |
"Nprg == mk_program({[]}, {Fake, NS1, NS2, NS3})"
|
5430
|
58 |
|
|
59 |
end
|