Timed interpreted systems as a new agent-based formalism for verification of timed security protocols

StatusVoR
Simple item page
cris.lastimport.scopus2025-04-04T03:14:32Z
dc.abstract.enThis article introduces a new method for modelling and verifying the execution of timed security protocols (TSPs) and their time-dependent security properties. The method, which is novel and reliable, uses an extension of interpreted systems, accessible semantics in multi-agent systems, and timed interpreted systems (TISs) with dense time semantics to model TSP executions. We enhance the models of TSPs by incorporating delays and varying lifetimes to capture real-life aspects of protocol executions. To illustrate the method, we model a timed version of the Needham–Schroeder Public Key Authentication Protocol. We have also developed a new bounded model checking reachability algorithm for the proposed structures, based on Satisfiability Modulo Theories (SMTs), and implemented it within the tool. The method comprises a new procedure for modelling TSP executions, translating TSPs into TISs, and translating TISs’ reachability problem into the SMT problem. The paper also includes thorough experimental results for nine protocols modelled by TISs and discusses the findings in detail.
dc.affiliationKatedra Informatyki
dc.affiliationWydział Projektowania w Warszawie
dc.contributor.authorZbrzezny, Agnieszka
dc.contributor.authorSiedlecka-Lamch, Olga
dc.contributor.authorSzymoniak, Sabina
dc.contributor.authorZbrzezny, Andrzej
dc.contributor.authorKurkowski, Mirosław
dc.date.access2024-11-10
dc.date.accessioned2025-03-25T07:04:19Z
dc.date.available2025-03-25T07:04:19Z
dc.date.created2024-11-04
dc.date.issued2024-11-10
dc.description.abstract<jats:p>This article introduces a new method for modelling and verifying the execution of timed security protocols (TSPs) and their time-dependent security properties. The method, which is novel and reliable, uses an extension of interpreted systems, accessible semantics in multi-agent systems, and timed interpreted systems (TISs) with dense time semantics to model TSP executions. We enhance the models of TSPs by incorporating delays and varying lifetimes to capture real-life aspects of protocol executions. To illustrate the method, we model a timed version of the Needham–Schroeder Public Key Authentication Protocol. We have also developed a new bounded model checking reachability algorithm for the proposed structures, based on Satisfiability Modulo Theories (SMTs), and implemented it within the tool. The method comprises a new procedure for modelling TSP executions, translating TSPs into TISs, and translating TISs’ reachability problem into the SMT problem. The paper also includes thorough experimental results for nine protocols modelled by TISs and discusses the findings in detail.</jats:p>
dc.description.accesstimeat_publication
dc.description.issue22
dc.description.physical1-24
dc.description.versionfinal_published
dc.description.volume14
dc.identifier.doi10.3390/app142210333
dc.identifier.issn2076-3417
dc.identifier.urihttps://share.swps.edu.pl/handle/swps/1367
dc.identifier.weblinkhttps://www.mdpi.com/2076-3417/14/22/10333
dc.languageen
dc.pbn.affiliationinformatyka
dc.rightsCC-BY
dc.rights.questionYes_rights
dc.share.articleOPEN_JOURNAL
dc.subject.entimed security protocols
dc.subject.enmulti-agent systems
dc.subject.entimed interpreted systems
dc.subject.enbounded model checking
dc.subject.ensatisfiability modulo theories
dc.swps.sciencecloudsend
dc.titleTimed interpreted systems as a new agent-based formalism for verification of timed security protocols
dc.title.journalApplied Sciences
dc.typeJournalArticle
dspace.entity.typeArticle