Es wird ein Verfahren entwickelt, das die formale Modellierung vernetzter IT-Systeme und ihrer Sicherheitsdienste sowie die Darstellung von Verhaltensweisen von Angreifern und von Administrationsprozessen leistet. Die Modellierung basiert auf Zustandstransitionssystemen. Zur Verifikation und Analyse soll Leslie Lamport’s Temporal Logic of Actions (TLA) eingesetzt werden, wobei das Team ihre modulare Spezifikationssprache cTLA verwendet. Es wird auch angestrebt, cTLA-Spezifikationen in Gerard Holzmann’s bekannte Modellierungssprache PROMELA zu übersetzen, so dass das Tool SPIN zur automatisierten Analyse eingesetzt werden kann. Ziel dieser Arbeiten ist es, die mittelbaren Auswirkungen von Angriffen und Administrationsfehlern zu untersuchen.