author  nipkow 
Fri, 24 Nov 2000 16:49:27 +0100  
changeset 10519  ade64af4c57c 
parent 5434  9b4bed3f394c 
child 11104  f2024fed9f0c 
permissions  rwrr 
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 NeedhamSchroeder PublicKey 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.*) 

5434
9b4bed3f394c
Got rid of not_Says_to_self and most uses of ~= in definitions and theorems
paulson
parents:
3683
diff
changeset

26 
Fake "[ evs: ns_public; X: synth (analz (spies evs)) ] 
2318  27 
==> Says Spy B X # evs : ns_public" 
28 

29 
(*Alice initiates a protocol run, sending a nonce to Bob*) 

5434
9b4bed3f394c
Got rid of not_Says_to_self and most uses of ~= in definitions and theorems
paulson
parents:
3683
diff
changeset

30 
NS1 "[ evs1: ns_public; Nonce NA ~: used evs1 ] 
2497  31 
==> 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

32 
# evs1 : ns_public" 
2318  33 

34 
(*Bob responds to Alice's message with a further nonce*) 

5434
9b4bed3f394c
Got rid of not_Says_to_self and most uses of ~= in definitions and theorems
paulson
parents:
3683
diff
changeset

35 
NS2 "[ evs2: ns_public; Nonce NB ~: used evs2; 
3659
eddedfe2f3f8
Renamed "evs" to "evs1", "evs2", etc. in protocol inductive definition
paulson
parents:
3541
diff
changeset

36 
Says A' B (Crypt (pubK B) {Nonce NA, Agent A}) : set evs2 ] 
2497  37 
==> 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

38 
# evs2 : ns_public" 
2318  39 

40 
(*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

41 
NS3 "[ evs3: ns_public; 
eddedfe2f3f8
Renamed "evs" to "evs1", "evs2", etc. in protocol inductive definition
paulson
parents:
3541
diff
changeset

42 
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

43 
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

44 
==> Says A B (Crypt (pubK B) (Nonce NB)) # evs3 : ns_public" 
2318  45 

46 
(**Oops message??**) 

47 

48 
end 