Timed Interpreted Systems as a New Agent-Based Formalism for Verification of Timed Security Protocols
Source abstract
Abstract
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.
Source: crossref · Quality: baseline
Research context
OpenAlex topics: Advanced Authentication Protocols Security · Access Control and Trust · Formal Methods in Verification
SciVX discovery tags are terminology-based. OpenAlex topics are source-provided classifications.
Affiliations
Faculty of Design, SWPS University, Chodakowska 19/31, 03-815 Warsaw, Poland
Faculty of Mathematics and Computer Science, University of Warmia and Mazury, 10-710 Olsztyn, Poland
Department of Computer Science, Czestochowa University of Technology, Dabrowskiego 73, 42-200 Czestochowa, Poland
Department of Mathematics and Computer Science, Jan Dlugosz University in Czestochowa, Armii Krajowej 13/15, 42-200 Czestochowa, Poland
Institute of Computer Science, Cardinal St. Wyszynski University, Woycickiego 1/3, 01-938 Warsaw, Poland
References (62)
Show source-provided references
1. Lowe, G. (1996). Breaking and Fixing the Needham-Schroeder Public-Key Protocol Using FDR. Tools and Algorithms for the Construction and Analysis of Systems: Second International Workshop, TACAS ’96, Passau, Germany, 27–29 March 1996, Proceedings, Springer.10.1007/3-540-61042-1_43 ↗
2. A Logic of Authentication10.1145/77648.77649 ↗
3. Dojen, R., Jurcut, A., Coffey, T., and Gyorodi, C. (2008). On Establishing and Fixing a Parallel Session Attack in a Security Protocol. Intelligent Distributed Computing, Systems and Applications: Proceedings of the 2nd International Symposium on Intelligent Distributed Computing (IDC 2008), Catania, Italy, 18–19 September 2008, Springer.
4. Checking EMTLK Properties of Timed Interpreted Systems via Bounded Model Checking
5. Automatic verification of temporal-epistemic properties of cryptographic protocols10.3166/jancl.19.463-487 ↗
6. Leustean, I., and Macovei, B. (2021, January 7–10). DELP: Dynamic Epistemic Logic for Security Protocols. Proceedings of the 23rd International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, SYNASC 2021, Timisoara, Romania.10.1109/SYNASC54541.2021.00053 ↗
7. Kurkowski, M., and Penczek, W. (2016). Applying Timed Automata to Model Checking of Security Protocols. Handbook of Finite State Based Models and Applications, Taylor & Francis Group.
8. Backes, M., Dreier, J., Kremer, S., and Künnemann, R. (2017, January 26–28). A Novel Approach for Reasoning about Liveness in Cryptographic Protocols and Its Application to Fair Exchange. Proceedings of the 2017 IEEE European Symposium on Security and Privacy (EuroS&P), Paris, France.10.1109/EuroSP.2017.12 ↗
9. Dynamic Fault-Tolerant Clock Synchronization10.1145/200836.200870 ↗
10. A Theory of Timed Automata10.1016/0304-3975(94)90010-8 ↗
11. Halpern, J.Y., van der Meyden, R., and Pucella, R. (2017, January 24–26). An Epistemic Foundation for Authentication Logics (Extended Abstract). Proceedings of the 16 Conference on Theoretical Aspects of Rationality and Knowledge (TARK 2017), Liverpool, UK.
12. Partial Order Reductions for Model Checking Temporal-epistemic Logics over Interleaved Multi-agent Systems10.3233/FI-2010-276 ↗
13. Evaluating Temporal Robustness of Mobile Networks10.1109/TMC.2011.248 ↗
14. Cheval, V., and Cortier, V. (2015, January 11–18). Timing Attacks in Security Protocols: Symbolic Framework and Proof Techniques. Verification of Security Protocols. Proceedings of the Principles of Security and Trust—4th International Conference, POST 2015, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015, London, UK.10.1007/978-3-662-46666-7_15 ↗
15. Simulation of Security Protocols based on Scenarios of Attacks10.3233/FI-2009-0096 ↗
16. Discrete vs. Dense Times in the Analysis of Cyber-Physical Security Protocols10.1007/978-3-662-46666-7_14 ↗
17. Basin, D.A., Cremers, C., and Meadows, C.A. (2018). Model Checking Security Protocols. Handbook of Model Checking, Springer.10.1007/978-3-319-10575-8_22 ↗
18. Biere, A., Cimatti, A., Clarke, E.M., Fujita, M., and Zhu, Y. (1999, January 21–25). Symbolic Model Checking Using SAT Procedures instead of BDDs. Proceedings of the 36th Conference on Design Automation, New Orleans, LA, USA.10.1145/309847.309942 ↗
19. Verification of the TESLA protocol in MCMAS-X
20. Symbolically analyzing security protocols using tamarin10.1145/3157831.3157835 ↗
21. Hess, A.V., and Mödersheim, S. (2017, January 21–25). Formalizing and Proving a Typing Result for Security Protocols in Isabelle/HOL. Proceedings of the 30th IEEE Computer Security Foundations Symposium, CSF 2017, Santa Barbara, CA, USA.10.1109/CSF.2017.27 ↗
22. Constraint differentiation: Search-space reduction for the constraint-based analysis of security protocols10.3233/JCS-2009-0351 ↗
23. SATMC: A SAT-based model checker for security protocols, business processes, and security APIs10.1007/s10009-015-0385-y ↗
24. A Formal Specification and Verification Framework for Timed Security Protocols10.1109/TSE.2017.2712621 ↗
25. TPMC: A Model Checker For Time–Sensitive Security Protocols10.4304/jcp.4.5.366-377 ↗
26. Zbrzezny, A.M., Zbrzezny, A., Siedlecka-Lamch, O., Szymoniak, S., and Kurkowski, M. (2020, January 9–13). VerSecTis—An agent based model checker for security protocols. Proceedings of the 19th International Conference on Autonomous Agents and Multiagent Systems (AAMAS 2020), Auckland, New Zealand.
27. LDYIS: A Framework for Model Checking Security Protocols
28. Boureanu, I., Cohen, M., and Lomuscio, A. (2010, January 10–14). Model checking detectability of attacks in multiagent systems. Proceedings of the 9th International Conference on Autonomous Agents and Multiagent Systems (AAMAS 2010), Toronto, ON, Canada.
29. Boureanu, I., Jones, A.V., and Lomuscio, A. (2012, January 4–8). Automatic verification of epistemic specifications under convergent equational theories. Proceedings of the 11th International Conference on Autonomous Agents and Multiagent Systems (AAMAS ’12), Valencia, Spain.
30. Millen, J.K. (1996, January 17–20). CAPSL: Common Authentication Protocol Specification Language. Proceedings of the 1996 Workshop on New Security Paradigms, Lake Arrowhead, CA, USA.10.1145/304851.304879 ↗
31. Boureanu, I., Kouvaros, P., and Lomuscio, A. (2016, January 9–13). Verifying Security Properties in Unbounded Multiagent Systems. Proceedings of the 2016 International Conference on Autonomous Agents & Multiagent Systems (AAMAS ’16), Singapore.
32. Timed analysis of security protocols10.3233/JCS-2007-15603 ↗
33. Modelling and Checking Timed Authentication of Security Protocols
34. Zbrzezny, A.M., Szymoniak, S., and Kurkowski, M. (2019, January 13–15). Efficient Verification of Security Protocols Time Properties Using SMT Solvers. Proceedings of the International Joint Conference: 12th International Conference on Computational Intelligence in Security for Information Systems (CISIS 2019) and 10th International Conference on EUropean Transnational Education (ICEUTE 2019), Seville, Spain. Proceedings.
35. Automated Verification of Timed Security Protocols with Clock Drift
36. Runtime verification of self-adaptive multi-agent system using probabilistic timed automata10.3233/JIFS-232397 ↗
37. Sankur, O. (2023). Timed Automata Verification and Synthesis via Finite Automata Learning. Tools and Algorithms for the Construction and Analysis of Systems: 29th International Conference, TACAS 2023, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2023, Paris, France, 22–27 April 2023, Proceedings, Part II, Springer.
38. Barthe, G., Lago, U.D., Malavolta, G., and Rakotonirina, I. (2022, January 7–11). Tidy: Symbolic Verification of Timed Cryptographic Protocols. Proceedings of the 2022 ACM SIGSAC Conference on Computer and Communications Security, Los Angeles, CA, USA.10.1145/3548606.3559343 ↗
39. Dormancy-aware timed branching bisimilarity with an application to communication protocol analysis10.1016/j.tcs.2024.114681 ↗
40. Sahu, P. (2023). Automated Verification for Real-Time Systems. Tools and Algorithms for the Construction and Analysis of Systems: 29th International Conference, TACAS 2023, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2023, Paris, France, 22–27 April 2023, Proceedings, Part I, Springer.
41. Fagin, R., Halpern, J.Y., Moses, Y., and Vardi, M.Y. (1995). Reasoning About Knowledge, MIT Press.10.7551/mitpress/5803.001.0001 ↗
42. Wooldridge, M. (2009). An Introduction to Multi-Agent Systems, John Wiley & Sons. [2nd ed.].
43. Deontic Interpreted Systems10.1023/A:1026176900459 ↗
44. Woźna-Szcześniak, B. (2013). SAT-Based Bounded Model Checking for Weighted Deontic Interpreted Systems. Progress in Artificial Intelligence: 16th Portuguese Conference on Artificial Intelligence, EPIA 2013, Angra do Heroísmo, Azores, Portugal, 9–12 September 2013, Proceedings, Springer.
45. BDD-versus SAT-based bounded model checking for the existential fragment of linear temporal logic with knowledge: Algorithms and their performance10.1007/s10458-013-9232-2 ↗
46. Using Encryption for Authentication in Large Networks of Computers10.1145/359657.359659 ↗
47. An Attack on the Needham-Schroeder Public-Key Authentication Protocol10.1016/0020-0190(95)00144-2 ↗
48. Baier, C., and Katoen, J.P. (2008). Principles of Model Checking, MIT Press.
49. Checking WECTLK Properties of Timed Real-Weighted Interpreted Systems via SMT-based Bounded Model Checking
50. Z3: An Efficient SMT solver
51. Yices 2.2
52. CVC410.1007/978-3-642-22110-1_14 ↗
53. Man-in-the-Middle Attack to the HTTPS Protocol10.1109/MSP.2009.12 ↗
54. Timestamps in Key Distribution Protocols10.1145/358722.358740 ↗
55. A Lesson on Authentication Protocol Design10.1145/182110.182113 ↗
56. Integrating security in a large distributed system10.1145/65000.65002 ↗
57. Lowe, G. (1996, January 10–12). Some new attacks upon security protocols. Proceedings of the 9th IEEE Computer Security Foundations Workshop, Kenmare, Ireland.
58. Siedlecka-Lamch, O., El Fray, I., Kurkowski, M., and Pejas, J. (2015). Verification of Mutual Authentication Protocol for MobInfoSec System. Computer Information Systems and Industrial Management: Proceedings of the 14th IFIP TC 8 International Conference, CISIM 2015, Warsaw, Poland, 24–26 September 2015, Springer.
59. A comparison of SMT-solvers for timed weighted interpreted systems10.16926/m.2016.21.15 ↗
60. Abadi, M., Blanchet, B., and Fournet, C. (2017). The Applied Pi Calculus: Mobile Values, New Names, and Secure Communication. J. ACM, 65.10.1145/3127586 ↗
61. SMT-Based Parameter Synthesis for Parametric Timed Automata10.1007/978-3-319-30165-5_1 ↗
62. André, É., Knapik, M., Penczek, W., and Petrucci, L. (2016, January 19–24). Controlling Actions and Time in Parametric Timed Automata. Proceedings of the 16th International Conference on Application of Concurrency to System Design, ACSD 2016, Torun, Poland.10.1109/ACSD.2016.20 ↗