Security protocols analysis including various time parameters

Sabina Szymoniak; Sabina Szymoniak

doi:10.3934/mbe.2021061

Mathematical Biosciences and Engineering

2021, Volume 18, Issue 2: 1136-1153. doi: 10.3934/mbe.2021061

Previous Article Next Article

Research article Special Issues

Security protocols analysis including various time parameters

Sabina Szymoniak ^,

Department of Computer Science, Czestochowa University of Technology, Dabrowskiego 69, 42-201 Czestochowa, Poland

Received: 28 September 2020 Accepted: 17 December 2020 Published: 11 January 2021

Communication is a key element of everyone's life. Nowadays, we most often use internet connections for communication. We use the network to communicate with our family, make purchases, we operate home appliances, and handle various matters related to public administration. Moreover, the Internet enables us to participate virtually in various official meetings or conferences. There is a risk of losing our sensitive data, as well as their use for malicious purposes. In this situation, each connection should be secured with an appropriate security protocol. These protocols also need to be regularly checked for vulnerability to attacks. In this article, we consider a tool that allows to analyze different executions of security protocols as well as simulate their operation. This research enables the gathering of knowledge about the behaviour of the security protocol, taking into account various time parameters (time of sending the message, time of generation confidential information, encryption and decryption times, delay in the network, lifetime) and various aspects of computer networks. The conducted research and analysis of the obtained results enable the evaluation of the protocol security and its vulnerability to attacks. Our approach also assumes the possibility of setting time limits that should be met during communication and operation of the security protocol. We show obtained results on Andrew and Needham Schroeder Public Key protocols examples.
- security protocols,
- timed analysis,
- formal verification,
- network application,
- attacks
Citation: Sabina Szymoniak. Security protocols analysis including various time parameters[J]. Mathematical Biosciences and Engineering, 2021, 18(2): 1136-1153. doi: 10.3934/mbe.2021061

Related Papers:

Abstract

Communication is a key element of everyone's life. Nowadays, we most often use internet connections for communication. We use the network to communicate with our family, make purchases, we operate home appliances, and handle various matters related to public administration. Moreover, the Internet enables us to participate virtually in various official meetings or conferences. There is a risk of losing our sensitive data, as well as their use for malicious purposes. In this situation, each connection should be secured with an appropriate security protocol. These protocols also need to be regularly checked for vulnerability to attacks. In this article, we consider a tool that allows to analyze different executions of security protocols as well as simulate their operation. This research enables the gathering of knowledge about the behaviour of the security protocol, taking into account various time parameters (time of sending the message, time of generation confidential information, encryption and decryption times, delay in the network, lifetime) and various aspects of computer networks. The conducted research and analysis of the obtained results enable the evaluation of the protocol security and its vulnerability to attacks. Our approach also assumes the possibility of setting time limits that should be met during communication and operation of the security protocol. We show obtained results on Andrew and Needham Schroeder Public Key protocols examples.

References

