Abstract
In this paper, we describe, how the automated theorem prover SETHEO is used for automatic verification of safety properties of cryptographic protocols. The protocols and their properties are specified using the so-called BAN logic, a multi-sorted modal logic capable of expressing beliefs about secure communication. The resulting formulas and inference rules are transformed into first order predicate logic and processed by the prover SETHEO. Proofs found by SETHEO are then automatically converted into a human-readable form. Experiments with several well-known protocols (e.g., Kerberos, Secure RPC handshake, and CCITT509) revealed very good results: the required properties of the protocols (as described in the literature) could be shown automatically within a few seconds of run-time.
This work is supported by the Deutsche Forschungsgemeinschaft within the habilitation grant Schu908-1/5 and the Sonderforschungsbereich SFB 342, Subproject A5.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
M. Abadi and M. R. Tuttle. A Semantics for a Logic of Authentication. In Proc. of the Tenth Annual ACM Symp. on Principles of Distributed Computing, pages 201–216. ACM press, 1991.
S. H. Brackin. A HOL Extension of GNY for Automatically Analyzing Cryptographic Protocols. In Proc. IEEE Computer Security Foundations Workshop IX. IEEE, 1996.
M. Burrows, M. Abadi, and R. Needham. A Logic of Authentication. In ACM Operating Systems Review 23(5)/Proceedings of the Twelfth ACM Symposium on Operating Systems Principles, 1989.
M. Burrows, M. Abadi, and R. Needham. A Logic of Authentication. ACM Transactions on Computer Systems, 8(1):18–36, 1990.
D. Craigen and M. Saaltink. Using EVES to Analyze Authentication Protocols. Technical Report TR-96-5508-05, ORA Canada, 1996.
J. Geiger. Formale Methoden zur Verifikation kryptographischer Protokolle. Fortgeschrittenenpraktikum, Institut für Informatik, Technische Universität München, 1995. in German.
Chr. Goller, R. Letz, K. Mayr, and J. Schumann. SETHEO V3.2: Recent Developments (System Abstract). In Proc. CADE 12, pages 778–782, 1994.
L. Gong, R. Needham, and R. Yahalom. Reasoning about belief in cryptographic protocols. In Proc. of IEEE Symposium on Security and Privacy, Oakland, Ca., USA, pages 234–248. IEEE, 1990.
M. J. C. Gordon. HOL: A proof generating system for higher-order logic. In G. Birtwistle and P. A. Subrahmanyam, editors, VLSI Specification, Verification and Synthesis, pages 73–128. Kluwer, 1988.
V. Kessler and G. Wedel. AUTLOG — An Advanced Logic of Authentication. In Proc. IEEE Computer Security Foundations Workshop IV, pages 90–99. IEEE, 1994.
D. Kindred and J. Wing. Fast, automatic checking of security protocols. In 2nd USENIX Workshop on Electronic Commerce, pages 41–52, 1996.
R. Letz, K. Mayr, and C. Goller. Controlled Integration of the Cut Rule into Connection Tableau Calculi. Journal Automated Reasoning, (13):297–337, 1994.
R. Letz, J. Schumann, S. Bayerl, and W. Bibel. SETHEO: A High-Performance Theorem Prover. Journal Automated Reasoning, 8(2):183–212, 1992.
D. W. Loveland. Automated Theorem Proving: a Logical Basis. North-Holland, 1978.
W. W. McCune and L. Wos. Experiments in Automated Deduction with Condensed Detachment. Technical report, Argonne National Laboratory, 1991.
C. A. Meadows. Formal verification of Cryptographic Protocols: A Survey. In Proc. AsiaCrypt, 1994.
J. Millen, S. Clark, and S. Freedman. The interrogator protocol security analysis. IEEE Trans. Software Engineering, SE-13(2), 1987.
J. K. Millen. CAPSL: Common Authentication Protocol Specification Language. http://www.mitre.org/research/capsl/, 1996.
M. Moser, O. Ibens, R. Letz, J. Steinbach, Chr. Goller, J. Schumann, and K. Mayr. The Model Elimination Provers SETHEO and E-SETHEO. Special issue of the Journal of Automated Reasoning, 1997. (to appear).
P. G. Neumann. Computer Related Risks. ACM Press, 1995.
J. Schumann. DELTA — A Bottom-up Preprocessor for Top-Down Theorem Provers, System Abstract. In Proc. CADE 12, Springer, 1994.
P. F. Syverson and P. van Oorschot. On Unifying Some Cryptographic Protocol Logics. In Proc. of the IEEE Comp. Soc. Sympos. on Research in Security and Privacy, pages 14–28, 1994.
Klaus Wagner. SIL: Ein SETHEO-basiertes Werkzeug zur Analyse kryptographischer Protokolle. Fortgeschrittenenpraktikum, Technische Universität München, 1997. in German.
Andreas Wolf and Johann Schumann. ILF-SETHEO: Processing Model Elimination Proofs for Natural Language Output (System Description). In Proc. CADE 14, 1997.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1997 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Schumann, J. (1997). Automatic verification of cryptographic protocols with SETHEO. In: McCune, W. (eds) Automated Deduction—CADE-14. CADE 1997. Lecture Notes in Computer Science, vol 1249. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-63104-6_12
Download citation
DOI: https://doi.org/10.1007/3-540-63104-6_12
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-63104-0
Online ISBN: 978-3-540-69140-2
eBook Packages: Springer Book Archive