KaoChow Protocol Timed Analysis

  • Sabina SzymoniakEmail author
Conference paper
Part of the Advances in Intelligent Systems and Computing book series (AISC, volume 889)


This paper discusses the problem of timed security protocols’ analysis. Delay in the network and encryption and decryption times are very important from a security point of view. This operations’ times may have a significant influence on users’ security. The timed analysis is based on a special formal model and computational structure. For this theoretical assumptions, a special tool has been implemented. This tool allows to calculate the correct protocol’s execution time and carry out simulations. Thanks to this, it was possible to check the possibility of Intruder’s attack including various time parameters. Experimental results are presented on KaoChow protocol example. These results show how significant for security is time.


KaoChow protocol Timed analysis Security protocols Simulations 


  1. 1.
    Kao, I.L., Chow, R.: An efficient and secure authentication protocol using uncertified keys. Oper. Syst. Rev. 29(3), 14–21 (1995)CrossRefGoogle Scholar
  2. 2.
    Paulson, L.: Inductive analysis of the internet protocol TLS. ACM Trans. Inf. Syst. Secur. (TISSEC) 2(3), 332–351 (1999)CrossRefGoogle Scholar
  3. 3.
    Burrows, M., Abadi, M., Needham, R.: A logic of authentication. Proc. R. Soc. Lond. A 426, 233–271 (1989)MathSciNetCrossRefGoogle Scholar
  4. 4.
    Lowe, G.: Breaking and fixing the Needham-Schroeder public-key protocol using FDR. In: TACAS. LNCS, pp. 147–166. Springer (1996)Google Scholar
  5. 5.
    Steingartner, W., Novitzka, V.: Coalgebras for modelling observable behaviour of programs. J. Appl. Math. Comput. Mech. 16(2), 145–157 (2017)MathSciNetCrossRefGoogle Scholar
  6. 6.
    Dolev, D., Yao, A.: On the security of public key protocols. IEEE Trans. Inf. Theor. 29(2), 198–207 (1983)MathSciNetCrossRefGoogle Scholar
  7. 7.
    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). LNCS, vol. 3576, pp. 281–285. Springer (2005)Google Scholar
  8. 8.
    Blanchet, B.: Modeling and verifying security protocols with the applied Pi Calculus and ProVerif. Found. Trends Priv. Secur. 1(1–2), 1–135 (2016)Google Scholar
  9. 9.
    Cremers, C., Mauw, S.: Operational semantics and verification of security protocols. In: Information Security and Cryptography. Springer, Heidelberg (2012)Google Scholar
  10. 10.
    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, pp. 280–291. Humboldt University (2006)Google Scholar
  11. 11.
    Jakubowska, G., Penczek, W.: Is your security protocol on time? In: Proceedings of FSEN 2007. LNCS, vol. 4767, pp. 65–80. Springer (2007)Google Scholar
  12. 12.
    Kurkowski, M.: Formalne metody weryfikacji własności protokolow zabezpieczajacych w sieciach komputerowych, Exit, Warsaw (2013). (in Polish)Google Scholar
  13. 13.
    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)CrossRefGoogle Scholar
  14. 14.
    Siedlecka-Lamch, O., Kurkowski, M., Piatkowski, J.: Probabilistic model checking of security protocols without perfect cryptography assumption. In: Proceedings of 23rd International Conference on Computer Networks, Brunow, 14–17 June 2016. Communications in Computer and Information Science, vol. 608, pp. 107–117. Springer (2016)Google Scholar
  15. 15.
    Szymoniak, S., Siedlecka-Lamch, O., Kurkowski, M.: Timed analysis of security protocols. In: Proceedings of 37th International Conference ISAT 2016, Karpacz, 18–20 September 2017. Advances in Intelligent Systems and Computing, vol. 522, pp. 53–63. Springer (2017)Google Scholar
  16. 16.
    Klasa, T., Fray, I.E.: Data scheme conversion proposal for information security monitoring systems. In: Kobayashi, S., Piegat, A., Pejaś, J., El Fray, I., Kacprzyk, J. (eds.) Hard and Soft Computing for Artificial Intelligence, Multimedia and Security. ACS 2016. Advances in Intelligent Systems and Computing, vol. 534. Springer, Cham (2017)Google Scholar
  17. 17.
    Szymoniak, S., Kurkowski, M., Piatkowski, J.: Timed models of security protocols including delays in the network. J. Appl. Math. Comput. Mech. 14(3), 127–139 (2015)CrossRefGoogle Scholar
  18. 18.
    Chadha, R., Sistla, P., Viswanathan, M.: Verification of randomized security protocols. In: 32nd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), pp. 1–12 (2017)Google Scholar
  19. 19.
    Basin, D., Cremers, C., Meadows, C.: Model checking security protocols. In: Handbook of Model Checking, pp. 727–762. Springer (2018)Google Scholar
  20. 20.
    Szymoniak, S., Siedlecka-Lamch, O., Kurkowski, M.: SAT-based verification of NSPK protocol including delays in the network. In: Proceedings of the IEEE 14th International Scientific Conference on Informatics, Poprad, Slovakia, 14–16 November 2017. IEEE (2017)Google Scholar
  21. 21.
    Security Protocols Spen Repository.

Copyright information

© Springer Nature Switzerland AG 2019

Authors and Affiliations

  1. 1.Institute of Computer and Information SciencesCzestochowa University of TechnologyCzestochowaPoland

Personalised recommendations