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

StatusVoR
Simple item page
dc.abstract.enWe 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.
dc.affiliationKatedra Informatyki
dc.affiliationWydział Projektowania w Warszawie
dc.contributor.authorZbrzezny, Agnieszka
dc.date.access2026-10-30
dc.date.accessioned2026-10-30T07:51:41Z
dc.date.available2026-10-30T07:51:41Z
dc.date.created2026-10-29
dc.date.issued2026-12
dc.description.abstract<jats:title>Abstract</jats:title> <jats:p>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.</jats:p>
dc.description.accesstimeat_publication
dc.description.issue6
dc.description.physical1-34
dc.description.sdgIndustryInnovationAndInfrastructure
dc.description.versionfinal_published
dc.description.volume34
dc.identifier.doi10.1093/jigpal/jzag054
dc.identifier.eissn1368-9894
dc.identifier.issn1367-0751
dc.identifier.urihttps://share.swps.edu.pl/handle/swps/2705
dc.identifier.weblinkhttps://academic.oup.com/jigpal/article-abstract/34/6/jzag054/9004242?redirectedFrom=fulltext
dc.languageen
dc.pbn.affiliationinformatyka
dc.rightsClosedAccess
dc.rights.explanationzamknięty dostęp
dc.rights.questionNo_rights
dc.share.articleOTHER
dc.subject.enfor mal verif ication
dc.subject.entimed security protocols
dc.subject.eninterleaving semantics
dc.subject.entimed inter preted systems
dc.subject.enSMT-based bounded model checking
dc.swps.sciencecloudsend
dc.titleFrom synchronous to interleaved: rethinking time and concurrency in protocol verification
dc.title.journalLogic Journal of the IGPL
dc.typeJournalArticle
dspace.entity.typeArticle