author  paulson 
Thu, 12 Sep 1996 10:40:05 +0200  
changeset 1985  84cf16192e03 
child 1995  c80e58e78d9c 
permissions  rwrr 
1985
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

1 
(* Title: HOL/Auth/OtwayRees 
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

2 
ID: $Id$ 
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

4 
Copyright 1996 University of Cambridge 
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

5 

84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

6 
Inductive relation "yahalom" for the Yahalom protocol. 
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

7 

84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

8 
From page 257 of 
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

9 
Burrows, Abadi and Needham. A Logic of Authentication. 
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

10 
Proc. Royal Soc. 426 (1989) 
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

11 
*) 
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

12 

84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

13 
OtwayRees = Shared + 
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

14 

84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

15 
consts yahalom :: "event list set" 
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

16 
inductive yahalom 
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

17 
intrs 
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

18 
(*Initial trace is empty*) 
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

19 
Nil "[]: yahalom" 
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

20 

84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

21 
(*The enemy MAY say anything he CAN say. We do not expect him to 
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

22 
invent new nonces here, but he can also use NS1. Common to 
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

23 
all similar protocols.*) 
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

24 
Fake "[ evs: yahalom; B ~= Enemy; X: synth (analz (sees Enemy evs)) ] 
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

25 
==> Says Enemy B X # evs : yahalom" 
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

26 

84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

27 
(*Alice initiates a protocol run*) 
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

28 
YM1 "[ evs: yahalom; A ~= B ] 
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

29 
==> Says A B {Nonce (newN evs), Agent A } # evs : yahalom" 
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

30 

84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

31 
(*Bob's response to Alice's message. Bob doesn't know who 
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

32 
the sender is, hence the A' in the sender field. 
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

33 
We modify the published protocol by NOT encrypting NB.*) 
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

34 
YM2 "[ evs: yahalom; B ~= Server; 
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

35 
Says A' B {Nonce NA, Agent A} : set_of_list evs ] 
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

36 
==> Says B Server 
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

37 
{Agent B, 
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

38 
Crypt {Agent A, Nonce NA, Nonce (newN evs)} (shrK B)} 
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

39 
# evs : yahalom" 
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

40 

84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

41 
(*The Server receives Bob's message. He responds by sending a 
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

42 
new session key to Alice, with a packet for forwarding to Bob.*) 
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

43 
YM3 "[ evs: yahalom; B ~= Server; 
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

44 
Says B' Server 
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

45 
{Nonce NA, Agent A, Agent B, 
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

46 
Crypt {Nonce NA, Agent A, Agent B} (shrK A), 
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

47 
Nonce NB, 
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

48 
Crypt {Nonce NA, Agent A, Agent B} (shrK B)} 
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

49 
: set_of_list evs ] 
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

50 
==> Says Server B 
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

51 
{Nonce NA, 
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

52 
Crypt {Nonce NA, Key (newK evs)} (shrK A), 
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

53 
Crypt {Nonce NB, Key (newK evs)} (shrK B)} 
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

54 
# evs : yahalom" 
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

55 

84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

56 
(*Bob receives the Server's (?) message and compares the Nonces with 
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

57 
those in the message he previously sent the Server.*) 
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

58 
YM4 "[ evs: yahalom; A ~= B; 
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

59 
Says S B {Nonce NA, X, Crypt {Nonce NB, Key K} (shrK B)} 
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

60 
: set_of_list evs; 
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

61 
Says B Server {Nonce NA, Agent A, Agent B, X', Nonce NB, X''} 
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

62 
: set_of_list evs ] 
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

63 
==> (Says B A {Nonce NA, X}) # evs : yahalom" 
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

64 

84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

65 
(*Alice checks her Nonce, then sends a dummy message to Bob, 
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

66 
using the new session key.*) 
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

67 
YM5 "[ evs: yahalom; 
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

68 
Says B' A {Nonce NA, Crypt {Nonce NA, Key K} (shrK A)} 
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

69 
: set_of_list evs; 
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

70 
Says A B {Nonce NA, Agent A, Agent B, X} : set_of_list evs ] 
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

71 
==> Says A B (Crypt (Agent A) K) # evs : yahalom" 
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

72 

84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

73 
end 