Abstract
This paper shows a new way of automatic verification of properties of untimed and timed security protocols. To do this we use a modified version of previously introduced formal model based on a network of synchronized (timed) automata that expreses behaviour and distributed knowledge of users during protocol executions. In our new approach we will use the backward induction method for searching of a tree of all real executions of an investigated protocol. Our approach uses additionally the boolean encoding of constructed structures and SAT solvers for searching answers to the questions about investigated properties which are expressed as reachability or unreachability of undesired states in a considered model. We exemplify all our notions and formalisms on the well known NSPK, and show experimental results for checking authentication and security properties of a few untimed and timed protocols.
The second and the third author acknowledge support from EU Project (European Social Fund.) PO KL Information technologies: Research and their interdisciplinary applications, Agreement UDA***/*-*/*POKL.04.01.01-00-051/10-00.
Chapter PDF
Similar content being viewed by others
References
Amnell, T., et al.: UPPAAL - Now, Next, and Future. In: Cassez, F., Jard, C., Rozoy, B., Dermot, M. (eds.) MOVEP 2000. LNCS, vol. 2067, pp. 99–124. Springer, Heidelberg (2001)
Armando, A., et al.: The AVISPA Tool for the Automated Validation of Internet Security Protocols and Applications. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol. 3576, pp. 281–285. Springer, Heidelberg (2005)
Armando, A., Compagna, L.: Sat-based model-checking for security protocols analysis. International Journal of Information Security 7(1), 3–32 (2008)
Bella, G., Massacci, F., Paulson, L.C.: Verifying the set registration protocols. IEEE Journal on Selected Areas in Communications 20(1), 77–87 (2003)
Bella, G., Paulson, L.C.: Using Isabelle to prove properties of the kerberos authentication system. In: Orman, H., Meadows, C. (eds.) Proc. of the DIMACS Workshop on Design and Formal Verification of Security Protocols (1997)
Burrows, M., Abadi, M., Needham, R.M.: A logic of authentication. ACM Trans. Comput. Syst. 8(1), 18–36 (1990)
Cohen, E.: TAPS: A first-order verifier for cryptographic protocols. In: CSFW 2000: Proceedings of the 13th IEEE Computer Security Foundations Workshop (CSFW 2000), p. 144. IEEE Computer Society, Washington, DC (2000)
Corin, R., Etalle, S., Hartel, P.H., Mader, A.: Timed model checking of security protocols. In: Proc. of the 2004 ACM Workshop FMSE, pp. 23–32. ACM (2004)
Delzanno, G., Ganty, P.: Automatic verification of time sensitive cryptographic protocols. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol. 2988, pp. 342–356. Springer, Heidelberg (2004)
Dolev, D., Yao, A.: On the security of public key protocols. IEEE Transactions on Information Theory 29(2), 198–207 (1983)
El Fray, I., Kurkowski, M., Pejaś, J., Maćków, W.: A New Mathematical Model for the Analytical Risk Assessment and Prediction in IT Systems. Control & Cybernetics 41, 241–268 (2012); Systems Research Institute PAS, Warsaw
Evans, N., Schneider, S.: Analysing time dependent security properties in CSP using PVS. In: Cuppens, F., Deswarte, Y., Gollmann, D., Waidner, M. (eds.) ESORICS 2000. LNCS, vol. 1895. Springer, Heidelberg (2000)
Jakubowska, G., Penczek, W., Srebrny, M.: Verifying security protocols with timestamps via translation to timed automata. In: Proc. of the International Workshop on Concurrency, Specification and Programming (CS&P 2005), pp. 100–115. Warsaw University (2005)
Kacprzak, M., et al.: Verics 2007 - a model checker for knowledge and real-time. Fundam. Inform. 85(1-4), 313–328 (2008)
Kurkowski, M., Maćków, W.: Using Backward Strategy to the Needham-Schroeder Public Key Protocol Verification. In: Artificial Intelligence and Security in Computing Systems, pp. 249–260. Kluwer Academic Publishers, Boston (2003)
Kurkowski, M., Pejaś, J.: A Propositional Logic for Access Control Policy in Distributed Systems. In: Artificial Intelligence and Security in Computing Systems, pp. 157–191. Kluwer Academic Publishers, Boston (2003)
Kurkowski, M., Penczek, W.: Verifying Security Protocols Modeled by Networks of Automata. Fund. Inform. 79(3-4), 453–471 (2007)
Kurkowski, M., Penczek, W.: Verifying Timed Security Protocols via Translation to Timed Automata. Fund. Inform. 93(1-3), 245–259 (2009)
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. Chapman&Hall/CRC Press, Boca Raton (2012)
Kurkowski, M., Srebrny, M.: A Quantifier-free First-order Knowledge Logic of Authentication. Fund. Inform. 72, 263–282 (2006)
Lowe, G.: Breaking and Fixing the Needham-Schroeder Public-key Protocol Using fdr. In: Margaria, T., Steffen, B. (eds.) TACAS 1996. LNCS, vol. 1055, pp. 147–166. Springer, Heidelberg (1996)
Lowe, G.: Some new attacks upon security protocols. In: Proceedings of the Computer Security Foundations Workshop VIII. IEEE Computer Society Press (1996)
Meadows, C.: The NRL protocol analyzer: An overview. Journal of Logic Programming 26(2), 13–131 (1996)
Moore, J.H.: Protocol failures in cryptosystems. Proceedings of the IEEE 76(5) (1988)
Needham, R.M., Schroeder, M.D.: Using encryption for authentication in large networks of computers. Commun. ACM 21(12), 993–999 (1978)
Paulson, L.C.: Inductive analysis of the internet protocol tls. ACM Trans. Inf. Syst. Secur. 2(3), 332–351 (1999)
Siedlecka-Lamch, O., Kurkowski, M., Piech, H.: A New Effective Approach for Modeling and Verification of Security Protocols. In: Proceedings of 21st International Workshop on Concurrency, Specification and Programming (CS&P 2012), pp. 191–202. Humboldt University Press, Berlin (2012)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2013 IFIP International Federation for Information Processing
About this paper
Cite this paper
Kurkowski, M., Siedlecka-Lamch, O., Dudek, P. (2013). Using Backward Induction Techniques in (Timed) Security Protocols Verification. In: Saeed, K., Chaki, R., Cortesi, A., Wierzchoń, S. (eds) Computer Information Systems and Industrial Management. CISIM 2013. Lecture Notes in Computer Science, vol 8104. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-40925-7_25
Download citation
DOI: https://doi.org/10.1007/978-3-642-40925-7_25
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-40924-0
Online ISBN: 978-3-642-40925-7
eBook Packages: Computer ScienceComputer Science (R0)