Analyzing Network Management Effects with SPIN and cTLA

Since many security incidents of networked computing infrastructures arise from inadequate technical management actions, we aim at a method supporting the formal analysis of those implications which administration activities may have towards system security. We apply the specification language cTLA which supports the modular description of process systems and facilitates the construction of a modeling framework. The framework defines a generic modeling structure and provides re-usable model elements. Due to cTLA’s connection to the temporal logic of actions TLA, formal analysis can resort to symbolic reasoning. Supplementarily, automated analysis can be applied. We focus here on automated analysis. It is supported by translation of cTLA specifications into suitable model descriptions for the powerful model checking tool SPIN. We outline the utilized methods and tools, and report on the modeling and SPIN-based analysis of IP-Hijacking.