Formale Modellierung und Analyse einer OrBAC-basierten Sicherheitspolitik am Beispiel der elektronischen Krankenakte

In Krankenhäusern gewinnt die elektronische Datenverarbeitung an immer größerer Bedeutung. Immer mehr Dokumente stehen elektronisch zur Verfügung. Die Dokumentation in einem Krankenhaus erfolgt dementsprechend häufig als elektronische Krankenakte, wobei eine Krankenakte sämtliche Daten umfasst, die im Zusammenhang mit der medizinischen Versorgung eines Patienten stehen. Neben vielen Vorteilen gegebenüber der konventionellen Krankenakte, wie z.B. dem gleichzeitigen gemeinsamen Zugriff von mehreren Personen, bringt die elektronische Krankenakte auch Risiken mit sich. Durch die hohe Verfügbarkeit der elektronischen Krankenakte ist die Gefahr von Missbrauch und Manipulation groß. Da sich die elektronische Krankenakte aus einer Vielzahl sensibler Dokumente zusammensetzt, werden hohe Anforderungen an den Datenschutz beim Umgang mit ihr gestellt. In Deutschland gibt es Gesetze, die regeln, wie weitgehend die Daten in einem Krankenhaus geschützt werden müssen. Um die Datenschutzbestimmungen einzuhalten, müssen Krankenhäuser alle möglichen Maßnahmen treffen. Unter anderem muss ein differenziertes Berechtigungskonzept erarbeitet werden, das auf genaue, saubere und wohldefinierte Weise beschreibt, welche Zugriffe auf die elektronische Krankenakte erlaubt sind und welche nicht. OrBAC (Organization based access control) ist ein Zugriffskontrollmodell, mit dem ebensolche Beschreibungen formuliert werden können. Im Rahmen dieser Diplomarbeit wird eine Zugriffskontrollpolitik mittels OrBAC für ein repräsentatives aber vereinfachtes Beispielkrankenhaus modelliert. Dabei fließen neben den datenschutzrechtlichen Bestimmungen auch organisatorische und strukturelle Rahmenbedingungen des Beispielkrankenhauses in die Zugriffskontrollpolitik mit ein. Ein Krankenhaus kann als ein System betrachtet werden, das während seines Betriebes ein gewisses Verhalten aufweist. Asynchrone Produktautomaten sind ein allgemeines Konzept kommunizierender Automaten. Im Rahmen der Diplomarbeit wird das betrachtete Beispielkrankenhaus und die dort vorherrschende Sicherheitspolitik mittels eines asynchronen Produktautomaten, des Krankenhaus-APAs, modelliert. Dieser asynchrone Produktautomat simuliert das Verhalten des Beispielkrankenhauses unter Beachtung der OrBAC-Zugriffskontrollpolitik. Der Erreichbarkeitsgraph des Krankenhaus-APAs gibt das vollständige Verhalten des Beispielkrankenhauses wieder. Anhand des Erreichbarkeitsgraphen eines asynchronen Produktautomaten kann das Systemverhalten analysiert werden. In der Regel ist jedoch der Erreichbarkeitsgraph zu komplex, als das Eigenschaften an ihm direkt abgelesen werden können. Deshalb werden mittels sogenannter schlichter Homomorphismen Abstraktionen des Systemverhaltens betrachtet. Exemplarisch werden einige ausgewählte Eigenschaften des Beispielkrankenhauses in dieser Diplomarbeit nachgewiesen.