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 
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. 

2538  7 
Version incorporating Lowe's fix (inclusion of B's identity in round 2). 
2318  8 
*) 
9 

10 
NS_Public = Public + 

11 

3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3466
diff
changeset

12 
consts ns_public :: event list set 
2549  13 

2318  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.*) 

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

22 
Fake "[ evs: ns_public; X: synth (analz (spies evs)) ] 
2318  23 
==> Says Spy B X # evs : ns_public" 
24 

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

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

28 
# evs1 : ns_public" 
2318  29 

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

31 
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

32 
Says A' B (Crypt (pubK B) {Nonce NA, Agent A}) : set evs2 ] 
2497  33 
==> Says B A (Crypt (pubK A) {Nonce NA, Nonce NB, Agent B}) 
3659
eddedfe2f3f8
Renamed "evs" to "evs1", "evs2", etc. in protocol inductive definition
paulson
parents:
3541
diff
changeset

34 
# evs2 : ns_public" 
2318  35 

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

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

38 
Says A B (Crypt (pubK B) {Nonce NA, Agent A}) : set evs3; 
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2497
diff
changeset

39 
Says B' A (Crypt (pubK A) {Nonce NA, Nonce NB, Agent B}) 
3659
eddedfe2f3f8
Renamed "evs" to "evs1", "evs2", etc. in protocol inductive definition
paulson
parents:
3541
diff
changeset

40 
: set evs3 ] 
eddedfe2f3f8
Renamed "evs" to "evs1", "evs2", etc. in protocol inductive definition
paulson
parents:
3541
diff
changeset

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

43 
(**Oops message??**) 

44 

45 
end 