author  paulson 
Fri, 11 Jul 1997 13:26:15 +0200  
changeset 3512  9dcb4daa15e8 
parent 3481  256f38c01b98 
child 3519  ab0a9fbed4c0 
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.*) 

2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

38 
WL2 "[ evs: woolam; A ~= B; 
3465  39 
Says A' B (Agent A) : set evs ] 
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

40 
==> Says B A (Nonce NB) # 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.*) 

3481
256f38c01b98
Deleted a redundant A~=B in rules that refer to a previous event
paulson
parents:
3470
diff
changeset

45 
WL3 "[ evs: woolam; 
3465  46 
Says A B (Agent A) : set evs; 
47 
Says B' A (Nonce NB) : set 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 

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

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

53 
WL4_analz_sees_Spy to pick up the wrong assumption!*) 

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

54 
WL4 "[ evs: woolam; B ~= Server; 
3465  55 
Says A' B X : set evs; 
56 
Says A'' B (Agent A) : set evs ] 

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

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

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

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

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

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

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

64 
# evs : woolam" 
2274  65 

66 
end 