Publication


Formal Security Analysis with Interacting State Machines

ESORICS 2002


Author: David von Oheimb, Volkmar Lotz
Year: 2002
Publisher: Springer LNCS 2502
CR Classification: D.2.4, F.1.2, H.2.0
CR General Terms: Security, Reliability, Theory, Verification
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), kind of high-level Input/Output Automata. The ISM framework is used to define system models and present them graphically with the AutoFocus tool, to let them be checked for consistency and translated to a representation within the theorem prover Isabelle/HOL (or alternatively to define them directly as Isabelle theory sections), and finally to employ the theorem prover for performing 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 SLE 66 smart card chip and Lowe's fix of the Needham-Schroeder Public-Key Protocol.


Copyright © 2002 Springer-Verlag.
This paper has been published by Springer LNCS.
Preprint version
Slides
Extended version, as part of the NICTA technical report 0401005T-1 (which is also available here).


BibTeX entry:

@inproceedings{FSA-ISM02, author = {Oheimb, David von and Volkmar Lotz}, title = {{Formal Security Analysis with Interacting State Machines}}, booktitle = {Proc.\ of the $7^{\rm th}$ European Symposium on Research in Computer Security (ESORICS)}, editor = {Dieter Gollmann and G{\"u}nter Karjoth and Michael Waidner}, publisher = {Springer}, series = {LNCS}, volume = {2502}, pages = {212--228}, year = 2002, note = {\url{http://ddvo.net/papers/FSA_ISM.html}. Extended version as NICTA TR 0401005T-1.}, 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), kind of high-level Input/Output Automata. The ISM framework is used to define system models and present them graphically with the AutoFocus tool, to let them be checked for consistency and translated to a representation within the theorem prover Isabelle/HOL (or alternatively to define them directly as Isabelle theory sections), and finally to employ the theorem prover for performing 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 SLE 66 smart card chip and Lowe's fix of the Needham-Schroeder Public-Key Protocol.}, CRClassification = {D.2.4, F.1.2, H.2.0}, CRGenTerms = {Security, Reliability, Theory, Verification} } @inproceedings{FSA-ISM04, author = {Oheimb, David von and Volkmar Lotz}, title = {{Formal Security Analysis with Interacting State Machines}}, booktitle = {Proc.\ NICTA Formal Methods Workshop on Operating Systems Verification}, editor = {Gerwin Klein}, publisher = {National ICT Australia, Technical Report 0401005T-1}, address = {Sydney, Australia}, pages = {37--72}, year = 2004, note = {\url{http://ddvo.net/papers/FSA_ISM.html}}, CRClassification = {D.2.4, F.1.2, H.2.0}, CRGenTerms = {Security, Reliability, Theory, Verification} }