Interacting State Machines (ISMs)

Interacting State Machines are a formalism for abstract modeling and verification of reactive systems. ISMs can be seen as high-level variants of Input/Output Automata or as AutoFocus automata with buffered I/O.

ISM structure

ISMs are typically defined graphically using AutoFocus, translated with a converter tool to Isabelle/HOL theory sections, and mechanically verified within Isabelle/HOL. Integration with ProofGeneral is provided.

Research Papers (and accompanying slides)

David von Oheimb, Georg Walter, and Volkmar Lotz: A Formal Security Model of the Infineon SLE 88 Smart Card Memory Management (the journal version of this paper contains a detailed description of the ISM semantics)
David von Oheimb and Volkmar Lotz: Generic Interacting State Machines and their instantiation with dynamic features
Thomas Kuhn and David von Oheimb: Interacting State Machines for Mobility
David von Oheimb: Interacting State Machines: a stateful approach to proving security
David von Oheimb and Volkmar Lotz: Formal Security Analysis with Interacting State Machines (recommended as an introduction to ISMs)
Sebastian Nanz: Integration of CASE Tools and Theorem Provers: A Framework for System Modeling and Verification with AutoFocus and Isabelle
Thomas Bleher: Secure Information Flow for Interacting State Machines

User Manual including Specifications

Sebastian Nanz and David von Oheimb: Using the ISM Framework

Download

URL: https://ddvo.net/ISM/index.html, Last modified: Thu Nov 19 19:07:34 CET 2009