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

StatusVoR
Dublin Core metadata
Alternative title
Authors
Zbrzezny, Agnieszka
Siedlecka-Lamch, Olga
Szymoniak, Sabina
Zbrzezny, Andrzej
Kurkowski, Mirosław
Monograph
Monograph (alternative title)
Date
2024-11-10
Publisher
Journal title
Applied Sciences
Issue
22
Volume
14
Pages
Pages
1-24
DOI
ISSN
2076-3417
ISSN of series
Weblink
https://www.mdpi.com/2076-3417/14/22/10333
Access date
2024-11-10
Abstract PL
Abstract EN
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.
Abstract other
Keywords PL
Keywords EN
timed security protocols
multi-agent systems
timed interpreted systems
bounded model checking
satisfiability modulo theories
Keywords other
Exhibition title
Place of exhibition (institution)
Exhibition curator
URI
https://share.swps.edu.pl/handle/swps/1367
Type
License type
cc-by
Except as otherwise noted, this item is licensed under the Attribution licence | Permitted use of copyrighted works
Funder
Time range from
Time range to
Contact person name
Related publication
Related publication
Grant/project name
Files
Timed Interpreted Systems as a New Agent-Based Formalism for Verification of Timed Security Protocols
Timed Interpreted Systems as a New Agent-Based Formalism for Verification of Timed Security Protocols(493.26 KB)
Download
Views
Views3
Acquisition Date4.04.2025
Downloads
Downloads1
Acquisition Date4.04.2025
Altmetrics©
Dimensions
Google Scholar
Google Scholar