Verification of cryptographic protocols: tagging enforces termination. (English) Zbl 1070.68033
Summary: We investigate a resolution-based verification method for secrecy and authentication properties of cryptographic protocols. In experiments, we could enforce its termination by tagging, a syntactic transformation of messages that leaves attack-free executions invariant. In this paper, we generalize the experimental evidence: we prove that the verification method always terminates for tagged protocols.
MSC:
| 68P25 | Data encryption (aspects in computer science) |
Software:
TAPSReferences:
| [1] | M. Abadi, B. Blanchet, Analyzing security protocols with secrecy types and logic programs, in: 29th ACM Symp. on Principles of Programming Languages (POPL’02), January 2002, pp. 33-44.; M. Abadi, B. Blanchet, Analyzing security protocols with secrecy types and logic programs, in: 29th ACM Symp. on Principles of Programming Languages (POPL’02), January 2002, pp. 33-44. · Zbl 1323.68259 |
| [2] | Abadi, M.; Needham, R., Prudent engineering practice for cryptographic protocols, IEEE Trans. Software Eng., 22, 1, 6-15 (1996) |
| [3] | R. Amadio, W. Charatonik, On name generation and set-based analysis in the Dolev-Yao model, in: CONCUR’02—Concurrency Theory, Lecture Notes in Computer Science, Vol. 2421, Springer, August 2002, pp. 499-514.; R. Amadio, W. Charatonik, On name generation and set-based analysis in the Dolev-Yao model, in: CONCUR’02—Concurrency Theory, Lecture Notes in Computer Science, Vol. 2421, Springer, August 2002, pp. 499-514. · Zbl 1012.68522 |
| [4] | B. Blanchet, An efficient cryptographic protocol verifier based on Prolog rules, in: 14th IEEE Computer Security Foundations Workshop (CSFW-14), June 2001, pp. 82-96.; B. Blanchet, An efficient cryptographic protocol verifier based on Prolog rules, in: 14th IEEE Computer Security Foundations Workshop (CSFW-14), June 2001, pp. 82-96. |
| [5] | B. Blanchet, From secrecy to authenticity in security protocols, in: Ninth Internat. Static Analysis Symp. (SAS’02), Lecture Notes in Computer Science, Vol. 2477, Springer, Berlin, September 2002, pp. 342-359.; B. Blanchet, From secrecy to authenticity in security protocols, in: Ninth Internat. Static Analysis Symp. (SAS’02), Lecture Notes in Computer Science, Vol. 2477, Springer, Berlin, September 2002, pp. 342-359. · Zbl 1015.68070 |
| [6] | M. Boreale, M.G. Buscemi, A framework for the analysis of security protocols, in: R. Amadio (Ed.), 13th Internat. Conf. on Concurrency Theory (CONCUR 2002), Lecture Notes in Computer Science, Vol. 2421, Brno, Csech Republic, Springer, Berlin, August 2002, pp. 483-498.; M. Boreale, M.G. Buscemi, A framework for the analysis of security protocols, in: R. Amadio (Ed.), 13th Internat. Conf. on Concurrency Theory (CONCUR 2002), Lecture Notes in Computer Science, Vol. 2421, Brno, Csech Republic, Springer, Berlin, August 2002, pp. 483-498. · Zbl 1012.68520 |
| [7] | P. Broadfoot, G. Lowe, B. Roscoe, Automating data independence, in: 6th European Symp. on Research in Computer Security (ESORICS’00), Lecture Notes in Computer Science, Vol. 1895, Springer, Berlin, October 2000, pp. 175-190.; P. Broadfoot, G. Lowe, B. Roscoe, Automating data independence, in: 6th European Symp. on Research in Computer Security (ESORICS’00), Lecture Notes in Computer Science, Vol. 1895, Springer, Berlin, October 2000, pp. 175-190. · Zbl 1481.68013 |
| [8] | P.J. Broadfoot, A.W. Roscoe, Capturing parallel attacks within the data independence framework, in: 15th IEEE Computer Security Foundations Workshop (CSFW’02), June 2002, pp. 147-159.; P.J. Broadfoot, A.W. Roscoe, Capturing parallel attacks within the data independence framework, in: 15th IEEE Computer Security Foundations Workshop (CSFW’02), June 2002, pp. 147-159. |
| [9] | Burrows, M.; Abadi, M.; Needham, R., A logic of authentication, Proc. Roy. Soc. London A, 426, 233-271 (1989) · Zbl 0687.68007 |
| [10] | E. Cohen, TAPS: a first-order verifier for cryptographic protocols, in: 13th IEEE Computer Security Foundations Workshop (CSFW-13), 2000, pp. 144-158.; E. Cohen, TAPS: a first-order verifier for cryptographic protocols, in: 13th IEEE Computer Security Foundations Workshop (CSFW-13), 2000, pp. 144-158. · Zbl 0974.68562 |
| [11] | H. Comon, V. Cortier, J. Mitchell, Tree automata with one memory, set constraints, and ping-pong protocols, in: Automata, Languages and Programming, 28th Internat. Colloq., ICALP’01, Lecture Notes in Computer Science, Vol. 2076, Springer, Berlin, July 2001, pp. 682-693.; H. Comon, V. Cortier, J. Mitchell, Tree automata with one memory, set constraints, and ping-pong protocols, in: Automata, Languages and Programming, 28th Internat. Colloq., ICALP’01, Lecture Notes in Computer Science, Vol. 2076, Springer, Berlin, July 2001, pp. 682-693. · Zbl 0986.68047 |
| [12] | H. Comon-Lundh, V. Cortier, New decidability results for fragments of first-order logic and application to cryptographic protocols, in: Proc. 14th Int. Conf. Rewriting Techniques and Applications (RTA’2003), Lecture Notes in Computer Science, Vol. 2706, Springer, Berlin, June 2003, pp. 148-164.; H. Comon-Lundh, V. Cortier, New decidability results for fragments of first-order logic and application to cryptographic protocols, in: Proc. 14th Int. Conf. Rewriting Techniques and Applications (RTA’2003), Lecture Notes in Computer Science, Vol. 2706, Springer, Berlin, June 2003, pp. 148-164. · Zbl 1038.03012 |
| [13] | R. Corin, S. Etalle, An improved constraint-based system for the verification of security protocols, in: Ninth Internat. Static Analysis Symposium (SAS’02), Lecture Notes in Computer Science, Vol. 2477, Springer, Berlin, September 2002, pp. 326-341.; R. Corin, S. Etalle, An improved constraint-based system for the verification of security protocols, in: Ninth Internat. Static Analysis Symposium (SAS’02), Lecture Notes in Computer Science, Vol. 2477, Springer, Berlin, September 2002, pp. 326-341. · Zbl 1015.68068 |
| [14] | V. Cortier, J. Millen, H. Rueß, Proving secrecy is easy enough, in: 14th IEEE Computer Security Foundations Workshop (CSFW-14), June 2001, pp. 97-108.; V. Cortier, J. Millen, H. Rueß, Proving secrecy is easy enough, in: 14th IEEE Computer Security Foundations Workshop (CSFW-14), June 2001, pp. 97-108. |
| [15] | Denning, D. E.; Sacco, G. M., Timestamps in key distribution protocols, Commun. ACM, 24, 8, 533-536 (1981) |
| [16] | N.A. Durgin, P.D. Lincoln, J.C. Mitchell, A. Scedrov, Undecidability of bounded security protocols, in: Workshop on Formal Methods and Security Protocols (FMSP’99), July 1999.; N.A. Durgin, P.D. Lincoln, J.C. Mitchell, A. Scedrov, Undecidability of bounded security protocols, in: Workshop on Formal Methods and Security Protocols (FMSP’99), July 1999. · Zbl 1033.94513 |
| [17] | Fábrega, F. J.T.; Herzog, J. C.; Guttman, J. D., Strand spacesproving security protocols correct, J. Comput. Security, 7, 2/3, 191-230 (1999) |
| [18] | A. Gordon, A. Jeffrey, Authenticity by typing for security protocols, in: 14th IEEE Computer Security Foundations Workshop (CSFW-14), June 2001, pp. 145-159.; A. Gordon, A. Jeffrey, Authenticity by typing for security protocols, in: 14th IEEE Computer Security Foundations Workshop (CSFW-14), June 2001, pp. 145-159. |
| [19] | J. Goubault-Larrecq, A method for automatic cryptographic protocol verification (extended abstract), invited paper, in: Fifth Internat. Workshop on Formal Methods for Parallel Programming: Theory and Applications (FMPPTA’00), Lecture Notes in Computer Science, Vol. 1800, Springer, Berlin, May 2000, pp. 977-984.; J. Goubault-Larrecq, A method for automatic cryptographic protocol verification (extended abstract), invited paper, in: Fifth Internat. Workshop on Formal Methods for Parallel Programming: Theory and Applications (FMPPTA’00), Lecture Notes in Computer Science, Vol. 1800, Springer, Berlin, May 2000, pp. 977-984. |
| [20] | J.D. Guttman, F.J.T. Fábrega, Protocol independence through disjoint encryption, in: Proc., 13th IEEE Computer Security Foundations Workshop (CSFW’00), July 2000, pp. 24-34.; J.D. Guttman, F.J.T. Fábrega, Protocol independence through disjoint encryption, in: Proc., 13th IEEE Computer Security Foundations Workshop (CSFW’00), July 2000, pp. 24-34. |
| [21] | J. Heather, G. Lowe, S. Schneider, How to prevent type flaw attacks on security protocols, in: 13th IEEE Computer Security Foundations Workshop (CSFW-13), July 2000, pp. 255-268.; J. Heather, G. Lowe, S. Schneider, How to prevent type flaw attacks on security protocols, in: 13th IEEE Computer Security Foundations Workshop (CSFW-13), July 2000, pp. 255-268. |
| [22] | J. Heather, S. Schneider, Towards automatic verification of authentication protocols on an unbounded network, in: 13th IEEE Computer Security Foundations Workshop (CSFW-13), July 2000, pp. 132-143.; J. Heather, S. Schneider, Towards automatic verification of authentication protocols on an unbounded network, in: 13th IEEE Computer Security Foundations Workshop (CSFW-13), July 2000, pp. 132-143. |
| [23] | G. Lowe, Breaking and fixing the Needham-Schroeder public-key protocol using FDR, in: Tools and Algorithms for the Construction and Analysis of Systems, Lecture Notes in Computer Science, Vol. 1055, Springer, Berlin, 1996. pp. 147-166.; G. Lowe, Breaking and fixing the Needham-Schroeder public-key protocol using FDR, in: Tools and Algorithms for the Construction and Analysis of Systems, Lecture Notes in Computer Science, Vol. 1055, Springer, Berlin, 1996. pp. 147-166. |
| [24] | G. Lowe, A hierarchy of authentication specifications, in: 10th IEEE Computer Security Foundations Workshop (CSFW ’97), June 1997, pp. 31-43.; G. Lowe, A hierarchy of authentication specifications, in: 10th IEEE Computer Security Foundations Workshop (CSFW ’97), June 1997, pp. 31-43. |
| [25] | J. Millen, V. Shmatikov, Constraint solving for bounded-process cryptographic protocol analysis, in: Eighth ACM Conf. on Computer and Communications Security (CCS’01), 2001, pp. 166-175.; J. Millen, V. Shmatikov, Constraint solving for bounded-process cryptographic protocol analysis, in: Eighth ACM Conf. on Computer and Communications Security (CCS’01), 2001, pp. 166-175. |
| [26] | Needham, R. M.; Schroeder, M. D., Using encryption for authentication in large networks of computers, Commun. ACM, 21, 12, 993-999 (1978) · Zbl 0387.68003 |
| [27] | F. Nielson, H.R. Nielson, H. Seidl, Cryptographic analysis in cubic time, in: TOSCA 2001—Theory of Concurrency, Higher Order Languages and Types, Electronic Notes in Theoretical Computer Science, Vol. 62, November 2001.; F. Nielson, H.R. Nielson, H. Seidl, Cryptographic analysis in cubic time, in: TOSCA 2001—Theory of Concurrency, Higher Order Languages and Types, Electronic Notes in Theoretical Computer Science, Vol. 62, November 2001. · Zbl 0977.68520 |
| [28] | Otway, D.; Rees, O., Efficient and timely mutual authentication, Operating Systems Rev., 21, 1, 8-10 (1987) |
| [29] | Paulson, L. C., The inductive approach to verifying cryptographic protocols, J. Comput. Security, 6, 1-2, 85-128 (1998) |
| [30] | R. Ramanujam, S. Suresh, A decidable subclass of unbounded security protocols, in: WITS’03—Workshop on Issues in the Theory of Security, April 2003, pp. 11-20.; R. Ramanujam, S. Suresh, A decidable subclass of unbounded security protocols, in: WITS’03—Workshop on Issues in the Theory of Security, April 2003, pp. 11-20. |
| [31] | R. Ramanujam, S. Suresh, Tagging makes secrecy decidable with unbounded nonces as well, in: FST TCS 2003: Foundations of Software Technology and Theoretical Computer Science, Lecture Notes in Computer Science, Vol. 2914, Springer, Berlin, December 2003, pp. 363-374.; R. Ramanujam, S. Suresh, Tagging makes secrecy decidable with unbounded nonces as well, in: FST TCS 2003: Foundations of Software Technology and Theoretical Computer Science, Lecture Notes in Computer Science, Vol. 2914, Springer, Berlin, December 2003, pp. 363-374. · Zbl 1205.94097 |
| [32] | Roscoe, A. W.; Broadfoot, P. J., Proving security protocols with model checkers by data independence techniques, J. Comput. Security, 7, 2,3, 147-190 (1999) |
| [33] | M. Rusinovitch, M. Turuani, Protocol insecurity with finite number of sessions is NP-complete, in: 14th IEEE Computer Security Foundations Workshop (CSFW-14), June 2001, pp. 174-187.; M. Rusinovitch, M. Turuani, Protocol insecurity with finite number of sessions is NP-complete, in: 14th IEEE Computer Security Foundations Workshop (CSFW-14), June 2001, pp. 174-187. |
| [34] | C. Weidenbach, Towards an automatic analysis of security protocols in first-order logic, in: 16th Internat. Conf. on Automated Deduction (CADE-16), Lecture Notes in Artificial Intelligence, Vol. 1632, Springer, Berlin, July 1999, pp. 314-328.; C. Weidenbach, Towards an automatic analysis of security protocols in first-order logic, in: 16th Internat. Conf. on Automated Deduction (CADE-16), Lecture Notes in Artificial Intelligence, Vol. 1632, Springer, Berlin, July 1999, pp. 314-328. · Zbl 1038.94548 |
| [35] | Woo, T. Y.C.; Lam, S. S., Authentication for distributed systems, Computer, 25, 1, 39-52 (1992) |
| [36] | T.Y.C. Woo, S.S. Lam, A semantic model for authentication protocols, in: IEEE Symposium on Research in Security and Privacy, May 1993, pp. 178-194.; T.Y.C. Woo, S.S. Lam, A semantic model for authentication protocols, in: IEEE Symposium on Research in Security and Privacy, May 1993, pp. 178-194. |
| [37] | Woo, T. Y.C.; Lam, S. S., Authentication for distributed systems, (Denning, D.; Denning, P., Internet Besieged: Countering Cyberspace Scofflaws (1997), ACM Press and Addison-Wesley: ACM Press and Addison-Wesley New York and Reading, MA), 319-355 |
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.
