equal
deleted
inserted
replaced
28 (*Duration of the authenticator*) |
28 (*Duration of the authenticator*) |
29 AutLife :: nat |
29 AutLife :: nat |
30 |
30 |
31 rules |
31 rules |
32 (*The ticket should remain fresh for two journeys on the network at least*) |
32 (*The ticket should remain fresh for two journeys on the network at least*) |
33 SesKeyLife_LB "2 <= SesKeyLife" |
33 SesKeyLife_LB "#2 <= SesKeyLife" |
34 |
34 |
35 (*The authenticator only for one journey*) |
35 (*The authenticator only for one journey*) |
36 AutLife_LB "1 <= AutLife" |
36 AutLife_LB "1' <= AutLife" |
37 |
37 |
38 translations |
38 translations |
39 "CT" == "length" |
39 "CT" == "length" |
40 |
40 |
41 "Expired T evs" == "SesKeyLife + T < CT evs" |
41 "Expired T evs" == "SesKeyLife + T < CT evs" |