author  paulson 
Fri, 29 Nov 1996 17:58:18 +0100  
changeset 2283  68829cf138fc 
parent 2274  1b1b46adc9b3 
child 2451  ce85a2aafc7a 
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 

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

19 
consts lost :: agent set (*No need for it to be a variable*) 
68829cf138fc
Swapping arguments of Crypt; removing argument lost
paulson
parents:
2274
diff
changeset

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

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

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

24 
Nil "[]: woolam" 
2274  25 

26 
(*The spy MAY say anything he CAN say. We do not expect him to 

27 
invent new nonces here, but he can also use NS1. Common to 

28 
all similar protocols.*) 

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

29 
Fake "[ evs: woolam; B ~= Spy; 
2274  30 
X: synth (analz (sees lost Spy 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*) 

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

34 
WL1 "[ evs: woolam; A ~= B ] 
68829cf138fc
Swapping arguments of Crypt; removing argument lost
paulson
parents:
2274
diff
changeset

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

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

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

38 
WL2 "[ evs: woolam; A ~= B; 
2274  39 
Says A' B (Agent A) : set_of_list evs ] 
2283
68829cf138fc
Swapping arguments of Crypt; removing argument lost
paulson
parents:
2274
diff
changeset

40 
==> Says B A (Nonce (newN evs)) # evs : woolam" 
2274  41 

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

43 
B is *not* properly determined  Alice essentially broadcasts 

44 
her reply.*) 

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

45 
WL3 "[ evs: woolam; A ~= B; 
2274  46 
Says B' A (Nonce NB) : set_of_list evs; 
47 
Says A B (Agent A) : set_of_list evs ] 

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

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

50 
(*Bob forwards Alice's response to the Server.*) 

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

51 
WL4 "[ evs: woolam; B ~= Server; 
2274  52 
Says A' B X : set_of_list evs; 
53 
Says A'' B (Agent A) : set_of_list evs ] 

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

54 
==> Says B Server {Agent A, Agent B, X} # evs : woolam" 
2274  55 

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

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

57 
WL5 "[ evs: woolam; B ~= Server; 
68829cf138fc
Swapping arguments of Crypt; removing argument lost
paulson
parents:
2274
diff
changeset

58 
Says B' Server {Agent A, Agent B, Crypt (shrK A) (Nonce NB)} 
2274  59 
: set_of_list evs ] 
2283
68829cf138fc
Swapping arguments of Crypt; removing argument lost
paulson
parents:
2274
diff
changeset

60 
==> Says Server B (Crypt (shrK B) {Agent A, Nonce NB}) 
68829cf138fc
Swapping arguments of Crypt; removing argument lost
paulson
parents:
2274
diff
changeset

61 
# evs : woolam" 
2274  62 

63 
end 