author  paulson 
Mon, 14 Jul 1997 12:47:21 +0200  
changeset 3519  ab0a9fbed4c0 
parent 3481  256f38c01b98 
child 3659  eddedfe2f3f8 
permissions  rwrr 
3445  1 
(* Title: HOL/Auth/Yahalom2 
2111
81c8d46edfa3
New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff
changeset

2 
ID: $Id$ 
81c8d46edfa3
New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff
changeset

3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 
81c8d46edfa3
New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff
changeset

4 
Copyright 1996 University of Cambridge 
81c8d46edfa3
New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff
changeset

5 

81c8d46edfa3
New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff
changeset

6 
Inductive relation "yahalom" for the Yahalom protocol, Variant 2. 
81c8d46edfa3
New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff
changeset

7 

81c8d46edfa3
New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff
changeset

8 
This version trades encryption of NB for additional explicitness in YM3. 
3432  9 
Also in YM3, care is taken to make the two certificates distinct. 
2111
81c8d46edfa3
New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff
changeset

10 

81c8d46edfa3
New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff
changeset

11 
From page 259 of 
81c8d46edfa3
New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff
changeset

12 
Burrows, Abadi and Needham. A Logic of Authentication. 
81c8d46edfa3
New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff
changeset

13 
Proc. Royal Soc. 426 (1989) 
81c8d46edfa3
New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff
changeset

14 
*) 
81c8d46edfa3
New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff
changeset

15 

81c8d46edfa3
New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff
changeset

16 
Yahalom2 = Shared + 
81c8d46edfa3
New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff
changeset

17 

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

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

19 
inductive "yahalom" 
2111
81c8d46edfa3
New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff
changeset

20 
intrs 
81c8d46edfa3
New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff
changeset

21 
(*Initial trace is empty*) 
3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3481
diff
changeset

22 
Nil "[]: yahalom" 
2111
81c8d46edfa3
New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff
changeset

23 

81c8d46edfa3
New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff
changeset

24 
(*The spy MAY say anything he CAN say. We do not expect him to 
81c8d46edfa3
New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff
changeset

25 
invent new nonces here, but he can also use NS1. Common to 
81c8d46edfa3
New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff
changeset

26 
all similar protocols.*) 
3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3481
diff
changeset

27 
Fake "[ evs: yahalom; B ~= Spy; 
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3481
diff
changeset

28 
X: synth (analz (sees Spy evs)) ] 
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3481
diff
changeset

29 
==> Says Spy B X # evs : yahalom" 
2111
81c8d46edfa3
New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff
changeset

30 

81c8d46edfa3
New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff
changeset

31 
(*Alice initiates a protocol run*) 
3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3481
diff
changeset

32 
YM1 "[ evs: yahalom; A ~= B; Nonce NA ~: used evs ] 
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3481
diff
changeset

33 
==> Says A B {Agent A, Nonce NA} # evs : yahalom" 
2111
81c8d46edfa3
New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff
changeset

34 

81c8d46edfa3
New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff
changeset

35 
(*Bob's response to Alice's message. Bob doesn't know who 
81c8d46edfa3
New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff
changeset

36 
the sender is, hence the A' in the sender field.*) 
3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3481
diff
changeset

37 
YM2 "[ evs: yahalom; B ~= Server; Nonce NB ~: used evs; 
3465  38 
Says A' B {Agent A, Nonce NA} : set evs ] 
3432  39 
==> Says B Server 
40 
{Agent B, Nonce NB, Crypt (shrK B) {Agent A, Nonce NA}} 

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

41 
# evs : yahalom" 
2111
81c8d46edfa3
New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff
changeset

42 

81c8d46edfa3
New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff
changeset

43 
(*The Server receives Bob's message. He responds by sending a 
2155  44 
new session key to Alice, with a packet for forwarding to Bob. 
3432  45 
!! Fields are reversed in the 2nd packet to prevent attacks!! *) 
3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3481
diff
changeset

46 
YM3 "[ evs: yahalom; A ~= B; A ~= Server; Key KAB ~: used evs; 
3432  47 
Says B' Server {Agent B, Nonce NB, 
48 
Crypt (shrK B) {Agent A, Nonce NA}} 

3465  49 
: set evs ] 
2111
81c8d46edfa3
New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff
changeset

50 
==> Says Server A 
81c8d46edfa3
New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff
changeset

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

52 
Crypt (shrK A) {Agent B, Key KAB, Nonce NA}, 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

53 
Crypt (shrK B) {Nonce NB, Key KAB, Agent A}} 
3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3481
diff
changeset

54 
# evs : yahalom" 
2111
81c8d46edfa3
New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff
changeset

55 

81c8d46edfa3
New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff
changeset

56 
(*Alice receives the Server's (?) message, checks her Nonce, and 
81c8d46edfa3
New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff
changeset

57 
uses the new session key to send Bob his Nonce.*) 
3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3481
diff
changeset

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

59 
Says S A {Nonce NB, Crypt (shrK A) {Agent B, Key K, Nonce NA}, 
3466
30791e5a69c4
Corrected indentations and margins after the renaming of "set_of_list"
paulson
parents:
3465
diff
changeset

60 
X} : set evs; 
3465  61 
Says A B {Agent A, Nonce NA} : set evs ] 
3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3481
diff
changeset

62 
==> Says A B {X, Crypt K (Nonce NB)} # evs : yahalom" 
2111
81c8d46edfa3
New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff
changeset

63 

2155  64 
(*This message models possible leaks of session keys. The nonces 
65 
identify the protocol run. Quoting Server here ensures they are 

66 
correct. *) 

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

67 
Oops "[ evs: yahalom; A ~= Spy; 
2155  68 
Says Server A {Nonce NB, 
2284
80ebd1a213fd
Swapped arguments of Crypt (for clarity and because it is conventional)
paulson
parents:
2155
diff
changeset

69 
Crypt (shrK A) {Agent B, Key K, Nonce NA}, 
3465  70 
X} : set evs ] 
3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3481
diff
changeset

71 
==> Says A Spy {Nonce NA, Nonce NB, Key K} # evs : yahalom" 
2111
81c8d46edfa3
New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff
changeset

72 

81c8d46edfa3
New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff
changeset

73 
end 