Spezifikation und Verifikation eines "Separation of Duty"-Szenarios als verbindliche Telekooperation im Sinne des Gleichgewichtsmodells

Das Gleichgewichtsmodell sichert kooperierenden Partnern in offenen Systemen verbindliche Telekooperation zu. Das Gleichgewichtsmodell wurde im Jahre 1993 veröffentlicht und steht am Ende einer Reihe von entwickelten Sicherheitsmodellen. Es stellt sich der Problematik, daß in offenen Systemen keine zentrale Instanz vorhanden ist, die die Integrität von Daten zusichern könnte. Wurde in "herkömmlichen" Sicherheitsmodellen die Abwesenheit von Gefahr als Anspruch an die IT-Sicherheit gestellt, so erweitert das Gleichgewichtsmodell diese Sichtweise durch den Anspruch an die Handhabbarkeit von Gefahr- und Konfliktsituationen. Als Schritt in Richtung dieser neuen Sichtweise der IT-Sicherheit dient das Clark/Wilson-Modell von 1987, welches sich dadurch auszeichnet, als erstes den Menschen als Interpretationsinstanz in ein Sicherheitsmodell mit einbezogen zu haben. An dieser Stelle des Sicherheitsmodells wurde das klassische "Vier-Augen-Prinzip", Separation of Duty, angewendet. In dieser Diplomarbeit wird basierend auf dem Gleichgewichtsmodell eine "Separation of Duty" Telekooperation im Sinne dieser Sicht der IT-Sicherheit mit Produktnetzen formal spezifiziert und den Methoden des SH-Verification Tools verifiziert. Als Beispiel für eine Separation of Duty Kooperation dient ein alltäglicher Beschaffungsantrag in einer Firma. Der Geschäftsführer delegiert die Entscheidung über einen Beschaffungsantrag an die bei den Kooperationspartner Fachabteilungsleiter und Rechnungsprüfer. Eine Bestellung wird nur ausgeführt, wenn beide dem Antrag zustimmen. Gemäß dem Gleichgewichtsmodell kontrollieren sich die Kooperationspartner gegenseitig durch das Sammeln von Beweisen, die die Verpflichtungszustände des jeweils anderen Kooperationspartners, sowie die Erfüllung der eigenen Verpflichtungen belegen. Generell gilt, daß jede Verpflichtungszustandsänderung durch einen Beweis für die Begünstigten kompensiert wird. Unter Benutzung der formalen Methoden des SH-Verification-Tools werden eine Reihe von Eigenschaften des kooperierenden Systems verifiziert. Zunächst wird nachgewiesen, daß die Kooperationsteilnehmer in der gewünschten Art und Weise gemäß der Kooperationspezifikation zusammenarbeiten und das Kooperationsprinzip eingehalten wird. Als zentraler Punkt des Gleichgewichtsmodells wird bewiesen, daß zu jedem Zeitpunkt der Kooperation das Gleichgewicht zwischen Verpflichtungszuständen und Beweisen eingehalten wird. Weiter werden spezielle Lebendigkeitseigenschaften des Systems verifiziert. Insbesondere kann immer wieder ein Beschaffungsantrag gestellt werden. Anhand einer fehlerhaften Spezifikation wird der für die Verifikation wesentliche Begriff der Schlichtheit von Homomorphismen verdeutlicht. Als Erweiterung der Arbeit wird abschließend ein Beispiel für einen ungeregelten Kooperationsabbruch durch Betrugsversuch spezifiziert und verifiziert.

The balance model assures non-repudiation of telecooperation in open systems. This security model, introduced in 1993 by Dr. Rüdiger Grimm, is the last step in a series of proposed security models. It addresses the problem that integrity of data in open systems cannot be assured by a third party. In contrast to "conventional" security models that are limited to locking out danger, the balance model extends this view to the handling of dangerous situations. An important step towards this "new" view of IT-security was the Clark/Wilson security model, introduced in 1987. As one of the first models, it makes use of a human as an interpretation instance using the classic four-eyes-principle Separation of duty. This diploma thesis is based on the balance model and describes a "Separation of duty"-telecooperation, which is formally specified with product nets and verified with methods based on formal language theory. These methods are supported by a tool, the SH-verification tool. The four-eyes-principle is exemplified by an everyday provision-application within a company. This example consists of a two-partner cooperation, in which the "manager" delegates the decision about a provision-application to the two cooperation partners "head of department" and "auditor". An order is placed only if both partners, head of department and auditor, agree to the provision. According to the balance model, the cooperation partners control each other through collection of proofs and administration of the partner's obligations. In general, each change in the state of obligation is compensated by a proof for the favored cooperation partner. Using the formal methods of the SH-verification tool, a number of properties of the cooperation system have been verified. At first it is shown that the cooperation partners work together according to the cooperation specification and the cooperation principle. As a main aspect of the balance model, it is proved that the balance between state of obligation and proofs is kept during the cooperation at any time. In addition, a special kind of liveness property is shown, namely the property that a new provision-application can always be started. The idea of simple homomorphisms - which is fundamental for the verification by the SH-verification tool - is explained using an incorrect specification. Finally, an example for an irregular ending of the cooperation - by fraud - is specified and verified.