From synchronous to interleaved: rethinking time and concurrency in protocol verification

Abstract

We introduce Timed Interleaved Interpreted Systems (TIIS), a dense-time agent-based formalism for modelling executions of timed security protocols under an interleaved discrete semantics. In TIIS, at most one global action is executed at a time—co-executed by all agents that share it, while all remaining components stutter—and time elapse is represented separately. Interleaving thus operates across distinct global actions rather than within a single synchronisation, which reflects asynchronous protocol behaviour more directly than joint-step semantics. We define the syntax and semantics of TIIS and focus on reachability-oriented timed security properties arising in protocol-execution models. We then present a translation from networks of timed automata to TIIS in an environment-owned-clocks normal form and prove that the resulting TIIS structure simulates the timed behaviour of the source network under explicit structural assumptions, and that under the same assumptions the translation preserves reachability in both directions. Finally, we propose a bounded model checking encoding for TIIS based on satisfiability modulo theories (SMT) that separates delay steps from discrete action steps, making the interleaving discipline explicit at the formula level; the encoding is sound and complete for each fixed bound. The approach is implemented within the broader BMC4TimeSec toolchain and evaluated on a large common benchmark corpus of multi-session timed protocol instances. The experiments show full agreement of verification outcomes across the aligned Timed Automata (TA), Timed Interpreted Systems (TIS), and TIIS backends. The timed-automata backend remains the strongest runtime baseline; TIIS is slower than TIS in aggregate runtime, but consistently reduces peak memory consumption, which we explain mechanically at the level of the SMT encoding.