Skip to main content
Fachgebiete
Automobil + Motoren Bauwesen + Immobilien Business IT + Informatik Elektrotechnik + Elektronik Energie + Nachhaltigkeit Finance + Banking Management + Führung Marketing + Vertrieb Maschinenbau + Werkstoffe Versicherung + Risiko
DE
EN
Bücher
Zeitschriften
Themenseiten
Organisationspsychologie Projektmanagement Marketing Smart Manufacturing
Weitere Formate
Podcasts Webinare Technik Webinare Wirtschaft Kongresse Veranstaltungskalender Awards
Jetzt Einzelzugang starten
Zugang für Unternehmen
Referenzkunden
SLX-Digitalkonferenz: Zukunftswerkstatt 2024

Mehr Umsatz mit Top-Kontakten

Am 7. Mai erfahren Sie, wie Vertriebsteams Leadgenerierung, Leadnurturing und Leadstrategien effizient steuern können.
Erweiterte Suche
Anmelden
nach oben
Erschienen in:
Artificial Intelligence Technology in Intelligent Health Informatics Kapitel lesen Erstes Kapitel lesen

2019 | OriginalPaper | Buchkapitel

Network’s Delays in Timed Analysis of Security Protocols

verfasst von : Sabina Szymoniak, Olga Siedlecka-Lamch, Mirosław Kurkowski

Erschienen in: Information Systems Architecture and Technology: Proceedings of 39th International Conference on Information Systems Architecture and Technology – ISAT 2018

Verlag: Springer International Publishing

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config
loading …

Abstract

For several years, the analysis of security protocols time properties has been very important in the area of computer networks security. Up to now, however, it has been primarily used for timestamps analysis, without the other time related parameters being taken into account. As we can see in literature using formal, mathematical structures many problems can be considered and solved. In order to present the assets and liabilities of the tested protocol, depending on the known time parameters, we have proposed a mathematical model.
For our research on security protocols time properties we use synchronized networks of timed automata – a specifically designed discrete mathematical model. This model allows to express and investigate the mentioned properties. In our work we also use encoding of structures and properties into Boolean propositional formulas that can be solved using SAT techniques. The investigation based on our model proved that even protocols which are potentially weak can be used with proper time constraints. In this paper we consider one of the popular security protocols: the WooLamPi protocol and its variations. By strengthening the crucial points, a way to improve protocol safety may also be found. Part of the work was to implement a tool which not only helps in the above mentioned activity, but also allows to display experimental results.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

  • über 102.000 Bücher
  • über 537 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Maschinenbau + Werkstoffe
  • Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 390 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Maschinenbau + Werkstoffe




 

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 340 Zeitschriften

aus folgenden Fachgebieten:

  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Versicherung + Risiko




Jetzt Wissensvorsprung sichern!

Jetzt informieren
Vorheriges Kapitel Concurrent, Coherent Design of Hardware and Software Embedded Systems with Higher Degree of Reliability and Fault Tolerant
Nächstes Kapitel Evaluation of an Impact of the DoS Attacks on the Selected Virtualization Platforms
Literatur
1.
Armando, A., Basin, D., Boichut, Y., Chevalier, Y., Compagna, L., Cuellar, J., et al.: The AVISPA tool for the automated validation of internet security protocols and applications. In: Proceedings of 17th International Conference on Computer Aided Verification (CAV 2005), vol. 3576. LNCS, pp. 281–285. Springer (2005)
2.
Blanchet, B.: Modeling and verifying security protocols with the applied pi calculus and ProVerif. Found. Trends Priv. Secur. 1(1–2), 1–135 (2016)
3.
4.
Cremers, C., Mauw, S.: Operational Semantics and Verification of Security Protocols. Information Security and Cryptography Series. Springer, Heidelberg (2012)CrossRef
5.
David, A., Larsen, K.G., et al.: Uppaal SMC tutorial. Int. J. Softw. Tools Technol. Transfer (STTT) 17(4), 397–415 (2015)
6.
7.
Jakubowska, G., Penczek, W.: Modeling and checking timed authentication security protocols. In: Proceedings of the International Workshop on Concurrency, Specification and Programming (CS&P 2006), Informatik-Berichte, vol. 206, no. 2, str. pp. 280–291. Humboldt University (2006)
8.
Jakubowska, G., Penczek, W.: Is your security protocol on time? In: Proceedings of FSEN’07. LNCS, vol. 4767, pp. 65–80. Springer (2007)
9.
Kacprzak, M., Nabiałek, W., Niewiadomski, A., Penczek, W., Półrola, A., Szreter, M., et al.: Verics 2007 - a model checker for knowledge and real-time. Fundamenta Informatiace 85, 313–328 (2008)
10.
Kurkowski, M., Penczek, W.: Applying timed automata to model checking of security protocols. In: Wang, J. (ed.) Handbook of Finite State Based Models and Applications, pp. 223–254. CRC Press, Boca Raton (2012)
11.
Kurkowski, M.: Formalne metody weryfikacji wlasnosci protokolow zabezpieczajacych w sieciach komputerowych, wyd. Exit, Warszawa (2013)
12.
Paulson, L.: Inductive analysis of the internet protocol TLS. ACM Trans. Inf. Syst. Secur. (TISSEC) 2(3), 332–351 (1999)CrossRef
13.
Penczek, W., Półrola, A.: Advances in Verification of Time Petri Nets and Timed Automata: Temporal Logic Approach. Studies in Computational Intelligence, vol. 20. Springer (2006)
14.
Szymoniak, S.: Modeling and verification of security protocols including delays in the network. Ph.D. thesis, Czestochowa University of Technology (2017)
15.
Siedlecka-Lamch, O., Kurkowski, M., Piatkowski, J.: Probabilistic model checking of security protocols without perfect cryptography assumption. In: Proceedings of 23rd International Conference, Computer Networks 2016, Brunow, Poland, 14–17 June 2016. Communications in Computer and Information Science, vol. 608, pp. 107–117. Springer (2016)
16.
Szymoniak, S., Siedlecka-Lamch, O., Kurkowski, M.: Timed analysis of security protocols. In: Proceedings of 37th International Conference ISAT 2016, Karpacz, Poland, 18–20 September 2017. Advances in Intelligent Systems and Computing, vol. 522, pp. 53–63. Springer (2017)
17.
Woo, T.Y.C., Lam, S.S.: A lesson on authentication protocol design. SIGOPS Oper. Syst. Rev. 28(3), 24 (1994)
Metadaten
Titel
Network’s Delays in Timed Analysis of Security Protocols
verfasst von
Sabina Szymoniak
Olga Siedlecka-Lamch
Mirosław Kurkowski
Copyright-Jahr
2019
Buch
Information Systems Architecture and Technology: Proceedings of 39th International Conference on Information Systems Architecture and Technology – ISAT 2018

Print ISBN: 978-3-319-99980-7

Electronic ISBN: 978-3-319-99981-4

Copyright-Jahr: 2019

DOI
https://doi.org/10.1007/978-3-319-99981-4_3