equal
deleted
inserted
replaced
38 authlife_LB [iff]: "2 \<le> authlife" |
38 authlife_LB [iff]: "2 \<le> authlife" |
39 by blast |
39 by blast |
40 |
40 |
41 |
41 |
42 abbreviation |
42 abbreviation |
43 CT :: "event list=>nat" |
43 CT :: "event list=>nat" where |
44 "CT == length" |
44 "CT == length" |
45 |
45 |
46 expiredK :: "[nat, event list] => bool" |
46 abbreviation |
|
47 expiredK :: "[nat, event list] => bool" where |
47 "expiredK T evs == sesKlife + T < CT evs" |
48 "expiredK T evs == sesKlife + T < CT evs" |
48 |
49 |
49 expiredA :: "[nat, event list] => bool" |
50 abbreviation |
|
51 expiredA :: "[nat, event list] => bool" where |
50 "expiredA T evs == authlife + T < CT evs" |
52 "expiredA T evs == authlife + T < CT evs" |
51 |
53 |
52 |
54 |
53 constdefs |
55 constdefs |
54 (* Yields the subtrace of a given trace from its beginning to a given event *) |
56 (* Yields the subtrace of a given trace from its beginning to a given event *) |