author  paulson 
Thu, 19 Dec 1996 11:58:39 +0100  
changeset 2451  ce85a2aafc7a 
parent 2378  fc103154ad8f 
child 2516  4d68fbe6378b 
permissions  rwrr 
1995  1 
(* Title: HOL/Auth/Yahalom 
1985
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 

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

14 

2378  15 
consts yahalom :: agent set => event list set 
2032  16 
inductive "yahalom lost" 
1985
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*) 
2032  19 
Nil "[]: yahalom lost" 
1985
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

20 

2032  21 
(*The spy MAY say anything he CAN say. We do not expect him to 
1985
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.*) 
2032  24 
Fake "[ evs: yahalom lost; B ~= Spy; 
25 
X: synth (analz (sees lost Spy evs)) ] 

26 
==> Says Spy B X # evs : yahalom lost" 

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

27 

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

28 
(*Alice initiates a protocol run*) 
2032  29 
YM1 "[ evs: yahalom lost; A ~= B ] 
2451
ce85a2aafc7a
Extensive tidying and simplification, largely stemming from
paulson
parents:
2378
diff
changeset

30 
==> Says A B {Agent A, Nonce (newN(length evs))} # evs 
ce85a2aafc7a
Extensive tidying and simplification, largely stemming from
paulson
parents:
2378
diff
changeset

31 
: yahalom lost" 
1985
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

32 

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

33 
(*Bob's response to Alice's message. Bob doesn't know who 
1995  34 
the sender is, hence the A' in the sender field.*) 
2032  35 
YM2 "[ evs: yahalom lost; B ~= Server; 
1995  36 
Says A' B {Agent A, Nonce NA} : set_of_list evs ] 
1985
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

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

38 
{Agent B, 
2451
ce85a2aafc7a
Extensive tidying and simplification, largely stemming from
paulson
parents:
2378
diff
changeset

39 
Crypt (shrK B) 
ce85a2aafc7a
Extensive tidying and simplification, largely stemming from
paulson
parents:
2378
diff
changeset

40 
{Agent A, Nonce NA, Nonce (newN(length evs))}} 
2032  41 
# evs : yahalom lost" 
1985
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

42 

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

43 
(*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

44 
new session key to Alice, with a packet for forwarding to Bob.*) 
2032  45 
YM3 "[ evs: yahalom lost; A ~= Server; 
1985
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

46 
Says B' Server 
2284
80ebd1a213fd
Swapped arguments of Crypt (for clarity and because it is conventional)
paulson
parents:
2156
diff
changeset

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

48 
: set_of_list evs ] 
1995  49 
==> Says Server A 
2451
ce85a2aafc7a
Extensive tidying and simplification, largely stemming from
paulson
parents:
2378
diff
changeset

50 
{Crypt (shrK A) {Agent B, Key (newK(length evs)), 
2284
80ebd1a213fd
Swapped arguments of Crypt (for clarity and because it is conventional)
paulson
parents:
2156
diff
changeset

51 
Nonce NA, Nonce NB}, 
2451
ce85a2aafc7a
Extensive tidying and simplification, largely stemming from
paulson
parents:
2378
diff
changeset

52 
Crypt (shrK B) {Agent A, Key (newK(length evs))}} 
2032  53 
# evs : yahalom lost" 
1985
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

54 

1995  55 
(*Alice receives the Server's (?) message, checks her Nonce, and 
56 
uses the new session key to send Bob his Nonce.*) 

2125  57 
YM4 "[ evs: yahalom lost; A ~= Server; A ~= B; 
2284
80ebd1a213fd
Swapped arguments of Crypt (for clarity and because it is conventional)
paulson
parents:
2156
diff
changeset

58 
Says S A {Crypt (shrK A) {Agent B, Key K, Nonce NA, Nonce NB}, 
2125  59 
X} : set_of_list evs; 
1995  60 
Says A B {Agent A, Nonce NA} : set_of_list evs ] 
2284
80ebd1a213fd
Swapped arguments of Crypt (for clarity and because it is conventional)
paulson
parents:
2156
diff
changeset

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

62 

2110  63 
(*This message models possible leaks of session keys. The Nonces 
2156  64 
identify the protocol run. Quoting Server here ensures they are 
65 
correct.*) 

2125  66 
Oops "[ evs: yahalom lost; A ~= Spy; 
2284
80ebd1a213fd
Swapped arguments of Crypt (for clarity and because it is conventional)
paulson
parents:
2156
diff
changeset

67 
Says Server A {Crypt (shrK A) 
80ebd1a213fd
Swapped arguments of Crypt (for clarity and because it is conventional)
paulson
parents:
2156
diff
changeset

68 
{Agent B, Key K, Nonce NA, Nonce NB}, 
2125  69 
X} : set_of_list evs ] 
2110  70 
==> Says A Spy {Nonce NA, Nonce NB, Key K} # evs : yahalom lost" 
71 

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

72 
end 