From Timed Interpreted Systems to Split-Step Timed Interpreted Systems: Making Delivery Delay Explicit and Deciding Realizability in Security Protocol Verification
From Timed Interpreted Systems to Split-Step Timed Interpreted Systems: Making Delivery Delay Explicit and Deciding Realizability in Security Protocol Verification
StatusVoR
Alternative title
Authors
Zbrzezny, Agnieszka
Monograph
Monograph (alternative title)
Date
2026-09-30
Publisher
Journal title
IEEE Access
Issue
Volume
Pages
Pages
ISSN
2169-3536
ISSN of series
Access date
2026-09-30
Abstract PL
Abstract EN
Timed security protocols rely on freshness tokens whose validity must hold when a response is delivered, not merely when it is sent. Many models collapse sending and delivery into one event, erasing the transit interval in which a token may expire. This abstraction has a concrete consequence: a delay-oblivious model can report that successful completion is reachable for a protocol that, on any network with a positive minimum transit latency, can never complete – a soundness gap rather than a missed attack. We introduce Split-Step Timed Interpreted Systems (SSTIS), a dense-time semantics in which every step has three phases – send, transit, and deliver-or-fail – making the transit interval and a delivery failure explicit local states.We formalise interpretations into classical Timed Interpreted Systems (TIS) and into SSTIS, and prove three results: SSTIS conservatively extends TIS at zero delay; a delivery-time failure is reachable in SSTIS but unsatisfiable in TIS by construction; and under a minimum transit delay D, a step whose freshness window L satisfies D > L fails in every run, including the fastest adversary-free delivery, so the protocol is unrealizable. From this we derive a linear-time realizability decision procedure that decides whether a guarded step can ever succeed, as a static pre-check before bounded model checking. We give a quantifier-free linear-real-arithmetic encoding with soundness and completeness proofs, apply it to the MobInfoSec SP2SP_MutualAuth protocol and classical timestamp families, and report a feasibility study across 779 protocol-variant instances and 12,410 reachability queries solved in under a second at the median.
Abstract other
Keywords PL
Keywords EN
Bounded model checking
delivery delay
formal verification
freshness
realizability
security protocols
SMT
timed interpreted systems
delivery delay
formal verification
freshness
realizability
security protocols
SMT
timed interpreted systems
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
