Abstract
The Neuman-Stubblebine key exchange protocol is formalized in first-order logic and analyzed by the automated theorem prover Spass. In addition to the analysis, we develop the necessary theoretical background providing new (un)decidability results for monadic firstorder fragments involved in the analysis. The approach is applicable to a variety of security protocols and we identify possible extensions leading to future directions of research.
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.
References
Bachmair, L. & Ganzinger, H. (1994),’ Rewrite-based equational theorem proving with selection and simplification’, Journal of Logic and Computation 4(3), 217–247.
Bogaert, B. & Tison, S. (1992), Equality and disequality constraints on direct subterms in tree automata, in A. Finkel & M. Jantzen, eds,’ Proceedings of 9th Annual Symposium on Theoretical Aspects of Computer Science, STACS92’, Vol. 577 of LNCS, Springer, pp. 161–171.
Burrows, M., Abadi, M. & Needham, R. (1990),’ A logic of authentication’, ACM Transactions on Computer Systems 8(1), 18–36.
Charatonik, W., McAllester, D., Niwinski, D., Podelski, A. & Walukiewicz, I. (1998), The horn mu-calculus, in `Proceedings 13th IEEE Symposium on Logic in Computer Science, LICS’98’, IEEE Computer Society Press, pp. 58–69.
Comon, H. & Delor, C. (1994),’ Equational formulae with membership constraints’, Information and Computation 112, 167–216.
Jacquemard, F., Meyer, C. & Weidenbach, C. (1998), Unification in extensions of shallow equational theories, in T. Nipkow, ed.,’ Rewriting Techniques and Applications, 9th International Conference, RTA-98’, Vol. 1379 of LNCS, Springer, pp. 76–90.
Mitchell, J. C. (1998), Finite-state analysis of security protocols, in A. J. Hu & M. Y. Vardi, eds,’ Computer Aided Verification (CAV-98): 10th International Conference’, Vol. 1427 of LNCS, Springer, pp. 71–76.
Neuman, B. C. & Stubblebine, S. G. (1993),’ A note on the use of timestamps as nonces’, ACM SIGOPS, Operating Systems Review 27(2), 10–14.
Paulson, L. C. (1997), Proving properties of security protocols by induction, in J. Millen, ed.,’ Proceedings of the 10th IEEE Computer Security Foundations Workshop’, IEEE Computer Society, pp. 70–83.
Schneier, B. (1996), Applied Cryptography, 2 edn, Wiley.
Schumann, J. (1997), Automatic verification of cryptographic protocols with setheo, in’ Proceedings of the 14th International Conference on Automated Deduction, CADE-14’, Vol. 1249 of LNAI, Springer, Townsville, Australia, pp. 87–100.
Weidenbach, C. (1998), Sorted unification and tree automata, in W. Bibel & P. H. Schmitt, eds,’ Automated Deduction-A Basis for Applications’, Vol. 1 of Applied Logic, Kluwer, chapter 9, pp. 291–320.
Weidenbach, C., Afshordel, B., Brahm, U., Cohrs, C., Engel, T., Keen, E., Theobalt, C. & Topic, D. (1999), System description: Spass version 1.0.0, in H. Ganzinger, ed.,’ 16th International Conference on Automated Deduction, CADE-16’, LNAI, Springer. This volume.
Author information
Authors and Affiliations
Rights and permissions
Copyright information
© 1999 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Weidenbach, C. (1999). Towards an Automatic Analysis of Security Protocols in First-Order Logic. In: Automated Deduction — CADE-16. CADE 1999. Lecture Notes in Computer Science(), vol 1632. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-48660-7_29
Download citation
DOI: https://doi.org/10.1007/3-540-48660-7_29
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-66222-8
Online ISBN: 978-3-540-48660-2
eBook Packages: Springer Book Archive