author  nipkow 
Fri, 24 Nov 2000 16:49:27 +0100  
changeset 10519  ade64af4c57c 
parent 6335  7e4bffaa2a3e 
child 11185  1b737b4c2108 
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 

3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3481
diff
changeset

15 
consts yahalom :: event list set 
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3481
diff
changeset

16 
inductive "yahalom" 
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*) 
3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3481
diff
changeset

19 
Nil "[]: yahalom" 
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.*) 
6335  24 
Fake "[ evs: yahalom; X: synth (analz (knows Spy evs)) ] 
3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3481
diff
changeset

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

26 

6335  27 
(*A message that has been sent can be received by the 
28 
intended recipient.*) 

29 
Reception "[ evsr: yahalom; Says A B X : set evsr ] 

30 
==> Gets B X # evsr : yahalom" 

31 

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

32 
(*Alice initiates a protocol run*) 
5434
9b4bed3f394c
Got rid of not_Says_to_self and most uses of ~= in definitions and theorems
paulson
parents:
5359
diff
changeset

33 
YM1 "[ evs1: yahalom; Nonce NA ~: used evs1 ] 
3659
eddedfe2f3f8
Renamed "evs" to "evs1", "evs2", etc. in protocol inductive definition
paulson
parents:
3519
diff
changeset

34 
==> Says A B {Agent A, Nonce NA} # evs1 : yahalom" 
1985
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

35 

6335  36 
(*Bob's response to Alice's message.*) 
5434
9b4bed3f394c
Got rid of not_Says_to_self and most uses of ~= in definitions and theorems
paulson
parents:
5359
diff
changeset

37 
YM2 "[ evs2: yahalom; Nonce NB ~: used evs2; 
6335  38 
Gets B {Agent A, Nonce NA} : set evs2 ] 
1985
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

39 
==> Says B Server 
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

40 
{Agent B, Crypt (shrK B) {Agent A, Nonce NA, Nonce NB}} 
3659
eddedfe2f3f8
Renamed "evs" to "evs1", "evs2", etc. in protocol inductive definition
paulson
parents:
3519
diff
changeset

41 
# evs2 : yahalom" 
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.*) 
5434
9b4bed3f394c
Got rid of not_Says_to_self and most uses of ~= in definitions and theorems
paulson
parents:
5359
diff
changeset

45 
YM3 "[ evs3: yahalom; Key KAB ~: used evs3; 
6335  46 
Gets 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}} 
3659
eddedfe2f3f8
Renamed "evs" to "evs1", "evs2", etc. in protocol inductive definition
paulson
parents:
3519
diff
changeset

48 
: set evs3 ] 
1995  49 
==> Says Server A 
3447
c7c8c0db05b9
Defines KeyWithNonce, which is used to prove the secrecy of NB
paulson
parents:
2516
diff
changeset

50 
{Crypt (shrK A) {Agent B, Key KAB, Nonce NA, Nonce NB}, 
c7c8c0db05b9
Defines KeyWithNonce, which is used to prove the secrecy of NB
paulson
parents:
2516
diff
changeset

51 
Crypt (shrK B) {Agent A, Key KAB}} 
3659
eddedfe2f3f8
Renamed "evs" to "evs1", "evs2", etc. in protocol inductive definition
paulson
parents:
3519
diff
changeset

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

53 

1995  54 
(*Alice receives the Server's (?) message, checks her Nonce, and 
3961  55 
uses the new session key to send Bob his Nonce. The premise 
5434
9b4bed3f394c
Got rid of not_Says_to_self and most uses of ~= in definitions and theorems
paulson
parents:
5359
diff
changeset

56 
A ~= Server is needed to prove Says_Server_not_range.*) 
9b4bed3f394c
Got rid of not_Says_to_self and most uses of ~= in definitions and theorems
paulson
parents:
5359
diff
changeset

57 
YM4 "[ evs4: yahalom; A ~= Server; 
6335  58 
Gets A {Crypt(shrK A) {Agent B, Key K, Nonce NA, Nonce NB}, X} 
59 
: set evs4; 

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

60 
Says A B {Agent A, Nonce NA} : set evs4 ] 
eddedfe2f3f8
Renamed "evs" to "evs1", "evs2", etc. in protocol inductive definition
paulson
parents:
3519
diff
changeset

61 
==> Says A B {X, Crypt K (Nonce NB)} # evs4 : yahalom" 
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.*) 

5359  66 
Oops "[ evso: yahalom; 
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}, 
3659
eddedfe2f3f8
Renamed "evs" to "evs1", "evs2", etc. in protocol inductive definition
paulson
parents:
3519
diff
changeset

69 
X} : set evso ] 
4537
4e835bd9fada
Expressed most Oops rules using Notes instead of Says, and other tidying
paulson
parents:
3961
diff
changeset

70 
==> Notes Spy {Nonce NA, Nonce NB, Key K} # evso : yahalom" 
2110  71 

3447
c7c8c0db05b9
Defines KeyWithNonce, which is used to prove the secrecy of NB
paulson
parents:
2516
diff
changeset

72 

c7c8c0db05b9
Defines KeyWithNonce, which is used to prove the secrecy of NB
paulson
parents:
2516
diff
changeset

73 
constdefs 
c7c8c0db05b9
Defines KeyWithNonce, which is used to prove the secrecy of NB
paulson
parents:
2516
diff
changeset

74 
KeyWithNonce :: [key, nat, event list] => bool 
c7c8c0db05b9
Defines KeyWithNonce, which is used to prove the secrecy of NB
paulson
parents:
2516
diff
changeset

75 
"KeyWithNonce K NB evs == 
c7c8c0db05b9
Defines KeyWithNonce, which is used to prove the secrecy of NB
paulson
parents:
2516
diff
changeset

76 
EX A B na X. 
c7c8c0db05b9
Defines KeyWithNonce, which is used to prove the secrecy of NB
paulson
parents:
2516
diff
changeset

77 
Says Server A {Crypt (shrK A) {Agent B, Key K, na, Nonce NB}, X} 
3465  78 
: set evs" 
3447
c7c8c0db05b9
Defines KeyWithNonce, which is used to prove the secrecy of NB
paulson
parents:
2516
diff
changeset

79 

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

80 
end 