From Timed Interpreted Systems to Split-Step Timed Interpreted Systems: Making Delivery Delay Explicit and Deciding Realizability in Security Protocol Verification

StatusVoR
Simple item page
dc.abstract.enTimed 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.
dc.affiliationKatedra Infromatyki, Wydział Projektowania
dc.affiliationWydział Projektowania w Warszawie
dc.contributor.authorZbrzezny, Agnieszka
dc.date.access2026-09-30
dc.date.accessioned2026-10-13T11:32:37Z
dc.date.available2026-10-13T11:32:37Z
dc.date.created2026-09-30
dc.date.issued2026-09-30
dc.description.accesstimeat_publication
dc.description.sdgIndustryInnovationAndInfrastructure
dc.description.versionfinal_published
dc.identifier.doi10.1109/ACCESS.2026.3738640
dc.identifier.issn2169-3536
dc.identifier.urihttps://share.swps.edu.pl/handle/swps/2609
dc.identifier.weblinkhttps://ieeexplore.ieee.org/document/11716583
dc.languageen
dc.pbn.affiliationinformatyka
dc.rightsCC-BY
dc.rights.questionYes_rights
dc.share.articleOPEN_JOURNAL
dc.subject.enBounded model checking
dc.subject.endelivery delay
dc.subject.enformal verification
dc.subject.enfreshness
dc.subject.enrealizability
dc.subject.ensecurity protocols
dc.subject.enSMT
dc.subject.entimed interpreted systems
dc.swps.sciencecloudnosend
dc.titleFrom Timed Interpreted Systems to Split-Step Timed Interpreted Systems: Making Delivery Delay Explicit and Deciding Realizability in Security Protocol Verification
dc.title.journalIEEE Access
dc.typeJournalArticle
dspace.entity.typeArticle