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:
<![CDATA[
@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}
}
]]>