From synchronous to interleaved: rethinking time and concurrency in protocol verification
From synchronous to interleaved: rethinking time and concurrency in protocol verification
StatusVoR
Alternative title
Authors
Zbrzezny, Agnieszka
Monograph
Monograph (alternative title)
Date
2026-12
Publisher
Journal title
Logic Journal of the IGPL
Issue
6
Volume
34
Pages
Pages
1-34
ISSN
1367-0751
ISSN of series
Access date
2026-10-30
Abstract PL
Abstract EN
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.
Abstract other
Keywords PL
Keywords EN
for mal verif ication
timed security protocols
interleaving semantics
timed inter preted systems
SMT-based bounded model checking
timed security protocols
interleaving semantics
timed inter preted systems
SMT-based bounded model checking
Keywords other
Sustainable Development Goals
Exhibition title
Place of exhibition (institution)
Exhibition curator
Type
License type
Funder
Time range from
Time range to
Contact person name
Related publication
Related publication
Grant/project name
Grant number
Collections
Views
0Acquisition Date20.10.2022
Downloads
0Acquisition Date20.10.2022
Altmetrics©
Dimensions
Google Scholar
