Abstract
Given an arbitrary intruder deduction capability, modeled as an inference system \({\cal S}\) and a protocol, we show how to compute an inference system \(\widehat{\cal S}\) such that the security problem for an unbounded number of sessions is equivalent to the deducibility of some message in \(\widehat{\cal S}\). Then, assuming that \(\cal S\) has some subformula property, we lift such a property to \(\widehat{S}\), thanks to a proof normalisation theorem. In general, for an unbounded number of sessions, this provides with a complete deduction strategy. In case of a bounded number of sessions, our theorem implies that the security problem is co-NP-complete. As an instance of our result we get a decision algorithm for the theory of blind-signatures, which, to our knowledge, was not known before.
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
Bernat, V.: Théories de l’intrus pour la vérification de protocoles cryptographiques. PhD thesis, École Normale Supérieure de Cachan (2006)
Cervesato, I., Durgin, N., Lincoln, P., Mitchell, J., Scedrov, A.: A meta-notation for protocol analysis. In: Syverson, P. (ed.) 12-th IEEE Computer Security Foundations Workshop, IEEE Computer Society Press, Los Alamitos (1999)
Chevalier, Y., Kuester, R., Rusinowitch, M., Turuani, M.: An NP decision procedure for protocol insecurity with xor. In: Kolaitis [15]
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.) FST TCS 2003: Foundations of Software Technology and Theoretical Computer Science. LNCS, vol. 2914, pp. 124–135. Springer, Heidelberg (2003)
Clarke, E., Jha, S., Marrero, W.: Using state space exploration and a natural deduction style message derivation engine to verify security protocols. In (PROCOMET). Proceedings of the IFIP Working Conference on Programming Concepts and Methods (1998)
Comon-Lundh, H., Cortier, V.: Security properties: two agents are sufficient. Science of Computer Programming 50(1–3), 51–71 (2004)
Comon-Lundh, H., Delaune, S.: The finite variant property: How to get rid of some algebraic properties. In: Giesl, J. (ed.) RTA 2005. LNCS, vol. 3467, Springer, Heidelberg (2005)
Comon-Lundh, H., Shmatikov, V.: Intruder deductions, constraint solving and insecurity decision in preence of exclusive or. In: Kolaitis [15]
Cortier, V., Millen, J., Rueß, H.: Proving secrecy is easy enough. In: 14th IEEE Computer Security Foundations Workshop, pp. 97–108. IEEE Computer Society Press, Los Alamitos (2001)
Cortier, V., Rusinowitch, M., Zalinescu, E.: A resolution strategy for verifying cryptographic protocols with cbc encryption and blind signatures. In (PPDP 2005). Proc. 7th ACM-SIGPLAN Int. Conf. on Principles and Practice of Declarative Programming, pp. 12–22. ACM Press, New York (2005)
Denker, G., Millen, J., Rueß, H.: The CAPSL integrated protocol environment. Technical report, SRI International (October 2000)
Dershowitz, N., Jouannaud, J.-P.: Rewrite systems. In: van Leeuwen, J. (ed.) Handbook of Theoretical Computer Science, vol. B, pp. 243–309. North Holland, Amsterdam (1990)
Fabrega, F.T., Herzog, J., Guttman, J.: Strand spaces: Proving security protocol correct. Journal of Computer Security 7, 191–230 (1999)
Fujioka, A., Okamoto, T., Ohta, K.: A practical secret voting scheme for large scale elections. In: Proc. ASIACRYPT 1992. LNCS, vol. 718, pp. 244–251. Springer, Heidelberg (1993)
Kolaitis, P. (ed.): Eighteenth Annual IEEE Symposium on Logic in Computer Science. IEEE Computer Society Press, Los Alamitos (2003)
Kremer, S., Ryan, M.: Analysis of an electronic voting protocol in the applied pi-calculus. In: Sagiv, M. (ed.) ESOP 2005. LNCS, vol. 3444, Springer, Heidelberg (2005)
McAllester, D.: Automatic recognition of tractability in inference relations. J. ACM 40(2), 284–303 (1993)
Rusinowitch, M., Turuani, M.: Protocol insecurity with finite number of sessions is NP-complete. In: Proc.14th IEEE Computer Security Foundations Workshop, Cape Breton, Nova Scotia (June 2001)
Shmatikov, V.: Decidable analysis of cryptographic protocols with products and modular exponentiation. In: Schmidt, D. (ed.) ESOP 2004. LNCS, vol. 2986, Springer, Heidelberg (2004)
Security protocols open repository, http://www.lsv.ens-cachan.fr/spore/
Turuani, M.: Sécurité des protocoles cryptographiques: décidabilité et complexité. PhD thesis, Université Henri Poincaré- Nancy 1 (2003)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2007 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Bernat, V., Comon-Lundh, H. (2007). Normal Proofs in Intruder Theories. In: Okada, M., Satoh, I. (eds) Advances in Computer Science - ASIAN 2006. Secure Software and Related Issues. ASIAN 2006. Lecture Notes in Computer Science, vol 4435. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-77505-8_12
Download citation
DOI: https://doi.org/10.1007/978-3-540-77505-8_12
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-77504-1
Online ISBN: 978-3-540-77505-8
eBook Packages: Computer ScienceComputer Science (R0)