author  nipkow 
Fri, 24 Nov 2000 16:49:27 +0100  
changeset 10519  ade64af4c57c 
parent 5434  9b4bed3f394c 
child 11185  1b737b4c2108 
permissions  rwrr 
5053  1 
(* Title: HOL/Auth/Kerberos_BAN 
2 
ID: $Id$ 

3 
Author: Giampaolo Bella, Cambridge University Computer Laboratory 

4 
Copyright 1998 University of Cambridge 

5 

6 
The Kerberos protocol, BAN version. 

7 

8 
From page 251 of 

9 
Burrows, Abadi and Needham. A Logic of Authentication. 

10 
Proc. Royal Soc. 426 (1989) 

11 
*) 

12 

13 
Kerberos_BAN = Shared + 

14 

15 
(* Temporal modelization: session keys can be leaked 

16 
ONLY when they have expired *) 

17 

18 
syntax 

19 
CT :: event list=>nat 

20 
Expired :: [nat, event list] => bool 

21 
RecentAuth :: [nat, event list] => bool 

22 

23 
consts 

24 

25 
(*Duration of the session key*) 

26 
SesKeyLife :: nat 

27 

28 
(*Duration of the authenticator*) 

29 
AutLife :: nat 

30 

31 
rules 

32 
(*The ticket should remain fresh for two journeys on the network at least*) 

33 
SesKeyLife_LB "2 <= SesKeyLife" 

34 

35 
(*The authenticator only for one journey*) 

36 
AutLife_LB "1 <= AutLife" 

37 

38 
translations 

39 
"CT" == "length" 

40 

41 
"Expired T evs" == "SesKeyLife + T < CT evs" 

42 

43 
"RecentAuth T evs" == "CT evs <= AutLife + T" 

44 

45 
consts kerberos_ban :: event list set 

46 
inductive "kerberos_ban" 

47 
intrs 

48 

49 
Nil "[]: kerberos_ban" 

50 

5434
9b4bed3f394c
Got rid of not_Says_to_self and most uses of ~= in definitions and theorems
paulson
parents:
5053
diff
changeset

51 
Fake "[ evs: kerberos_ban; X: synth (analz (spies evs)) ] 
5053  52 
==> Says Spy B X # evs : kerberos_ban" 
53 

54 

5434
9b4bed3f394c
Got rid of not_Says_to_self and most uses of ~= in definitions and theorems
paulson
parents:
5053
diff
changeset

55 
Kb1 "[ evs1: kerberos_ban ] 
5053  56 
==> Says A Server {Agent A, Agent B} # evs1 
57 
: kerberos_ban" 

58 

59 

5434
9b4bed3f394c
Got rid of not_Says_to_self and most uses of ~= in definitions and theorems
paulson
parents:
5053
diff
changeset

60 
Kb2 "[ evs2: kerberos_ban; Key KAB ~: used evs2; 
5053  61 
Says A' Server {Agent A, Agent B} : set evs2 ] 
62 
==> Says Server A 

63 
(Crypt (shrK A) 

64 
{Number (CT evs2), Agent B, Key KAB, 

65 
(Crypt (shrK B) {Number (CT evs2), Agent A, Key KAB})}) 

66 
# evs2 : kerberos_ban" 

67 

68 

5434
9b4bed3f394c
Got rid of not_Says_to_self and most uses of ~= in definitions and theorems
paulson
parents:
5053
diff
changeset

69 
Kb3 "[ evs3: kerberos_ban; 
5053  70 
Says S A (Crypt (shrK A) {Number Ts, Agent B, Key K, X}) 
71 
: set evs3; 

72 
Says A Server {Agent A, Agent B} : set evs3; 

73 
~ Expired Ts evs3 ] 

74 
==> Says A B {X, Crypt K {Agent A, Number (CT evs3)} } 

75 
# evs3 : kerberos_ban" 

76 

77 

5434
9b4bed3f394c
Got rid of not_Says_to_self and most uses of ~= in definitions and theorems
paulson
parents:
5053
diff
changeset

78 
Kb4 "[ evs4: kerberos_ban; 
5053  79 
Says A' B {(Crypt (shrK B) {Number Ts, Agent A, Key K}), 
80 
(Crypt K {Agent A, Number Ta}) }: set evs4; 

5434
9b4bed3f394c
Got rid of not_Says_to_self and most uses of ~= in definitions and theorems
paulson
parents:
5053
diff
changeset

81 
~ Expired Ts evs4; RecentAuth Ta evs4 ] 
5053  82 
==> Says B A (Crypt K (Number Ta)) # evs4 
83 
: kerberos_ban" 

84 

5434
9b4bed3f394c
Got rid of not_Says_to_self and most uses of ~= in definitions and theorems
paulson
parents:
5053
diff
changeset

85 
(*Old session keys may become compromised*) 
9b4bed3f394c
Got rid of not_Says_to_self and most uses of ~= in definitions and theorems
paulson
parents:
5053
diff
changeset

86 
Oops "[ evso: kerberos_ban; 
5053  87 
Says Server A (Crypt (shrK A) {Number Ts, Agent B, Key K, X}) 
88 
: set evso; 

89 
Expired Ts evso ] 

5434
9b4bed3f394c
Got rid of not_Says_to_self and most uses of ~= in definitions and theorems
paulson
parents:
5053
diff
changeset

90 
==> Notes Spy {Number Ts, Key K} # evso : kerberos_ban" 
5053  91 

92 

93 
end 