author  nipkow 
Fri, 24 Nov 2000 16:49:27 +0100  
changeset 10519  ade64af4c57c 
parent 5434  9b4bed3f394c 
child 11185  1b737b4c2108 
permissions  rwrr 
2274  1 
(* Title: HOL/Auth/WooLam 
2 
ID: $Id$ 

3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 

4 
Copyright 1996 University of Cambridge 

5 

6 
Inductive relation "woolam" for the WooLam protocol. 

7 

8 
Simplified version from page 11 of 

9 
Abadi and Needham. Prudent Engineering Practice for Cryptographic Protocols. 

10 
IEEE Trans. S.E. 22(1), 1996, pages 615. 

11 

12 
Note: this differs from the WooLam protocol discussed by Lowe in his paper 

13 
Some New Attacks upon Security Protocols. 

14 
Computer Security Foundations Workshop, 1996. 

15 
*) 

16 

17 
WooLam = Shared + 

18 

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

19 
consts woolam :: event list set 
2283
68829cf138fc
Swapping arguments of Crypt; removing argument lost
paulson
parents:
2274
diff
changeset

20 
inductive woolam 
2274  21 
intrs 
22 
(*Initial trace is empty*) 

2283
68829cf138fc
Swapping arguments of Crypt; removing argument lost
paulson
parents:
2274
diff
changeset

23 
Nil "[]: woolam" 
2274  24 

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

25 
(** These rules allow agents to send messages to themselves **) 
9b4bed3f394c
Got rid of not_Says_to_self and most uses of ~= in definitions and theorems
paulson
parents:
3683
diff
changeset

26 

2274  27 
(*The spy MAY say anything he CAN say. We do not expect him to 
28 
invent new nonces here, but he can also use NS1. Common to 

29 
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

30 
Fake "[ evs: woolam; X: synth (analz (spies evs)) ] 
2283
68829cf138fc
Swapping arguments of Crypt; removing argument lost
paulson
parents:
2274
diff
changeset

31 
==> Says Spy B X # evs : woolam" 
2274  32 

33 
(*Alice initiates a protocol run*) 

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

34 
WL1 "[ evs1: woolam ] 
3659
eddedfe2f3f8
Renamed "evs" to "evs1", "evs2", etc. in protocol inductive definition
paulson
parents:
3519
diff
changeset

35 
==> Says A B (Agent A) # evs1 : woolam" 
2274  36 

37 
(*Bob responds to Alice's message with a challenge.*) 

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

38 
WL2 "[ evs2: woolam; Says A' B (Agent A) : set evs2 ] 
3659
eddedfe2f3f8
Renamed "evs" to "evs1", "evs2", etc. in protocol inductive definition
paulson
parents:
3519
diff
changeset

39 
==> Says B A (Nonce NB) # evs2 : woolam" 
2274  40 

41 
(*Alice responds to Bob's challenge by encrypting NB with her key. 

42 
B is *not* properly determined  Alice essentially broadcasts 

43 
her reply.*) 

3659
eddedfe2f3f8
Renamed "evs" to "evs1", "evs2", etc. in protocol inductive definition
paulson
parents:
3519
diff
changeset

44 
WL3 "[ evs3: woolam; 
eddedfe2f3f8
Renamed "evs" to "evs1", "evs2", etc. in protocol inductive definition
paulson
parents:
3519
diff
changeset

45 
Says A B (Agent A) : set evs3; 
eddedfe2f3f8
Renamed "evs" to "evs1", "evs2", etc. in protocol inductive definition
paulson
parents:
3519
diff
changeset

46 
Says B' A (Nonce NB) : set evs3 ] 
eddedfe2f3f8
Renamed "evs" to "evs1", "evs2", etc. in protocol inductive definition
paulson
parents:
3519
diff
changeset

47 
==> Says A B (Crypt (shrK A) (Nonce NB)) # evs3 : woolam" 
2274  48 

3470  49 
(*Bob forwards Alice's response to the Server. NOTE: usually 
50 
the messages are shown in chronological order, for clarity. 

51 
But here, exchanging the two events would cause the lemma 

3683  52 
WL4_analz_spies to pick up the wrong assumption!*) 
5434
9b4bed3f394c
Got rid of not_Says_to_self and most uses of ~= in definitions and theorems
paulson
parents:
3683
diff
changeset

53 
WL4 "[ evs4: woolam; 
3659
eddedfe2f3f8
Renamed "evs" to "evs1", "evs2", etc. in protocol inductive definition
paulson
parents:
3519
diff
changeset

54 
Says A' B X : set evs4; 
eddedfe2f3f8
Renamed "evs" to "evs1", "evs2", etc. in protocol inductive definition
paulson
parents:
3519
diff
changeset

55 
Says A'' B (Agent A) : set evs4 ] 
eddedfe2f3f8
Renamed "evs" to "evs1", "evs2", etc. in protocol inductive definition
paulson
parents:
3519
diff
changeset

56 
==> Says B Server {Agent A, Agent B, X} # evs4 : woolam" 
2274  57 

58 
(*Server decrypts Alice's response for Bob.*) 

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

59 
WL5 "[ evs5: woolam; 
2283
68829cf138fc
Swapping arguments of Crypt; removing argument lost
paulson
parents:
2274
diff
changeset

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

61 
: set evs5 ] 
2283
68829cf138fc
Swapping arguments of Crypt; removing argument lost
paulson
parents:
2274
diff
changeset

62 
==> Says Server B (Crypt (shrK B) {Agent A, Nonce NB}) 
3659
eddedfe2f3f8
Renamed "evs" to "evs1", "evs2", etc. in protocol inductive definition
paulson
parents:
3519
diff
changeset

63 
# evs5 : woolam" 
2274  64 

65 
end 