Timed Interpreted Systems as a New Agent-Based Formalism for Verification of Timed Security Protocols
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 in...
Saved in:
| Main Authors: | , , , , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
MDPI AG
2024-11-01
|
| Series: | Applied Sciences |
| Subjects: | |
| Online Access: | https://www.mdpi.com/2076-3417/14/22/10333 |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1846154571961860096 |
|---|---|
| author | Agnieszka M. Zbrzezny Olga Siedlecka-Lamch Sabina Szymoniak Andrzej Zbrzezny Mirosław Kurkowski |
| author_facet | Agnieszka M. Zbrzezny Olga Siedlecka-Lamch Sabina Szymoniak Andrzej Zbrzezny Mirosław Kurkowski |
| author_sort | Agnieszka M. Zbrzezny |
| collection | DOAJ |
| description | 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. |
| format | Article |
| id | doaj-art-d26158a578204b63a90c016325d3a07e |
| institution | Kabale University |
| issn | 2076-3417 |
| language | English |
| publishDate | 2024-11-01 |
| publisher | MDPI AG |
| record_format | Article |
| series | Applied Sciences |
| spelling | doaj-art-d26158a578204b63a90c016325d3a07e2024-11-26T17:48:21ZengMDPI AGApplied Sciences2076-34172024-11-0114221033310.3390/app142210333Timed Interpreted Systems as a New Agent-Based Formalism for Verification of Timed Security ProtocolsAgnieszka M. Zbrzezny0Olga Siedlecka-Lamch1Sabina Szymoniak2Andrzej Zbrzezny3Mirosław Kurkowski4Faculty of Design, SWPS University, Chodakowska 19/31, 03-815 Warsaw, PolandDepartment of Computer Science, Czestochowa University of Technology, Dabrowskiego 73, 42-200 Czestochowa, PolandDepartment of Computer Science, Czestochowa University of Technology, Dabrowskiego 73, 42-200 Czestochowa, PolandDepartment of Mathematics and Computer Science, Jan Dlugosz University in Czestochowa, Armii Krajowej 13/15, 42-200 Czestochowa, PolandInstitute of Computer Science, Cardinal St. Wyszynski University, Woycickiego 1/3, 01-938 Warsaw, PolandThis 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.https://www.mdpi.com/2076-3417/14/22/10333timed security protocolsmulti-agent systemstimed interpreted systemsbounded model checkingsatisfiability modulo theories |
| spellingShingle | Agnieszka M. Zbrzezny Olga Siedlecka-Lamch Sabina Szymoniak Andrzej Zbrzezny Mirosław Kurkowski Timed Interpreted Systems as a New Agent-Based Formalism for Verification of Timed Security Protocols Applied Sciences timed security protocols multi-agent systems timed interpreted systems bounded model checking satisfiability modulo theories |
| title | Timed Interpreted Systems as a New Agent-Based Formalism for Verification of Timed Security Protocols |
| title_full | Timed Interpreted Systems as a New Agent-Based Formalism for Verification of Timed Security Protocols |
| title_fullStr | Timed Interpreted Systems as a New Agent-Based Formalism for Verification of Timed Security Protocols |
| title_full_unstemmed | Timed Interpreted Systems as a New Agent-Based Formalism for Verification of Timed Security Protocols |
| title_short | Timed Interpreted Systems as a New Agent-Based Formalism for Verification of Timed Security Protocols |
| title_sort | timed interpreted systems as a new agent based formalism for verification of timed security protocols |
| topic | timed security protocols multi-agent systems timed interpreted systems bounded model checking satisfiability modulo theories |
| url | https://www.mdpi.com/2076-3417/14/22/10333 |
| work_keys_str_mv | AT agnieszkamzbrzezny timedinterpretedsystemsasanewagentbasedformalismforverificationoftimedsecurityprotocols AT olgasiedleckalamch timedinterpretedsystemsasanewagentbasedformalismforverificationoftimedsecurityprotocols AT sabinaszymoniak timedinterpretedsystemsasanewagentbasedformalismforverificationoftimedsecurityprotocols AT andrzejzbrzezny timedinterpretedsystemsasanewagentbasedformalismforverificationoftimedsecurityprotocols AT mirosławkurkowski timedinterpretedsystemsasanewagentbasedformalismforverificationoftimedsecurityprotocols |