Seminarium Instytutu

Zapraszamy na seminarium w poniedziałek 28 kwietnia w godz. 12:10-13:00 w sali 3/40, bud. 34.  Dr  Agnieszka Małgorzata Zbrzezny , Uniwersytet Warmińsko-Mazurski w Olsztynie, wygłosi referat na temat „Weryfikacja protokołów bezpieczeństwa z czasem”.

Streszczenie
Podczas wystąpienia zostanie omówiony kompletny proces modelowania oraz weryfikacji czasowych protokołów bezpieczeństwa. Do modelowania protokołów zostaną użyte formalizmy czasowe jakimi są: automaty z czasem [1,2,3], czasowe systemy interpretowane [4,6] oraz przeplotowe czasowe systemy interpretowane, które zapewniają możliwość modelowania różnego rodzaju zależności czasowych. Następnie zostaną pokazane dwie bazowe techniki ograniczonej weryfikacji modelowej: bazująca na translacji do SAT oraz bazująca na translacji do SMT [4].

W drugiej części zostanie omówione jedno z autorskich narzędzi do weryfikacji protokołów bezpieczeństwa, VerSecTis [5,6], które umożliwia analizę zależności czasowych w protokołach i wykrywanie potencjalnych luk w ich bezpieczeństwie.

Wystąpienie zakończy podsumowanie dotychczasowych osiągnięć oraz perspektyw badawczych w obszarze weryfikacji modelowej systemów współbieżnych z uwzględnieniem czasu.

[1] Rajeev Alur, David L. Dill. A Theory of Timed Automata. Theoretical Computer Science, 126(2):183–235, 1994.

[2] Agnieszka M. Zbrzezny, Sabina Szymoniak, Miroslaw Kurkowski. Practical Approach in Verification of Security Systems Using Satisfiability Modulo Theories. Log. J. IGPL 30(2): 289-300 (2022).

[3] Sabina Szymoniak, Olga Siedlecka-Lamch, Agnieszka M. Zbrzezny, Andrzej Zbrzezny, Miroslaw Kurkowski. SAT and SMT-Based Verification of Security Protocols Including Time Aspects. Sensors 21(9): 3055 (2021)

[4] Bożena Woźna-Szcześniak. Checking EMTLK properties of timed interpreted systems via bounded model checking. Ana L. C. Bazzan, Michael N. Huhns, Alessio Lomuscio, Paul Scerri, redaktorzy, International conference on Autonomous Agents and Multi-Agent Systems, AAMAS ’14, Paris, France, May 5-9, 2014, strony 1477–1478. IFAAMAS/ACM, 2014.

[5] Agnieszka M. Zbrzezny, Andrzej Zbrzezny, Sabina Szymoniak, Olga Siedlecka-Lamch, Miroslaw Kurkowski. VerSecTis – an agent based model checker for security protocols. Amal El Fallah Seghrouchni, Gita Sukthankar, Bo An, Neil Yorke-Smith, redaktorzy, Proceedings of the 19th International Conference on Autonomous Agents and Multiagent Systems, AAMAS ’20, Auckland, New Zealand, May 9-13, 2020, strony 2123–2125. International Foundation for Autonomous Agents and Multiagent Systems, 2020.

[6] Agnieszka M. Zbrzezny., Olga Siedlecka-Lamch, Sabina Szymoniak, Andrzej Zbrzezny, Mirosław Kurkowski. 2024. „Timed Interpreted Systems as a New Agent-Based Formalism for Verification of Timed Security Protocols” Applied Sciences 14, no. 22: 10333. https://doi.org/10.3390/app142210333