Abstract
We introduce the ISM approach, a framework for modeling and verifying reactive systems in a formal, even machine-checked, way. The framework has been developed for applications in security analysis. It is based on the notion of Interacting State Machines (ISMs), sort of high-level Input/Output Automata. System models can be defined and presented graphically using the AutoFocus tool. They may be type-checked and translated to a representation within the theorem prover Isabelle or defined directly as Isabelle theories. The theorem prover may be used to perform any kind of syntactic and semantic checks, in particular semi-automatic verification. We demonstrate that the framework can be fruitfully applied for formal system analysis by two classical application examples: the LKW model of the Infineon SLE66 SmartCard chip and Lowe’s fix of the Needham-Schroeder Public-Key Protocol.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Atmel, Hitachi Europe, Infineon Technologies, and Philips Semiconductors. Smartcard IC Platform Protection Profile, Version 1.0, July 2001.
David Aspinall, Healfdene Goguen, Thomas Kleymann, and Dilip Sequeira. Proof General, 1999.
Michael Butler. csp2B: A practical approach to combining CSP and B. In Proceedings of FM’99: World Congress on Formal Methods, pages 490–508, 1999. http://www.dsse.ecs.soton.ac.uk/techreports/99-2.html.
Common Criteria for Information Technology Security Evaluation (CC), Version 2.1, 1999. ISO/IEC 15408.
Danny Dolev and Andrew C. Yao. On the security of public key protocols. IEEE Transactions on Information Theory, IT-29(12):198–208, March 1983.
Clemens Fischer. Combination and implementation of processes and data: from CSP-OZ to Java. PhD thesis, University of Oldenburg, 2000.
Stephen J. Garland and Nancy A. Lynch. The IOA language and toolset: Support for designing, analyzing, and building distributed systems. Technical Report MIT/LCS/TR-762, Laboratory for Computer Science, MIT, August 1998.
Franz Huber, Bernhard Schätz, Alexander Schmidt, and Katharina Spies. Autofocus-a tool for distributed systems specification. In Proceedings FTRTFT’96-Formal Techniques in Real-Time and Fault-Tolerant Systems, volume 1135 of LNCS, pages 467–470. Springer-Verlag, 1996. See also http://autofocus.in.tum.de/index-e.html.
Information Technology Security Evaluation Criteria (ITSEC), June 1991.
Jan Jürjens and Guido Wimmel. Formally testing fail-safety of electronic purse protocols. In Automated Software Engineering. IEEE Computer Society, 2001.
Dilsun Kirli Kaynar. IOA language and toolset, 2001. http://theory.lcs.mit.edu/tds/ioa.html.
Volkmar Lotz, Volker Kessler, and Georg Walter. A Formal Security Model for Microprocessor Hardware. In IEEE Transactions on Software Engineering, volume 26, pages 702–712, August 2000. http://www.computer.org/tse/ts2000/e8toc.htm.
Gavin Lowe. Breaking and fixing the Needham-Schroeder public-key protocol using FDR. In Proceedings of TACAS, volume 1055, pages 147–166. Springer-Verlag, 1996.
Gavin Lowe. A hierarchy of authentication specifications. In PCSFW: Proceedings of The 10th Computer Security Foundations Workshop. IEEE Computer Society Press, 1997.
Nancy Lynch and Mark Tuttle. An introduction to input/output automata. CWI Quarterly, 2(3):219–246, 1989. http://theory.lcs.mit.edu/tds/papers/Lynch/CWI89.html.
David von Oheimb. Interacting State Machines, 2002. Submitted for publication.
David von Oheimb. The Isabelle/HOL implementation of Interacting State Machines, 2002. Technical documentation, available on request.
David von Oheimb, Volkmar Lotz, and Gerog Walter. An interpretation of the LKW model according to the SLE66CX322P security target. Unpublished, January 2002.
Lawrence C. Paulson. Isabelle: A Generic Theorem Prover, volume 828 of LNCS. Springer-Verlag, 1994. For an up-to-date description, see http://isabelle.in.tum.de/.
Lawrence C. Paulson. The inductive approach to verifying cryptographic protocols. Journal of Computer Security, 6:85–128, 1998.
Lawrence C. Paulson, Tobias Nipkow, Markus Wenzel, et al. The Isabelle/HOL library. http://isabelle.in.tum.de/library/HOL/.
Oscar Slotosch et al. Validas Model Validation AG. http://www.validas.de/.
Guido Wimmel and Alexander Wisspeintner. Extended description techniques for security engineering. In M. Dupuy and P. Paradinas, editors, International Conference on Information Security (IFIP/SEC). Kluwer Academic Publishers, 2001.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2002 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
von Oheimb, D., Lotz, V. (2002). Formal Security Analysis with Interacting State Machines. In: Gollmann, D., Karjoth, G., Waidner, M. (eds) Computer Security — ESORICS 2002. ESORICS 2002. Lecture Notes in Computer Science, vol 2502. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45853-0_13
Download citation
DOI: https://doi.org/10.1007/3-540-45853-0_13
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-44345-2
Online ISBN: 978-3-540-45853-1
eBook Packages: Springer Book Archive