Publication

Interacting State Machines
- a stateful approach to proving security -

Proceedings of BCS FASec 2002

Author: David von Oheimb
Year: 2002
Publisher: Springer LNCS 2629
Editor: Ali Abdallah, Peter Ryan, Steve Schneider
CR Classification: D.2.4, F.1.2, H.2.0
CR General Terms: Security, Reliability, Theory, Verification
Abstract: We introduce Interacting State Machines (ISMs), a general formalism for abstract modeling and verification of reactive systems. We motivate and explain the concept of ISMs and describe their graphical representation with the CASE tool AutoFocus. The semantics of ISMs is defined using Higher-Order Logic within the theorem prover Isabelle. ISMs can be seen as high-level variants of Input/Output Automata, therefore we give also a semantic translation from ISMs to IOAs. By the ``benchmark'' example of Lowe's fix of the Needham-Schroeder protocol we demonstrate the strengths of the ISM approach to express and prove security properties in a both elegant and machine-checked way.

BibTeX entry:

@inproceedings{DvO-ISM02, author={Oheimb, David von}, title={{Interacting State Machines}: \textit{a stateful approach to proving security}}, booktitle = {Formal Aspects of Security}, editor = {Ali E.\ Abdallah and Peter Ryan and Steve Schneider}, conference = {BCS-FACS FASec 2002}, year = {2002}, publisher = {Springer}, series = {LNCS}, volume = 2629, pages = {15--32}, abstract = { We introduce Interacting State Machines (ISMs), a general formalism for abstract modeling and verification of reactive systems. We motivate and explain the concept of ISMs and describe their graphical representation with the CASE tool AutoFocus. The semantics of ISMs is defined using Higher-Order Logic within the theorem prover Isabelle. ISMs can be seen as high-level variants of Input/Output Automata, therefore we give also a semantic translation from ISMs to IOAs. By the ``benchmark'' example of Lowe's fix of the Needham-Schroeder protocol we demonstrate the strengths of the ISM approach to express and prove security properties in a both elegant and machine-checked way.}, CRClassification = {D.2.4, F.1.2, H.2.0}, CRGenTerms = {Security, Reliability, Theory, Verification}, url = {\url{http://ddvo.net/papers/ISMs.html}} }