Abstract
Quantitative timing is often explicitly used in systems for better security, e.g., the credentials for automatic website logon often has limited lifetime. Verifying timing relevant security protocols in these systems is very challenging as timing adds another dimension of complexity compared with the untimed protocol verification. In our previous work, we proposed an approach to check the correctness of the timed authentication in security protocols with fixed timing constraints. However, a more difficult question persists, i.e., given a particular protocol design, whether the protocol has security flaws in its design or it can be configured secure with proper parameter values? In this work, we answer this question by proposing a parameterized verification framework, where the quantitative parameters in the protocols can be intuitively specified as well as automatically analyzed. Given a security protocol, our verification algorithm either produces the secure constraints of the parameters, or constructs an attack that works for any parameter values. The correctness of our algorithm is formally proved. We implement our method into a tool called PTAuth and evaluate it with several security protocols. Using PTAuth, we have successfully found a timing attack in Kerberos V which is unreported before.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
PTAuth extended paper, tool and experiment models, http://www.comp.nus.edu.sg/~li-li/r/time.html .
Abadi, M., Needham, R.M.: Prudent engineering practice for cryptographic protocols. IEEE Trans. Software Eng. 22(1), 6–15 (1996)
Bagnara, R., Ricci, E., Zaffanella, E., Hill, P.M.: Possibly not closed convex polyhedra and the parma polyhedra library. In: Hermenegildo, M.V., Puebla, G. (eds.) SAS 2002. LNCS, vol. 2477, pp. 213–229. Springer, Heidelberg (2002)
Barker, E.B., Barker, W.C., Burr, W.E., Polk, W.T., Smid, M.E.: SP 800-57. Recommendation for key management. Technical report, National Institute of Standards & Technology (2007)
Bella, G., Paulson, L.C.: Kerberos version IV: Inductive analysis of the secrecy goals. In: Quisquater, J.-J., Deswarte, Y., Meadows, C., Gollmann, D. (eds.) ESORICS 1998. LNCS, vol. 1485, pp. 361–375. Springer, Heidelberg (1998)
Blanchet, B.: An efficient cryptographic protocol verifier based on Prolog rules. In: CSFW, pp. 82–96. IEEE CS (2001)
Brands, S., Chaum, D.: Distance-bounding protocols (extended abstract). In: Helleseth, T. (ed.) Advances in Cryptology - EUROCRYPT 1993. LNCS, vol. 765, pp. 344–359. Springer, Heidelberg (1994)
Burrows, M., Abadi, M., Needham, R.M.: A logic of authentication. ACM Trans. Comput. Syst. 8(1), 18–36 (1990)
Butler, F., Cervesato, I., Jaggard, A.D., Scedrov, A., Walstad, C.: Formal analysis of kerberos 5. Theor. Comput. Sci. 367, 57–87 (2006)
Capkun, S., Hubaux, J.-P.: Secure positioning in wireless networks. IEEE Journal on Selected Areas in Communications 24(2), 221–232 (2006)
CCITT. The directory authentication framework - Version 7, 1987 Draft Recommendation X.509 (1987)
Cervesato, I., Durgin, N.A., Lincoln, P., Mitchell, J.C., Scedrov, A.: A meta-notation for protocol analysis. In: CSFW, pp. 55–69. IEEE CS (1999)
Cremers, C.J.F.: The Scyther tool: Verification, falsification, and analysis of security protocols. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol. 5123, pp. 414–418. Springer, Heidelberg (2008)
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.C.-C.: On the security of public key protocols. IEEE Transactions on Information Theory 29(2), 198–207 (1983)
Kohl, J., Neuman, B.C.: The Kerberos Network Authentication Service (Version 5). Internet Request for Comments RFC-1510. RFC Editor (1993)
Kohl, J.T., Neuman, B.C., T’so, T.Y.: The evolution of the kerberos authentication system. In: Distributed Open Systems, pp. 78–94. IEEE CS (1994)
Krawczyk, H.: Skeme: A versatile secure key exchange mechanism for internet. In: NDSS, pp. 114–127. IEEE CS (1996)
LDAP Account Manager. Kerberos V implementation heimdal-1.5.2 (2014), http://www.h5l.org
Li, L., Sun, J., Liu, Y., Dong, J.S.: Tauth: Verifying timed security protocols. In: Merz, S., Pang, J. (eds.) ICFEM 2014. LNCS, vol. 8829, pp. 300–315. Springer, Heidelberg (2014)
Lowe, G.: An attack on the needham-schroeder public-key authentication protocol. Information Processing Letters 56, 131–133 (1995)
Lowe, G.: A family of attacks upon authentication protocols. Technical report, Department of Mathematics and Computer Science, University of Leicester (1997)
Meier, S., Schmidt, B., Cremers, C., Basin, D.: The TAMARIN prover for the symbolic analysis of security protocols. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 696–701. Springer, Heidelberg (2013)
MIT. Kerberos V implementation krb5-1.13 (2014), http://web.mit.edu/kerberos/
Mitchell, J., Mitchell, M., Stern, U.: Automated analysis of cryptographic protocols using Murϕ. In: S&P, pp. 141–151 (1997)
Needham, R.M., Schroeder, M.D.: Using encryption for authentication in large networks of computers. Commun. ACM 21(12), 993–999 (1978)
Neuman, C., Yu, T., Hartman, S., Raeburn, K.: The Kerberos Network Authentication Service (Version 5). RFC-4120. RFC Editor (2005)
Sastry, N., Shankar, U., Wagner, D.: Secure verification of location claims. In: Workshop on Wireless Security, pp. 1–10. ACM (2003)
Sedighpour, S., Capkun, S., Ganeriwal, S., Srivastava, M.B.: Implementation of attacks on ultrasonic ranging systems (demo). In: SenSys, p. 312. ACM (2005)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2015 Springer International Publishing Switzerland
About this paper
Cite this paper
Li, L., Sun, J., Liu, Y., Dong, J.S. (2015). Verifying Parameterized Timed Security Protocols. In: Bjørner, N., de Boer, F. (eds) FM 2015: Formal Methods. FM 2015. Lecture Notes in Computer Science(), vol 9109. Springer, Cham. https://doi.org/10.1007/978-3-319-19249-9_22
Download citation
DOI: https://doi.org/10.1007/978-3-319-19249-9_22
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-19248-2
Online ISBN: 978-3-319-19249-9
eBook Packages: Computer ScienceComputer Science (R0)