equal
deleted
inserted
replaced
15 very realistic - model. |
15 very realistic - model. |
16 *} |
16 *} |
17 |
17 |
18 (* Temporal modelization: session keys can be leaked |
18 (* Temporal modelization: session keys can be leaked |
19 ONLY when they have expired *) |
19 ONLY when they have expired *) |
20 |
|
21 syntax |
|
22 CT :: "event list=>nat" |
|
23 expiredK :: "[nat, event list] => bool" |
|
24 expiredA :: "[nat, event list] => bool" |
|
25 |
20 |
26 consts |
21 consts |
27 |
22 |
28 (*Duration of the session key*) |
23 (*Duration of the session key*) |
29 sesKlife :: nat |
24 sesKlife :: nat |
42 specification (authlife) |
37 specification (authlife) |
43 authlife_LB [iff]: "2 \<le> authlife" |
38 authlife_LB [iff]: "2 \<le> authlife" |
44 by blast |
39 by blast |
45 |
40 |
46 |
41 |
47 translations |
42 abbreviation |
48 "CT" == "length " |
43 CT :: "event list=>nat" |
49 |
44 "CT == length" |
50 "expiredK T evs" == "sesKlife + T < CT evs" |
45 |
51 |
46 expiredK :: "[nat, event list] => bool" |
52 "expiredA T evs" == "authlife + T < CT evs" |
47 "expiredK T evs == sesKlife + T < CT evs" |
|
48 |
|
49 expiredA :: "[nat, event list] => bool" |
|
50 "expiredA T evs == authlife + T < CT evs" |
53 |
51 |
54 |
52 |
55 constdefs |
53 constdefs |
56 (* Yields the subtrace of a given trace from its beginning to a given event *) |
54 (* Yields the subtrace of a given trace from its beginning to a given event *) |
57 before :: "[event, event list] => event list" ("before _ on _") |
55 before :: "[event, event list] => event list" ("before _ on _") |