[1]	R. M. Needham, M. D. Schroeder, Using encryption for authentication in large networks of computers, Commun. ACM, 21 (1978), 993–999. doi: 10.1145/359657.359659
[2]	D. Dolev, A. C. Yao, On the security of public key protocols, IEEE Trans. Inf. Theory, 29 (1983), 198–208.
[3]	G. Lowe, An attack on the needham-schroeder public-key authentication protocol, Inf. Process. Lett., 56 (1995), 131–133. doi: 10.1016/0020-0190(95)00144-2
[4]	G. Lowe, Breaking and fixing the needham-schroeder public-key protocol using FDR, in Proceedings of the Second International Workshop on Tools and Algorithms for Construction and Analysis of Systems, TACAs '96, Springer-Verlag, London, UK, 1996.
[5]	M. Burrows, M. Abadi, R. Needham, A logic of authentication, ACM Trans. Comput. Syst., 8 (1990), 18–36. doi: 10.1145/77648.77649
[6]	L. C. Paulson, Inductive analysis of the internet protocol TLS, ACM Trans. Inf. Syst. Secur., 2 (1999), 332–351. doi: 10.1145/322510.322530
[7]	M. Kurkowski, W. Penczek, Verifying security protocols modelled by networks of automata, Fundam. Inf., 79 (2007), 453–471.
[8]	B. Nguyen, C. Sprenger, C. Cremers, Abstractions for security protocol verification, J. Comput. Secur., 26 (2018), 459–508. doi: 10.3233/JCS-15769
[9]	W. Steingartner, V. Novitzka, Coalgebras for modelling observable behaviour of programs, J. Appl. Math. Comput. Mech., 16 (2017), 145–157. doi: 10.17512/jamcm.2017.2.12
[10]	J. Perh, Z. Bilanov, W. Steingartner, J. Piatko, Benchmark of software developed in different component models, in 2019 IEEE 13th International Symposium on Applied Computational Intelligence and Informatics (SACI), 2019.
[11]	D. Galinec, W. Steingartner, V. Zebic, Cyber rapid response team: An option within hybrid threats, IEEE 15th International Scientific Conference on Informatics, 2019.
[12]	A. Armando, D. Basin, Y. Boichut, Y. Chevalier, L. Compagna, J. Cuellar, et al., The AVISPA Tool for the Automated Validation of Internet Security Protocols and Applications, Springer Berlin Heidelberg, Berlin, Heidelberg, 2005.
[13]	M. Kacprzak, W. NabiaÅek, A. Niewiadomski, W. Penczek, A. PÅrola, M. Szreter, et al., Verics 2007-a model checker for knowledge and real-time, Fundam. Inf., 85 (2008), 313–328.
[14]	C. Cremers, The Scyther Tool: Verification, Falsification, and Analysis of Security Protocols, International Conference on Computer Aided Verification, 2008.
[15]	A. Casimiro, R. d Lemos, C. Gacek, Operational Semantics and Verification of Security Protocols, Information Security and Cryptography, Springer, 2012.
[16]	A. David, K. G. Larsen, A. Legay, M. Mikuionis, D. B. Poulsen, Uppaal smc tutorial, Int. J. Software Tools Technol. Trans, 17 (2015), 397–415. doi: 10.1007/s10009-014-0361-y
[17]	B. Blanchet, Modeling and verifying security protocols with the applied pi calculus and proverif, Found. Trends Priv. Secur., 1 (2016), 1–135. doi: 10.1561/3300000004
[18]	V. Cortier, S. Delaune, J. Dreier, Automatic generation of sources lemmas in tamarin: Towards automatic proofs of security protocols, European Symposium on Research in Computer Security, 2020.
[19]	M. Kurkowski, Formalne metody weryfikacji własności protokołów zabezpieczajacych w sieciach komputerowych, Informatyka-Akademicka Oficyna Wydawnicza EXIT, Akademicka Oficyna Wydawnicza Exit, 2013.
[20]	M. Kurkowski, O. Siedlecka-Lamch, P. Dudek, Using backward induction techniques in (timed) security protocols verification, in Proceedings of 12th International Conference CISIM 2013, Krakow, Poland, 2013.
[21]	O. Siedlecka-Lamch, M. Kurkowski, J. Piatkowski, Probabilistic model checking of security protocols without perfect cryptography assumption, International Conference on Computer Networks, 2016.
[22]	S. Szymoniak, M. Kurkowski, J. Piatkowski, Timed models of security protocols including delays in the network, J. Appl. Math. Comput. Mech., 14 (2015), 127–139.
[23]	R. Corin, S. Etalle, P. H. Hartel, A. Mader, Timed Analysis of Security Protocols, J. Comput. Secur. 15 (2017), 619–645.
[24]	O. Siedlecka-Lamch, I. El Fray, M. Kurkowski, J. Pejas, Verification of mutual authentication protocol for mobinfosec system, IFIP International Conference on Computer Information Systems and Industrial Management, 2015.
[25]	O. Siedlecka-Lamch, S. Szymoniak, M. Kurkowski, A fast method for security protocols verification, IFIP International Conference on Computer Information Systems and Industrial Management, 2019,
[26]	S. Szymoniak, The impact of time parameters on the security protocols correctness, International Conference on Computer Networks, 2018.
[27]	S. Szymoniak, O. Siedlecka-Lamch, M. Kurkowski, On some time aspects in security protocols analysis, International Conference on Computer Networks, 2018.
[28]	A. Kassem, P. Lafourcade, Y. Lakhnech, S. Mödersheim, Multiple independent lazy intruders, in 1st Workshop on Hot Issues in Security Principles and Trust (HotSpot 2013), 2013.
[29]	D. Basin, S. Mdersheim L. Vigan, OFMC: A symbolic model-checker for security protocols, Int. J. Inf. Secur., 4 (2005), 181–208. doi: 10.1007/s10207-004-0055-7
[30]	S. Mdersheim, F. Nielson, H. R. Nielson, Lazy mobile intruders, International Conference on Principles of Security and Trust Springer, 2013.
[31]	A. Grosser, M. Kurkowski, J. Piatkowski, S. Szymoniak, ProToc–An Universal Language for Security Protocols Specifications, Soft Computing in Computer and Information Science, 2015.
[32]	M. Satyanarayanan, Integrating security in a large distributed system, ACM Trans. Comput. Syst., 7 (1989), 247–280. doi: 10.1145/65000.65002

Reader Comments

Your name:*

Email:*
© 2021 the Author(s), licensee AIMS Press. This is an open access article distributed under the terms of the Creative Commons Attribution License (http://creativecommons.org/licenses/by/4.0)