On the symbolic reduction of processes with cryptographic functions. (English) Zbl 1051.68054
Summary: We study the reachability problem for cryptographic protocols represented as processes relying on perfect cryptographic functions. We introduce a symbolic reduction system that can handle hashing functions, symmetric keys, and public keys. Desirable properties such as secrecy or authenticity are specified by inserting logical assertions in the processes. We show that the symbolic reduction system provides a flexible decision procedure for finite processes and a reference for sound implementations. The symbolic reduction system can be regarded as a variant of syntactic unification which is compatible with certain set-membership constraints. For a significant fragment of our formalism, we argue that a dag implementation of the symbolic reduction system leads to an algorithm running in NPTIME thus matching the lower bound of the problem. In the case of iterated or finite control processes, we show that the problem is undecidable in general and in PTIME for a subclass of iterated processes that do not rely on pairing. Our technique is based on rational transductions of regular languages and it applies to a class of processes containing the ping-pong protocols presented by D. Dolev, S. Even and R. M. Karp [Inf. Control 55, 57–68 (1982; Zbl 0537.94012)].
MSC:
| 68P25 | Data encryption (aspects in computer science) |
Citations:
Zbl 0537.94012References:
| [1] | R. Amadio, W. Charatonik, On name generation and set-based analysis in Dolev-Yao model, RR-INRIA, January 2002.; R. Amadio, W. Charatonik, On name generation and set-based analysis in Dolev-Yao model, RR-INRIA, January 2002. · Zbl 1012.68522 |
| [2] | R. Amadio, D. Lugiez, On the reachability problem in cryptographic protocols, in: Proc. CONCUR00, Lecture Notes in Computer Science, Vol. 1877, Springer, Berlin, 2000, also RR-INRIA 3915.; R. Amadio, D. Lugiez, On the reachability problem in cryptographic protocols, in: Proc. CONCUR00, Lecture Notes in Computer Science, Vol. 1877, Springer, Berlin, 2000, also RR-INRIA 3915. · Zbl 0999.94538 |
| [3] | R. Amadio, S. Prasad, The game of the name in cryptographic tables, in: Proc. ASIAN99, Lecture Notes in Computer Science, Vol. 1742, Springer, Berlin, 1999.; R. Amadio, S. Prasad, The game of the name in cryptographic tables, in: Proc. ASIAN99, Lecture Notes in Computer Science, Vol. 1742, Springer, Berlin, 1999. · Zbl 0989.94506 |
| [4] | R. Amadio, D. Lugiez, V. Vanackère, On the reachability problem in cryptographic protocols, Workshop on Issues in the Theory of Security, Geneve, 2000, Short presentation of results in [2]; R. Amadio, D. Lugiez, V. Vanackère, On the reachability problem in cryptographic protocols, Workshop on Issues in the Theory of Security, Geneve, 2000, Short presentation of results in [2] |
| [5] | R. Amadio, D. Lugiez, V. Vanackère, On the symbolic reduction of processes with cryptographic functions, Research Report INRIA-Sophia, March 2001.; R. Amadio, D. Lugiez, V. Vanackère, On the symbolic reduction of processes with cryptographic functions, Research Report INRIA-Sophia, March 2001. |
| [6] | M. Abadi, P. Rogaway, Reconciling two views of cryptography, in: Proc. IFIP TCS, Sendai, 2000.; M. Abadi, P. Rogaway, Reconciling two views of cryptography, in: Proc. IFIP TCS, Sendai, 2000. · Zbl 1008.68048 |
| [7] | Baader, F.; Nipkow, T., Term Rewriting and All That (1998), Cambridge University Press: Cambridge University Press Cambridge |
| [8] | D. Bolignano, Formal verification of cryptographic protocols, in: Proc. ACM Conf. on Computer Communication and Security, 1996.; D. Bolignano, Formal verification of cryptographic protocols, in: Proc. ACM Conf. on Computer Communication and Security, 1996. |
| [9] | M. Boreale, On name generation and set-based analysis in Dolev-Yao model, Draft, March 2000, Revised version appeared in Proc. ICALP01, Lecture Notes in Computer Science, Vol. 2076, Springer, Berlin, 2001.; M. Boreale, On name generation and set-based analysis in Dolev-Yao model, Draft, March 2000, Revised version appeared in Proc. ICALP01, Lecture Notes in Computer Science, Vol. 2076, Springer, Berlin, 2001. |
| [10] | M. Boreale, R. De Nicola, R. Pugliese, Proof techniques for cryptographic processes, in: Proc. IEEE Logic in Computer Science, 1999.; M. Boreale, R. De Nicola, R. Pugliese, Proof techniques for cryptographic processes, in: Proc. IEEE Logic in Computer Science, 1999. · Zbl 1017.68050 |
| [11] | Burrow, M.; Abadi, M.; Needham, R., A logic of authentication, Proc. Roy. Soc. Lond., 426, 233-271 (1989) · Zbl 0687.68007 |
| [12] | Büchi, R., Regular canonical systems, Arch. Math. Logik Grundlag., 6, 91-111 (1964) · Zbl 0129.26102 |
| [13] | Caucal, D., On the regular structure of prefix rewriting, Theoret. Comput. Sci., 106, 61-86 (1992) · Zbl 0780.68077 |
| [14] | E. Clarke, S. Jha, W. Marrero, Using state space exploration and a natural deduction style message derivation engine to verify security protocols, in: Proc. IFIP PROCOMET, 1998.; E. Clarke, S. Jha, W. Marrero, Using state space exploration and a natural deduction style message derivation engine to verify security protocols, in: Proc. IFIP PROCOMET, 1998. |
| [15] | J. Corbin, M. Bidoit, A rehabilitation of Robinson’s unification algorithm, in: IFIP Cong., 1983.; J. Corbin, M. Bidoit, A rehabilitation of Robinson’s unification algorithm, in: IFIP Cong., 1983. · Zbl 0522.68043 |
| [16] | H. Comon, V. Cortier, J. Mitchell, Tree automata with one memory, set constraints, and ping-pong protocols, in: Proc. ICALP, Lecture Notes in Computer Science, Vol. 2076, Springer, Berlin, 2001, pp. 682-693.; H. Comon, V. Cortier, J. Mitchell, Tree automata with one memory, set constraints, and ping-pong protocols, in: Proc. ICALP, Lecture Notes in Computer Science, Vol. 2076, Springer, Berlin, 2001, pp. 682-693. · Zbl 0986.68047 |
| [17] | Dolev, D.; Yao, A., On the security of public key protocols, IEEE Trans. Inform. Theory, 29, 2, 198-208 (1983) · Zbl 0502.94005 |
| [18] | Dolev, D.; Even, S.; Karp, R. M., On the security of ping-pong protocols, Inform. and Comput., 55, 57-68 (1982) · Zbl 0537.94012 |
| [19] | Durante, A.; Focardi, R.; Gorrieri, R., A compiler for analysing cryptographic protocols using non-interference, ACM Trans. Software Eng. Methodol., 9, 4, 489-530 (2000) |
| [20] | N. Durgin, P. Lincoln, J. Mitchell, A. Scedrov, Undecidability of bounded security protocols, in: Proc. Formal Methods and Security Protocols, FLOC Workshop, Trento, 1999.; N. Durgin, P. Lincoln, J. Mitchell, A. Scedrov, Undecidability of bounded security protocols, in: Proc. Formal Methods and Security Protocols, FLOC Workshop, Trento, 1999. · Zbl 1033.94513 |
| [21] | J. Goubault, A method for automatic cryptographic protocol verification, in: Proc. FMPPTA, Springer, Berlin, 2000.; J. Goubault, A method for automatic cryptographic protocol verification, in: Proc. FMPPTA, Springer, Berlin, 2000. |
| [22] | Hopcroft, J.; Ullman, J., Introduction to Automata Theory, Languages, and Computation (1979), Addison-Wesley: Addison-Wesley Reading, MA · Zbl 0426.68001 |
| [23] | A. Huima, Efficient infinite-state analysis of security protocols, in: Proc. Formal Methods and Security Protocols, FLOC Workshop, Trento, 1999.; A. Huima, Efficient infinite-state analysis of security protocols, in: Proc. Formal Methods and Security Protocols, FLOC Workshop, Trento, 1999. |
| [24] | F. Jacquemard, M. Rusinowitch, F. Vigneron, Compiling and verifying security protocols, in: Proc. Logic Programming and Automated Reasoning, 2000, also RR-INRIA 3938.; F. Jacquemard, M. Rusinowitch, F. Vigneron, Compiling and verifying security protocols, in: Proc. Logic Programming and Automated Reasoning, 2000, also RR-INRIA 3938. · Zbl 0988.68562 |
| [25] | G. Lowe, Breaking and fixing the Needham-Schroeder public-key protocol using FDR, in: Proc. TACAS, Lecture Notes in Computer Science, Springer, Berlin, 1996.; G. Lowe, Breaking and fixing the Needham-Schroeder public-key protocol using FDR, in: Proc. TACAS, Lecture Notes in Computer Science, Springer, Berlin, 1996. |
| [26] | G. Lowe, A hierarchy of authentication specifications, in: Proc. 10th IEEE Computer Security Foundations Workshop, 1997.; G. Lowe, A hierarchy of authentication specifications, in: Proc. 10th IEEE Computer Security Foundations Workshop, 1997. |
| [27] | Lowe, G., Towards a completeness result for model-checking of security protocols, J. Comput. Security, 2-3, 89-146 (1999) |
| [28] | J. Mitchell, M. Mitchell, U. Stern, Automated analysis of cryptographic protocols using murphi, in: Proc. IEEE Symp. on Security and Privacy, 1997.; J. Mitchell, M. Mitchell, U. Stern, Automated analysis of cryptographic protocols using murphi, in: Proc. IEEE Symp. on Security and Privacy, 1997. |
| [29] | D. Monniaux, Abstracting cryptographic protocols with tree automata, in: Proc. Static Analysis Symp., Lecture Notes in Computer Science, Springer, Berlin, 1999.; D. Monniaux, Abstracting cryptographic protocols with tree automata, in: Proc. Static Analysis Symp., Lecture Notes in Computer Science, Springer, Berlin, 1999. · Zbl 0949.68065 |
| [30] | L. Paulson, Proving properties of security protocols by induction, in: Proc. IEEE Computer Security Foundations Workshop, 1997.; L. Paulson, Proving properties of security protocols by induction, in: Proc. IEEE Computer Security Foundations Workshop, 1997. |
| [31] | M. Rusinowitch, M. Turuani, Protocol insecurity with finite number of sessions is NP-complete, RR INRIA 4134, March 2001.; M. Rusinowitch, M. Turuani, Protocol insecurity with finite number of sessions is NP-complete, RR INRIA 4134, March 2001. · Zbl 1042.68009 |
| [32] | V. Vanackère, Protocoles cryptographiques et calcul symbolique, ENS-Lyon, July 2000, Mémoire de DEA.; V. Vanackère, Protocoles cryptographiques et calcul symbolique, ENS-Lyon, July 2000, Mémoire de DEA. |
| [33] | C. Weidenbach, Towards an automatic analysis of security protocols in first-order logic, in: Proc. CADE 99, Lecture Notes in Computer Science, Vol. 1632, Springer, Berlin, 1999.; C. Weidenbach, Towards an automatic analysis of security protocols in first-order logic, in: Proc. CADE 99, Lecture Notes in Computer Science, Vol. 1632, Springer, Berlin, 1999. · Zbl 1038.94548 |
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
