equal
deleted
inserted
replaced
8 |
8 |
9 theory KerberosIV_Gets imports Public begin |
9 theory KerberosIV_Gets imports Public begin |
10 |
10 |
11 text{*The "u" prefix indicates theorems referring to an updated version of the protocol. The "r" suffix indicates theorems where the confidentiality assumptions are relaxed by the corresponding arguments.*} |
11 text{*The "u" prefix indicates theorems referring to an updated version of the protocol. The "r" suffix indicates theorems where the confidentiality assumptions are relaxed by the corresponding arguments.*} |
12 |
12 |
13 syntax |
13 abbreviation |
14 Kas :: agent |
14 Kas :: agent |
15 Tgs :: agent --{*the two servers are translations...*} |
15 "Kas == Server" |
16 |
16 |
17 |
17 Tgs :: agent |
18 translations |
18 "Tgs == Friend 0" |
19 "Kas" == "Server " |
|
20 "Tgs" == "Friend 0" |
|
21 |
19 |
22 |
20 |
23 axioms |
21 axioms |
24 Tgs_not_bad [iff]: "Tgs \<notin> bad" |
22 Tgs_not_bad [iff]: "Tgs \<notin> bad" |
25 --{*Tgs is secure --- we already know that Kas is secure*} |
23 --{*Tgs is secure --- we already know that Kas is secure*} |
26 |
|
27 (*The current time is just the length of the trace!*) |
|
28 syntax |
|
29 CT :: "event list=>nat" |
|
30 |
|
31 expiredAK :: "[nat, event list] => bool" |
|
32 |
|
33 expiredSK :: "[nat, event list] => bool" |
|
34 |
|
35 expiredA :: "[nat, event list] => bool" |
|
36 |
|
37 valid :: "[nat, nat] => bool" ("valid _ wrt _") |
|
38 |
|
39 |
24 |
40 constdefs |
25 constdefs |
41 (* authKeys are those contained in an authTicket *) |
26 (* authKeys are those contained in an authTicket *) |
42 authKeys :: "event list => key set" |
27 authKeys :: "event list => key set" |
43 "authKeys evs == {authK. \<exists>A Peer Ta. Says Kas A |
28 "authKeys evs == {authK. \<exists>A Peer Ta. Says Kas A |
78 |
63 |
79 specification (replylife) |
64 specification (replylife) |
80 replylife_LB [iff]: "Suc 0 \<le> replylife" |
65 replylife_LB [iff]: "Suc 0 \<le> replylife" |
81 by blast |
66 by blast |
82 |
67 |
83 translations |
68 abbreviation |
84 "CT" == "length " |
69 (*The current time is just the length of the trace!*) |
85 |
70 CT :: "event list=>nat" |
86 "expiredAK Ta evs" == "authKlife + Ta < CT evs" |
71 "CT == length" |
87 |
72 |
88 "expiredSK Ts evs" == "servKlife + Ts < CT evs" |
73 expiredAK :: "[nat, event list] => bool" |
89 |
74 "expiredAK Ta evs == authKlife + Ta < CT evs" |
90 "expiredA T evs" == "authlife + T < CT evs" |
75 |
91 |
76 expiredSK :: "[nat, event list] => bool" |
92 "valid T1 wrt T2" == "T1 <= replylife + T2" |
77 "expiredSK Ts evs == servKlife + Ts < CT evs" |
|
78 |
|
79 expiredA :: "[nat, event list] => bool" |
|
80 "expiredA T evs == authlife + T < CT evs" |
|
81 |
|
82 valid :: "[nat, nat] => bool" ("valid _ wrt _") |
|
83 "valid T1 wrt T2 == T1 <= replylife + T2" |
93 |
84 |
94 (*---------------------------------------------------------------------*) |
85 (*---------------------------------------------------------------------*) |
95 |
86 |
96 |
87 |
97 (* Predicate formalising the association between authKeys and servKeys *) |
88 (* Predicate formalising the association between authKeys and servKeys *) |