×
Bozga, Liana; Ene, Cristian; Lakhnech, Yassine

A symbolic decision procedure for cryptographic protocols with time stamps. (English) Zbl 1094.68025

J. Log. Algebr. Program. 65, No. 1, 1-35 (2005).
Summary: We present a symbolic decision procedure for time-sensitive cryptographic protocols. We consider protocols described in a process algebra-like notation that includes clocks, time-stamps and time variables. While the values of all clocks increase with rate one when time passes, time variables are simply variables that range over the time domain and can be used to remember time-stamps, i.e. time values. Our symbolic decision procedure deals with secrecy, authentication and any property that can be described as a safety property. Our approach is based on a logic representation of sets of configurations that combines a decidable logic with time constraints.

Cited in 1 Document

MSC:

68P25 Data encryption (aspects in computer science)
68M12 Network protocols

Keywords:

verification; cryptographic protocols; security; timed models

Software:

TAPS
Cite Review PDF
Full Text: DOI

References:

[1] Alur, R.; Dill, D., A theory of timed automata, Theoretical Computer Science, 126 (1994) · Zbl 0803.68071
[2] R. Alur, T. Feder, T.A. Henzinger, The benefits of relaxing punctuality, in: Proceedings of the 10th ACM Symposium on Principles of Distributed Computing, ACM Press, 1991, pp. 139-152; R. Alur, T. Feder, T.A. Henzinger, The benefits of relaxing punctuality, in: Proceedings of the 10th ACM Symposium on Principles of Distributed Computing, ACM Press, 1991, pp. 139-152 · Zbl 1314.68195
[3] R.M. Amadio, D.Lugiez, On the reachability problem in cryptographic protocols, in: International Conference on Concurrency Theory, LNCS, vol. 1877, 2000, pp. 380-394; R.M. Amadio, D.Lugiez, On the reachability problem in cryptographic protocols, in: International Conference on Concurrency Theory, LNCS, vol. 1877, 2000, pp. 380-394 · Zbl 0999.94538
[4] G.Bella, L.C. Paulson, Mechanizing BAN Kerberos by the inductive method, in: A.J. Hu, M.Y. Vardi (Eds.), Proceedings of the 10th International Conference on Computer-Aided Verification (CAV’98), Vancouver, BC, Canada, June 1998, LNCS, Springer-Verlag, vol. 1427, pp. 416-427; G.Bella, L.C. Paulson, Mechanizing BAN Kerberos by the inductive method, in: A.J. Hu, M.Y. Vardi (Eds.), Proceedings of the 10th International Conference on Computer-Aided Verification (CAV’98), Vancouver, BC, Canada, June 1998, LNCS, Springer-Verlag, vol. 1427, pp. 416-427 · Zbl 1524.68005
[5] M.Boreale, Symbolic trace analysis of cryptographic protocols, ICALP: Annual International Colloquium on Automata, Languages and Programming, 2001; M.Boreale, Symbolic trace analysis of cryptographic protocols, ICALP: Annual International Colloquium on Automata, Languages and Programming, 2001 · Zbl 0986.94022
[6] A. Bouajjani, Y. Lakhnech, Temporal logic + timed automata: expressiveness and decidability, in: I. Lee, S.A. Smolka (Eds.), CONCUR’95: Concurrency Theory, LNCS, Springer-Verlag, vol. 962, 1995, pp. 531-546; A. Bouajjani, Y. Lakhnech, Temporal logic + timed automata: expressiveness and decidability, in: I. Lee, S.A. Smolka (Eds.), CONCUR’95: Concurrency Theory, LNCS, Springer-Verlag, vol. 962, 1995, pp. 531-546
[7] L.Bozga, Automatic verification of cryptographic protocols, PhD thesis, University Joseph Fourier (Grenoble 1), 2004; L.Bozga, Automatic verification of cryptographic protocols, PhD thesis, University Joseph Fourier (Grenoble 1), 2004
[8] Burrows, M.; Abadi, M.; Needham, R., A logic of authentication, ACM Transactions on Computer Systems, 8, 1, 18-36 (1990)
[9] J.A. Clark, J.L. Jacob, A survey of authentication protocol literature, Version 1.0, Department of Computer Science, University of York, November 1997; J.A. Clark, J.L. Jacob, A survey of authentication protocol literature, Version 1.0, Department of Computer Science, University of York, November 1997
[10] Ernie Cohen, Taps: a first-order verifier for cryptographic protocols, in: Proceedings of the 13th IEEE Computer Security Foundations Workshop (CSFW’00), IEEE Computer Society, 2000, p. 144; Ernie Cohen, Taps: a first-order verifier for cryptographic protocols, in: Proceedings of the 13th IEEE Computer Security Foundations Workshop (CSFW’00), IEEE Computer Society, 2000, p. 144 · Zbl 0974.68562
[11] Comon, H., Disunification a survey, (Computational Logic: Essays in Honor of Alan Robinson (1991.), MIT Press: MIT Press Cambridge, MA) · Zbl 0793.03002
[12] Comon, H.; Shmatikov, V., Is it possible to decide whether a cryptographic protocol is secure or not?, Journal of Telecommunications and Information Technology (2002)
[13] H. Comon-Lundh, V. Cortier, New decidability results for fragments of first-order logic and application to cryptographic protocols, in: 14th Int. Conf. Rewriting Techniques and Applications (RTA’2003), LNCS, vol. 2706, 2003; H. Comon-Lundh, V. Cortier, New decidability results for fragments of first-order logic and application to cryptographic protocols, in: 14th Int. Conf. Rewriting Techniques and Applications (RTA’2003), LNCS, vol. 2706, 2003 · Zbl 1038.03012
[14] Cortier, V.; Millen, J.; Rueß, H., Proving secrecy is easy enough, IEEE Computer Security Foundations Workshop, 97-110 (2001)
[15] Dolev, D.; Yao, A. C., On the security of public key protocols, IEEE Transactions on Information Theory, 29, 2, 198-208 (1983) · Zbl 0502.94005
[16] Neil Evans; Steve Schneider, Analyzing time dependent security properties in CSP using PVS, ESORICS, 222-237 (2000)
[17] M. Fiore, M. Abadi, Computing symbolic models for verifying cryptographic protocols, in: 14th IEEE Computer Security Foundations Workshop (CSFW ’01), Washington-Brussels-Tokyo, June 2001, IEEE, pp. 160-173; M. Fiore, M. Abadi, Computing symbolic models for verifying cryptographic protocols, in: 14th IEEE Computer Security Foundations Workshop (CSFW ’01), Washington-Brussels-Tokyo, June 2001, IEEE, pp. 160-173
[18] Gong, Li, A security risk of depending on synchronized clocks, Operating Systems Review, 26, 1, 49-53 (1992)
[19] T.A. Henzinger, X. Nicollin, J. Sifakis, S. Yovine, Symbolic model-checking for real-time systems, in: Seventh Annual IEEE Symposium on Logic in Computer Science, IEEE Computer Society Press, 1992, pp. 394-406; T.A. Henzinger, X. Nicollin, J. Sifakis, S. Yovine, Symbolic model-checking for real-time systems, in: Seventh Annual IEEE Symposium on Logic in Computer Science, IEEE Computer Society Press, 1992, pp. 394-406 · Zbl 0806.68080
[20] Jouannaud, J. P.; Kirchner, C., Solving equations in abstract algebras: a rule-based survey of unification, (Jean-Louis Lassez; Gordon Plotkin, Computational Logic Essays in Honor of Alan Robinson (1991.), MIT Press)
[21] G. Lowe, Breaking and fixing the Needham-Schroeder Public-Key protocol using FDR, in: Tools and Algorithms for the Construction and Analysis of Systems, LNCS, vol. 1055, 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, LNCS, vol. 1055, 1996, pp. 147-166
[22] G. Lowe. A hierarchy of authentication specifications, in: 10th IEEE Computer Security Foundations Workshop (CSFW ’97), Washington-Brussels-Tokyo, June 1997, IEEE, pp. 31-44; G. Lowe. A hierarchy of authentication specifications, in: 10th IEEE Computer Security Foundations Workshop (CSFW ’97), Washington-Brussels-Tokyo, June 1997, IEEE, pp. 31-44
[23] Millen, J.; Shmatikov, V., Constraint solving for bounded-process cryptographic protocol analysis, ACM Conference on Computer and Communications Security, 166-175 (2001)
[24] Paulson, L., Proving properties of security protocols by induction, IEEE Computer Security Foundations Workshop, 70-83 (1997)
[25] A.W. Roscoe. Intensional specification of security protocols, in: 9th IEEE Computer Security Foundations Workshop (CSFW ’96), Washington-Brussels-Tokyo, June 1996, IEEE, pp. 28-38; A.W. Roscoe. Intensional specification of security protocols, in: 9th IEEE Computer Security Foundations Workshop (CSFW ’96), Washington-Brussels-Tokyo, June 1996, IEEE, pp. 28-38
[26] Rusinowitch, M.; Turuani, M., Protocol insecurity with finite number of sessions is NP-complete, IEEE Computer Security Foundations Workshop (2001.)
[27] S. Schneider, Verifying authentication protocols with CSP, in: 10th IEEE Computer Security Foundations Workshop (CSFW ’97), Washington-Brussels-Tokyo, June 1997, IEEE, pp. 3-17; S. Schneider, Verifying authentication protocols with CSP, in: 10th IEEE Computer Security Foundations Workshop (CSFW ’97), Washington-Brussels-Tokyo, June 1997, IEEE, pp. 3-17
[28] Alexander Schrijver, Theory of Linear and Integer Programming (1986.), John Wiley: John Wiley Chichester · Zbl 0665.90063
[29] Thayer, J.; Herzog, J.; Guttman, J., Honest ideals on strand spaces, IEEE Computer Security Foundations Workshop, 66-78 (1998)
[30] Venkataraman, K. N., Decidability of the purely existential fragment of the theory of term algebras, JACM (1987.)
[31] Woo, T. Y.C.; Lam, S. S., Authentication for distributed systems, Computer, 25, 1, 39-52 (1992)
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.