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 "Suc 0 <= AutLife" |
36 AutLife_LB "Suc 0 <= AutLife" |
37 |
37 |
38 translations |
38 translations |