author  paulson 
Thu, 18 Sep 1997 13:24:04 +0200  
changeset 3683  aafe719dff14 
parent 3659  eddedfe2f3f8 
child 5434  9b4bed3f394c 
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 

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

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

27 
all similar protocols.*) 

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

28 
Fake "[ evs: woolam; B ~= Spy; 
3683  29 
X: synth (analz (spies evs)) ] 
2283
68829cf138fc
Swapping arguments of Crypt; removing argument lost
paulson
parents:
2274
diff
changeset

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

32 
(*Alice initiates a protocol run*) 

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

33 
WL1 "[ evs1: woolam; A ~= B ] 
eddedfe2f3f8
Renamed "evs" to "evs1", "evs2", etc. in protocol inductive definition
paulson
parents:
3519
diff
changeset

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

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

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

37 
WL2 "[ evs2: woolam; A ~= B; 
eddedfe2f3f8
Renamed "evs" to "evs1", "evs2", etc. in protocol inductive definition
paulson
parents:
3519
diff
changeset

38 
Says A' B (Agent A) : set evs2 ] 
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!*) 
3659
eddedfe2f3f8
Renamed "evs" to "evs1", "evs2", etc. in protocol inductive definition
paulson
parents:
3519
diff
changeset

53 
WL4 "[ evs4: woolam; B ~= Server; 
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.*) 

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

59 
WL5 "[ evs5: woolam; B ~= Server; 
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 