Abstract
We improve the NP proof for the insecurity problem, partly motivated by an error in the NP proof of the influential paper “Protocol insecurity with a finite number of sessions and composed keys is NP-complete” by Rusinowitch and Turuani [1]. We enhance several different aspects of the proofs with a complete presentation, and we prove stronger results that fix the non-trivial error. Besides fixing the error, our proof framework has reusable structure and proves several results that are neither covered nor proved in [1] and its sequels, including the important fact that the attacker does not need to generate nonces in an attack, which the proof of [1] relies on. We show a sharper result that the complexity of the derivation problem is in square time. Furthermore, we extend the scope of the NP complexity to cover the scenarios where a fixed number of role instances are assumed, and delayed decryption is allowed. These are new results since the NP result of assuming a fixed number of role instances does not seem to be obtainable by a reduction from the NP result of assuming a fixed number of sessions, and [1] and its sequels cannot handle delayed decryption.
Research is done at the University of Houston, supported in part by NSF grants CCF 0306475 and CNS 0755500. Current address of the first author: LDCSEE Department, West Virginia University, Morgantown, WV 26506, USA.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Rusinowitch, M., Turuani, M.: Protocol insecurity with a finite number of sessions, composed keys is NP-complete. Theor. Comput. Sci. 1-3(299), 451–475 (2003)
Turuani, M.: Web page, http://www.loria.fr/~turuani/
Liang, Z., Verma, R.M.: Complexity of checking freshness of cryptographic protocols. In: Sekar, R., Pujari, A.K. (eds.) ICISS 2008. LNCS, vol. 5352, pp. 86–101. Springer, Heidelberg (2008)
Chevalier, Y., Küsters, R., Rusinowitch, M., Turuani, M.: Complexity results for security protocols with Diffie-Hellman exponentiation and commuting public key encryption. ACM Transactions on Computational Logic (TOCL) 9(4) (2008)
Amadio, R.M., Lugiez, D., Vanackère, V.: On the symbolic reduction of processes with cryptographic functions. Theor. Comput. Sci. 290(1), 695–740 (2003)
Millen, J.K., Shmatikov, V.: Constraint solving for bounded-process cryptographic protocol analysis. In: ACM Conference on Computer and Communications Security, pp. 166–175 (2001)
Durgin, N.A., Lincoln, P., Mitchell, J.C.: Multiset rewriting and the complexity of bounded security protocols. Journal of Computer Security 12(2), 247–311 (2004)
Liang, Z., Verma, R.M.: Correcting and Improving the NP Proof for Cryptographic Protocol Insecurity. Technical Report UH-CS-09-10, Computer Science Department, University of Houston (September 2009), http://www.cs.uh.edu/preprint
Tiplea, F.L., Enea, C., Birjoveanu, C.V.: Decidability and complexity results for security protocols. In: Verification of Infinite-State Systems with Applications to Security, pp. 185–211. IOS Press, Amsterdam (2006)
Chevalier, Y., Küsters, R., Rusinowitch, M., Turuani, M.: Deciding the security of protocols with Diffie-Hellman exponentiation and products in exponents. In: Pandya, P.K., Radhakrishnan, J. (eds.) FSTTCS 2003. LNCS, vol. 2914, pp. 124–135. Springer, Heidelberg (2003)
Chevalier, Y., Küsters, R., Rusinowitch, M., Turuani, M.: An NP decision procedure for protocol insecurity with XOR. Theor. Comput. Sci. 338(1-3), 247–274 (2005)
Chevalier, Y., Küsters, R., Rusinowitch, M., Turuani, M.: Deciding the security of protocols with commuting public key encryption. Electronic Notes in Theoretical Computer Science 125(1), 55–66 (2005)
Liang, Z., Verma, R.M.: A note on an NP-completeness proof for cryptographic protocol insecurity. Technical Report UH-CS-08-15, Computer Science Department, University of Houston (October 2008), http://www.cs.uh.edu/preprint
Froschle, S.: The insecurity problem: Tackling unbounded data. In: IEEE Computer Security Foundations Symposium 2007, pp. 370–384. IEEE Computer Society, Los Alamitos (2007)
Liang, Z., Verma, R.M.: Secrecy checking of protocols: Solution of an open problem. In: Automated Reasoning for Security Protocol Analysis (ARSPA 2007), July 2007, pp. 95–112 (2007)
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)
Thayer, F.J., Herzog, J.C., Guttman, J.D.: Strand spaces: Proving security protocols correct. Journal of Computer Security 7(1) (1999)
Paulson, L.C.: The inductive approach to verifying cryptographic protocols. Journal of Computer Security 6(1-2), 85–128 (1998)
Corin, R., Etalle, S.: An improved constraint-based system for the verification of security protocols. In: Hermenegildo, M.V., Puebla, G. (eds.) SAS 2002. LNCS, vol. 2477, pp. 326–341. Springer, Heidelberg (2002)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2009 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Liang, Z., Verma, R.M. (2009). Correcting and Improving the NP Proof for Cryptographic Protocol Insecurity . In: Prakash, A., Sen Gupta, I. (eds) Information Systems Security. ICISS 2009. Lecture Notes in Computer Science, vol 5905. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-10772-6_9
Download citation
DOI: https://doi.org/10.1007/978-3-642-10772-6_9
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-10771-9
Online ISBN: 978-3-642-10772-6
eBook Packages: Computer ScienceComputer Science (R0)