Benutzer:Markusbischof/Der Prosecco Ansatz

Einleitung

Im Umfeld von sicherheitskritischen Anwendungen nehmen Smart Cards eine spezielle Rolle ein. Sie bieten einen manipulationssicheren Speicher, durch den eine Anwendung ohne weiteren Aufwand auf eine sichere Hardwareebene aufsetzen kann. Des weiteren sind Smart Cards sehr verbreitet. Die meisten Menschen besitzten eine Bankkarte, noch mehr verwenden eine Smart Card in Form einer SIM-Karte in ihrem Handy. Bei diesen Anwendungen reicht aber die Smart Card mit ihrem sicheren Speicher alleine nicht aus. Die darauf aufsetzende Anwendung muss gewisse Eigenschaften garantieren, die nicht durch die Smart Card gewährleistet werden können. Beispielsweise sollte sich das Handy nur einschalten, wenn auch die korrekte PIN-Nummer eingegeben wurde. Diese Forderungen an die Anwendung müssen mit einer anderen Methodik oder Technik sichergestellt werden. Prosecco stellt eine Methodik dar, die mit Hilfe von formalen Methoden solche Forderungen verifiziert.

Beim Entwurf der Anwendungen stellt sich aber heraus, dass trotz der scheinbar einfachen Funktionen, die umgesetzt werden sollen, viel schief gehen kann. Eines der prominentesten Beispiele ist das Needham-Schroeder-Protokoll ([NED]), das nach Jahren erst mit Hilfe von formalen Methoden als unsicher nachgewiesen werden konnte. Zwar stellt dieses Protokoll keine Anwendung im eigentlichen Sinne dar, aber dennoch zeigt sich, dass im sicherheitskritischen Umfeld mit formalen Methoden viel erreicht werden kann.

Prosecco ist ein durchgängiger Ansatz für die Modellierung von Smart Card-Anwendungen. Smart Card-Anwendungen stellen in vielerlei Hinsicht spezielle Anforderungen. In vielen Fällen werden sie nämlich in einem sicherheitskritischen Umfeld verwendet, da sie durch ihren manipulationssicheren Speicher bereits von Haus aus gegen Angriffe auf Hardwareebene gesichert sind. Allerdings stellt die Sicherheit auf Anwendungsebene einen ebenso wichtigen Teil dar. Prosecco versucht den Entwicklern einer Anwendung vorgefertige Methoden und Werkzeuge zur Verfügung zu stellen, um gewisse Sicherheitseigenschaften für die Anwendung nachzuweisen.

Der Schwerpunkt liegt bei Prosecco auf dem Entwurf der beteiligten Agenten und den ausgetauschten Daten. Ebenso verfügt Prosecco über ein variables Angreifermodell, das es erlaubt, für eine Anwendung spezifische Angreiferfähigkeiten anzugeben.

In der vorliegenden Arbeit wird der Prosecco-Ansatz näher untersucht. Zuerst werden die Hintergründe von Prosecco erläutert. Danach wird das grafische Modell und dessen Umsetzung in das formale Modell untersucht. Es schließt sich eine genauere Betrachtung der entstehenden ASM an. Anschließend wird erläutert, wie mit Prosecco und dem Theorembeweiser KIV die Sicherheit einer Anwendung gezeigt werden kann. Schließlich werden noch zwei Fallstudien, die E-Wallet - und Mondex-Fallstudie, vorgestellt.

Grundlegende Konzepte

Die Verifikation kryptografischer Protokolle

Um ein kryptografisches Protokoll zu entwickeln, bedarf es einiges an Erfahrung. Selbst wenn das Protokoll einen einfachen Eindruck macht und nur aus wenigen Schritten besteht, können schwerwiegende Designfehler vorliegen. Getroffene Annahmen oder nicht getroffene Vorkehrungen bei Multiinstanzen können leicht die Sicherheit eines Protokolls gefährden.

Damit solche Designfehler nicht entstehen, wurde eine Reihe von Designregeln entworfen. Aber auch diese führen nicht immer zu einem sicheren Protokoll. Daher ist es notwendig, eine genaue mathematische Analyse des Protokolls vorzunehmen. Allerdings sollte man dabei immer im Auge behalten, dass die Sicherheit eines Protokolls jeweils davon abhängt, was Sicherheit im Einzelfall bedeutet. Bestimmte Eigenschaften, die ein Protokoll erfüllt, mögen für den einen Sicherheit bedeuten, für den anderen allerdings nicht. Auch ist stets zu beachten, dass ein formales Modell die Wirklichkeit nicht exakt nachstellen kann, und daher nicht alle Annahmen ohne Überprüfung gültig sind.

Ein Ansatz, um das Verfahren der Verifikation etwas zu erleichtern (und dadurch auch die Gefahren zu verkleinern), ist die Verwendung eines standardisierten Angreifermodells. Solch ein Modell hilft bei der Verifikation keine Stelle zu vergessen, an welcher der Angreifer möglicherweise Einfluss auf das Protokoll, bzw. auf die Kommunikation, nehmen könnte. Im nächsten Abschnitt soll das Angreifermodell, das in Prosecco verwendet wird, vorgestellt werden.

Das Angreifermodell

Bei der Verifikation der Sicherheit von Protokollen muss im allgemeinen von einer bösartigen Umwelt ausgegangen werden. Ein Protokoll, das nicht unter der Berücksichtigung möglicher Angriffe entwickelt wurde, bringt keinen Nutzen für denjenigen, der es in einem sicherheitskritischen Umfeld verwenden möchte. Aus diesem Grund wird in den meisten Ansätzen ein Angreifer (Attacker) modelliert, der als Mitspieler im Protokollablauf ebenfalls Aktionen ausführen kann. Typische Fähigkeiten, die ein Angreifer besitzt, sind das Abhören einer Nachricht (read), das Unterdrücken von Nachrichten (suppress) und das Verschicken von beliebigen, verfügbaren Nachrichten an einen Protokollteilnehmer (send). Üblicherweise schreibt man dem Angreifer weitere Fähigkeiten zu, so kann er z.B. abgehörte Nachrichten bis zu einem gewissen Grad auseinandernehmen, um die möglicherweise enthaltenen Teildokumente ebenfalls in sein Wissen aufzunehmen. Dieses Wissen stellt eine transitive Hülle aller Dokumente dar, die der Angreifer jemals erhalten hat, da er bei jedem neuen Dokument, das in sein Wissen kommt, erneut die Analyse durchführt, welche alle im Wissen enthaltenen Dokumente soweit wie möglich dekomponiert. Hört der Angreifer beispielsweise einen Schlüssel ab, so versucht er, alle verschlüsselten Dokumente, die er bis zu diesem Zeitpunkt kennt, mit dem vorliegenden Schlüssel zu entschlüsseln, um an neue Informationen wie ein Passwort oder eine PIN-Nummer zu kommen.

Der Angreifer, der all diese Fähigkeiten besitzt, wird nach seinen Erfindern auch Dolev-Yao-Angreifer ([DOYA]) genannt. Er ist ein maximal indeterministischer Angreifer. Das bedeutet allerdings auch, dass er in manchen Szenarien einen zu mächtigen Angreifer darstellt. In vielen Fällen hat der Angreifer nicht für alle möglichen Verbindungskanäle alle diese Fähigkeiten, sondern nur eine Teilmenge von read, send und suppress. Ein typisches Beispiel ist hier der Geldautomat in der Bank. Es kann davon ausgegangen werden, dass der Angreifer nicht die Kommunikation zwischen der eingeführten Karte und dem Geldautomat abhören kann. Auf der anderen Seite wird bei jeglicher Internetkommunikation davon ausgegangen, dass der Angreifer völlige Kontrolle über das Netz hat.

Für ein bestimmtes Szenario muss also jeweils ein adäquates Angreifermodell gewählt werden. Prosecco unterstützt den Entwickler eines Protokolls mit einem generischen Angreifermodell. Das Modell erlaubt eine präzise Spezifikation der Möglichkeiten des Angreifers basierende auf dem Dolev-Yao-Angreifer und bindet die Spezifikation direkt in das entworfene Anwendungsmodell ein.

Das Kommunikationsmodell

Ein wichtiger Baustein bei der Protokollmodellierung stellt das Modell der ausgetauschten Nachrichten dar. Auf dem Gebiet der Nachrichtenmodellierung existieren schon viele Ansätze. Einer der umfassendsten wurde von Paulson eingeführt und verwendet ([Pau98]). Das in Prosecco verwendete Modell ähnelt Paulsons Ansatz in weiten Teilen. Der verwendete Datentyp document ist eine Abstraktion derjenigen Konzepte, die beim Einsatz von Kryptografie auftreten. Er bildet auch die getroffenen Annahmen der Kryptografie ab. Um die Annahme der perfekten Kryptografie darzustellen, legt der Datentyp beispielsweise fest, dass der Inhalt eines verschlüsselten Dokumentes nur mit dem korrekten Schlüssel entschlüsselt werden kann.

Prosecco im Überblick

Prosecco verwendet eine an UML angelehnte grafische Notation, um die Funktionsweise der Anwendung zu beschreiben. Hierzu werden im Wesentlichen drei Diagrammtypen benötigt.

Ein Diagrammtyp wird verwendet, um die beteiligten Agenten und die verwendeten Datentypen zu beschreiben. Dieser Diagrammtyp wird Agentendiagramm genannt. Ein weiterer Typ (Deploymentdiagramm) dient dazu, die Kommunikationsmöglichkeiten zwischen den Agenten zu beschreiben. Typsicherweise kann ein Agent mehrere Verbindungen mit anderen Agenten aufbauen. Beispielsweise kann ein PC mit mehreren anderen PCs eine Netzwerkverbindung über verschiedene Ports aufbauen. Wäre dieser PC ein Agent in einer Anwendung, so müssten die möglichen Verbindungen im Deploymentdiagramm angegeben werden. Schließlich werden noch Activitydiagramme benötigt. Je ein solches Diagramm bildet ein Protokoll ab. Ein Protokoll entspricht einer einzelnen Funktion in der Anwendung. Beispielsweise müsste bei der E-Wallet-Anwendung für die load- bzw. pay-Funktion jeweils ein Activitydiagramm vorliegen.

Das formale Modell, welches aus den Diagrammen erstellt wird, basiert auf strukturierten algebraischen Spezifikationen und ASMs. Die Erstellung erfolgt schrittweise, beginnend mit dem Agentendiagramm. Die generierten Spezifikationen werden im Theorembeweiser KIV ([KIV99]) in einem Projekt zusammengefasst. Zusätzlich werden dort die notwendigen Basisspezifikationen von Prosecco eingebunden. Näheres zum KIV System und dessen Zusammenspiel mit Prosecco kann [Han06] entnommen werden.

In den folgenden Abschnitten soll jeweils eine kurze Einführung in die soeben genannten Diagrammtypen erfolgen. Anhand eines Beispiels wird der Aufbau und die notwendige Transformation in das formales Modell beschrieben.

Agentendiagramm

Das Agentendiagramm entspricht einem UML-Klassendiagramm ohne Assoziationen. Es werden dort die an der Anwendung beteiligten Agententypen als Klassen modelliert. Jeder Agent hat durch seine Instanzenfelder, die der Klasse hinzugefügt werden können, einen eigenen Zustand. Über diesen Zustand (bzw. über die Felder des Zustandes) können dann beim Beweisen der Sicherheitseigenschaften für die Anwendung Theoreme formuliert und bewiesen werden.

Zusätzlich können anwendungsspezifische Datentypen, die nicht bereits von der Basisbibliothek geliefert werden, definiert und in den Klassen verwendet werden. Allerdings verfügt die Basisbibliothek über die meisten Standarddatentypen wie int oder bool, so dass selten ein eigener Typ benötigt wird.

Die Abbildung zeigt einen Ausschnitt aus dem Agentendiagramm der E-Wallet-Anwendung. Es werden zwei Agententypen definiert. Das cardlet und das terminal. Beide haben Instanzenfelder, die den internen Zustand der jeweiligen Agenten dieses Typs darstellen.

Agentendiagramm der E-Wallet-Agenten

Die Transformation des Diagramms in ein formales Modell beginnt mit der Erzeugung der Agentenidentitäten. Dazu wird die Sorte agent verwendet. Neben den Agenten, die als Klassen im Diagramm mit dem Stereotyp <<agent>> bezeichnet wurden, kommen zu der Sorte immer noch die Agenten user, attacker und fake-cardlet hinzu. Für jeden Agententyp (für jede Klasse) wird ein Konstruktor in der Sorte spezifiziert. Zusätzlich hat jede Instanz der Sorte, also ein einzelner Agent, noch eine eindeutige Nummer. Dadurch können die Agenten unterschieden werden.

Die Sorte agent hat im vorliegenden Beispiel folgende Gestalt:

---

agent = data specification
using nat

agent = cardlet(. .no : nat ;) with cardlet?

| terminal(. .no : nat;) with terminal?

| attacker(. .no : nat;) with attacaker?

| user(. .no : nat;) with user?

| fake-cardlet(. .no : nat;) with fake-cardlet?

;

variables agent, agent0 : agent;

end data specification

---

Neben Instanzenfeldern können im Agentendiagramm auch Konstanten definiert werden. Diese werden gesammelt in einer Spezifikation (contants) mit ihrem jeweiligen Typ und Wert erzeugt.

Um den Zustand der ASM zu initialisieren, wird aus dem Agentendiagramm die ASM-Prozedur INIT erzeugt, welche sicherstellt, dass die Felder des lokalen Zustandes der Agenten den jeweiligen Wert zugewiesen bekommen. Zusätzlich werden an dieser Stelle noch Felder die für die Infrastruktur benötigt werden initialisiert.

Deploymentdiagramm

Prosecco nutzt das Deploymentdiagramm, um die möglichen Kommunikationsverbindungen zwischen den Agenten zu modellieren. Außerdem wird hier festgelegt, welche Chipkartenprogramme auf welchen Chipkarten laufen. Für jeden Agententyp, der eine Verbindung mit einem anderen Agententyp aufnehmen können soll, muss hier eine Assoziation im Diagramm angegeben werden. Über Metainformationen, die über den Stereotyp link der Assoziation beigefügt werden, wird festgelegt, auf welchem Port der jeweilige Agententyp mit seinem Gegenüber kommunizieren kann. Zusätzlich wird für jeden Kommunikationskanal festgelegt, welche Einflussmöglichkeiten der Angreifer auf dem Kanal besitzt. Diese stellen jeweils eine Teilmenge von {read, send, suppress} dar.

Deploymentdiagramm der E-Wallet-Anwendung

Die Abbildung zeigt das Deploymentdiagramm der E-Wallet-Anwendung. Aus diesem Diagramm erzeugt Prosecco eine Reihe von Axiomen, die dem aktuellen Projekt hinzugefügt werden.

Neben der Definition der existierenden Agenten (Prädikat $\exists$agent) wird durch das Diagramm festgelegt, wie viele Agenten der jeweiligen Sorte existieren. Für jeden Typ wird ein Axiom generiert, das die Anzahl angibt. Prosecco übernimmt auch hier einiges an Arbeit. Für manche Typen steht schon im Vorraus fest, wie viele Agenten es gibt. Beispielsweise ist festgelegt, dass es immer Kartenprogramme (cardlets) gibt, die dem Benutzer gehören, und solche, die im Besitz des Angreifers sind. Bei beiden Gruppen existieren jeweils eine feste, endliche Anzahl an Agenten, die von Null verschieden ist.

Weiterhin wird durch die Verbindungen (links) festgelegt, welche Verbindungen die jeweiligen Agenten zueinander aufbauen können. Daraus ergeben sich die gültigen Endpunkte einer Verbindung und die Menge der gültigen Verbindungen. Die Prädikate, die dadurch spezifiziert werden heißen endpoint-ok bzw. conn-ok. Folgender Spezifikationsausschnitt zeigt das Ergebnis der Generierung am Beispiel der E-Wallet-Anwendung:

---

conn-ok :

conn-ok(mk-connection(agent0 $\bigodot$ port0, agent1 $\bigodot$ port1) $\vee$

$\leftrightarrow$ (user?(agent0) $\wedge$ terminal?(agent1) $\wedge$ port1 = 1) $\vee$

(attacker?(agent0) $\wedge$ terminal?(agent1) $\wedge$ port1 = 1) $\vee$

(attacker?(agent0) $\wedge$ terminal?(agent1) $\wedge$ port1 = 2) $\vee$

(attacker?(agent0) $\wedge$ cardlet?(agent1) $\wedge$ port1 = 1) $\vee$

(terminal?(agent0) $\wedge$ port0 = 2 $\wedge$ cardlet?(agent1) $\wedge$ port1 = 1);

---

Die Spezifikation des Prädikates conn-ok sagt aus, Verbindungen zwischen verschiedenen Agententypen möglich sind. Beispielsweise besagt die letzte Zeile der Spezifikation, dass eine Verbindung zwischen dem Terminal an Port 2 und einem Cardlet an Port 1 eine korrekte Verbindung ist.

Auf ähnliche Weise werden die Fähigkeiten des Angreifers in Prädikate gegossen. Für eine Verbindung wird jeweils für suppress, send, eavesdrop festgelegt, ob der Angreifer die jeweilige Fähigkeit besitzt. Für eine genauere Analyse sei an dieser Stelle auf [Han06] verwiesen.

Activitydiagramm

Nachdem durch die letzen zwei Diagrammtypen die statische Sicht auf die Anwendung modelliert wurde, wird mit Hilfe der Activitydiagramme die dynamische Sicht ausgedrückt. Mit Hilfe der aus den Diagrammen bekannten Elemente wird der Protokollablauf für jeweils eine Funktion der Anwendung modelliert. Somit entsteht für jedes mögliche Protokoll der Anwendung ein Diagramm.

Im Folgenden soll auf die Bestandteile eines Activitydiagrammes eingegangen werden.

Die Agenten, die an dem Protokoll teilnehmen, werden durch Swimlanes voneinander getrennt. Geht ein Pfeil von einem Knoten über eine Swimlane zu einem anderen Knoten, so entspricht dies einer Kommunikation über eine durch das Deploymentdiagramm angegebene Verbindung.

Ein einzelner Aktivitätsknoten beinhaltet eine Zustandsänderung des Agenten. Typischerweise sind dies Zuweisungen an Felder des Agenten. Ein Verzweigungsknoten entspricht einem if...then...else...-Konstrukt. Eine Besonderheit ist hier, dass es nur zwei ausgehende Kanten gibt, und eine Kante jeweils mit dem Negat der anderen beschriftet sein muss.

Ein Signal-Sending-Knoten zeigt an, dass ein Agent nun einen Rückgabewert liefert, der über die Swimlanes am Pfeil entlang zu dem entsprechenden Gegenüber übertragen wird.

Als letztes Element enthält ein Activitydiagramm noch einen Initialknoten, der den Protokollablauf startet. An ihm wird eine Bedingung angegeben, die wahr sein muss, damit der Protokollschritt gestartet wird. Beispielsweise kann hier gefordert werden, dass der Protokollschritt erst startet, wenn eine Eingabe mit einem bestimmten Format an einem bestimmten Port anliegt. Dies könnte in der E-Wallet-Anwendung eine Benutzereingabe zum Starten einer Geldübertragung sein.

Die Abbildung zeigt einen kleinen Ausschnitt eines Activitydiagramms aus der E-Wallet-Anwendung. Hier kann man sehr gut die verwendeten Elemente und deren Verwendung erkennen.

Auch bei Activitydiagrammen bietet Prosecco einiges an Infrastruktur, die verwendet werden kann. Felder, die in den Guards und Aktivitätsknoten verwendet werden, stammen direkt aus dem Agentendiagramm. Neben den Feldern können auch entsprechende Funktionen auf den Datentypen der Felder verwendet werden. Welche Funktionen jeweils zur Verfügung stehen, hängt natürlich von dem verwendeten Datentyp ab.

Die Transformation eines Aktivitätsdiagrammes stellt sich etwas komplizierter dar, und soll hier nur in groben Zügen angesprochen werden. Der interessierte Leser sei an dieser Stelle wieder auf [Han06] verwiesen.

Aus allen Activitydiagrammen wird für jeden Agententyp eine separate ASM-Regel erzeugt. Diese beinhaltet für jeden möglichen Protokollschritt des Agenten dessen Ablauf. Verzweigungsknoten erzeugen jeweils ein if...then...else...-Konstrukt, Aktivitäten werden durch die darin enthaltenen Zuweisungen ersetzt, und ein Signal-Sending-Knoten ruft die Bibliotheksfunktion SEND auf, die das Übertragen der Daten übernimmt. Beispielsweise wird bei einer Verzeigung mit Bedingung $\varphi$ und den Folgeknoten $d_1$ und $d_2$ das Konstrukt

---

if $\varphi$ then $d_{1}$ else $d_{2}$

---

erzeugt. Für $d_{1}$ und $d_{2}$ muss die Übersetzung jeweils rekursiv vorgenommen werden.

Nach der Transformation liegen die ASMs als Spezifikation in KIV vor, und es kann mit der Verifikation der gewünschten Sicherheitseigenschaften begonnen werden. Üblicherweise wird zuerst ein Theorem formuliert, das testet, ob erfolgreiche Abläufe möglich sind.

Activitydiagramm der E-Wallet-Anwendung für die Funktion load

Die Basisbibliothek

Die in Prosecco erstellten Modelle bauen alle auf einer strukturierten algebraischen Spezifikation auf. Diese Spezifikation stellt alle möglichen Basisdatentypen und -funktionen zur Verfügung, die bei der Entwicklung von Chipkartenanwendungen notwendig sind. Zusätzlich stehen hier noch einige Funktionen zur Verfügung, die man in seiner Anwendung wiederverwenden kann. Hier ist ebenfalls der Datentyp document spezifiziert.

Die Protokoll-ASM

Die Protokoll-ASM entspricht dem formalen Anwendungsmodell. Sie wird in Prosecco automatisch aus den verschiedenen Diagrammen erzeugt. Die Protokoll-ASM selbst besteht dabei aus einer einzigen ASM-Regel. Die Regel ist so aufgebaut, dass an jeder Stelle, an der eine Entscheidung getroffen werden kann, indeterministisch eine Wahl getroffen wird. Dadurch ist jeder mögliche Durchlauf durch die Anwendung mit der ASM möglich, und somit auch alle möglichen Folgen von Protokollschritten. Durch diese Form der Konstruktion ist nach der Verifikation der Sicherheitseigenschaften gewährleistet, dass es keine Kombination von Protokollschritten in der Anwendung gibt, die die Sicherheitseigenschaften verletzten. Somit ist die Sicherheit der Anwendung nachgewiesen.

Aufbau der Hauptregel

Da die Hauptregel alle möglichen Kombinationen der einzelnen Protokollschritte der Agenten durchläuft, muss die Regel iterativ aufgebaut sein. In einer einzelnen Iteration wird ein Protokollschritt eines Agenten ausgeführt. Welcher Agent welchen Protokollschritt wählt ist dabei indeterministisch. Gibt es an einer Stelle ein Problem, ist durch die verschiedenen Iterationen bekannt, durch welche Kombination von Protokollschritten verschiedener Agenten das Problem verursacht wurde, und man kann entsprechend reagieren.

Die Hauptregel selbst hat die folgende Gestalt:

---

INIT(; as);
while $\neg$ stop do
begin

ASM-STEP(; as);

stop := [?]

end

---

INIT sorgt dafür, dass der Zustand der ASM wohldefiniert ist. Wohldefiniert heißt in diesem Fall, dass die state functions der Anwendung mit den richtigen Werten initial belegt sind.

Die while-Schleife führt so lange das Makro ASM-STEP aus, bis die boolsche Variable stop den Wert true annimmt. Nach jeder Ausführung von ASM-STEP wird die stop-Variable zufällig mit true oder false belegt. Dies sorgt für die bereits erwähnte Erzeugung aller möglichen endlichen Abläufe. Unendliche Abläufe werden an dieser Stelle nicht betrachtet, da ein Angriff, der unendlich viele Protokollschritte benötigt, in der Realität als irrelevant betrachtet wird.

In dem Makro ASM-STEP wird zuerst ein gültiger Agent ausgewählt. Ist dies geschehen, wird in einem nächsten Schritt einer der möglichen Protokollschritte des Agenten ausgeführt.

Nach endlich vielen Durchläufen durch die Schleife wird stop zu true. Danach ist die ASM in einem bestimmten Zustand as'. Da durch die ASM alle möglichen Abläufe der Anwendung abgedeckt sind, beweist man die Sicherheitseigenschaften der Anwendung indem man diese für jeden solchen endlichen, erreichbaren Zustand as' einzeln beweist.

Die eigentlich interessanten Funktionen sind in dem Makro ASM-STEP verborgen. Um den Aufbau des Makros zu verdeutlichen, soll hier der entsprechende E-Wallet ASM-Code angeführt werden. Der Lesbarkeit halber wurden manche Teile ausgeblendet, damit der Aufbau klarer wird.

---

E-WALLET-STEP(...)
begin var asm-step with

...

(asm-step = cardlet-agent-step

$\rightarrow$ $\exists$ agent. cardlet?(agent) $\wedge$ $\exists$agent(agent, lost-cardlets))

(asm-step = terminal-agent-step

$\rightarrow$ $\exists$ agent. terminal?(agent) $\wedge$ $\exists$agent(agent, lost-cardlets))

in begin case

...

asm-step = cardlet-agent-step:

var agent with cardlet?(agent) $\wedge$ $\exists$agent(agent, lost-cardlets)

in CARDLET(...);

asm-step = terminal-agent-step:

var agent with terminal?(agent) $\wedge$ $\exists$agent(agent, lost-cardlets)

in TERMINAL(...);

default:

SKIP;

endcase;

stop := [?]
end

---

Zu Beginn wird der Variablen asm-step ein Wert zugewiesen, der gewissen Einschränkungen unterliegt. Beispielsweise kann der Wert cardlet-agent-step nur dann ausgewählt werden, wenn ein cardlet Agent auch tatsächlich existiert.

Im case-Statement wird dann das jeweilige Makro aufgerufen, welches zuvor durch die asm-step-Variable ausgewählt wurde. Dieses Makro enthält dann die Protokollschritte, die aus den Activitydiagrammen erzeugt wurden, wenn es sich um einen anwendungsspezifischen Protokollschritt handelt. Ansonsten ist das Makro eine Infrastrukturfunktion und bereits in der Basisbibliothek spezifiziert. Im obigen Beispiel werden das CARDLET- bzw. das TERMINAL-Marko aufgerufen. Beide sind anwendungsspezifisch und beschreiben die entsprechenden Funktionen einer Geldkarte bzw. einer Ladestation. Somit liegt für diese Makros jeweils für jede Funktion ein Acitivitydiagramm vor.

Erzeugung der ASM

Prosecco sieht vor, dass aus den verschiedenen Diagrammen das formale Modell entsteht. Dies wird in einem Transformationsschritt von der grafischen Notation in eine formale vorgenommen. Zu beachten ist hierbei, dass eine gewisse Reihenfolge bei der Transformation einzuhalten ist. Der Grund dafür ist, dass nur bekannte Signatursymbole in einer Spezifikation verwendet werden können. Es kann also nicht ein Diagramm nach dem anderen abgearbeitet werden, sondern es liegen komplizierte Zusammenhänge zwischen den Diagrammen vor.

In Kapitel 3 wurde bereits anhand einiger Beispiele verdeutlicht, wie aus den Diagrammen das formale Modell entsteht. Im Folgenden sollen einige ausgewählte Aspekte der Modellierung der verschiedenen Diagramme besprochen werden.

Datentypen im Agentendiagramm

Bei der Definition der Agenten und deren state functions kann auf eine Menge an vordefinierten Variablentypen zurückgegriffen werden. Manche Datentypen sind eher allgemein (z.B. Zahlen oder Mengen), andere sind widerrum speziell bei der Verifikation von kryptografischen Prokollen interessant (z.B. verschlüsselte Dokumente).

Es bleibt bei dem Entwurf der Anwendung natürlich freigestellt, eigene Datentypen zu entwerfen. Diese müssen in Prosecco im Agentendiagramm mit angegeben werden. Ein solcher Datentyp wird im Diagramm als eigene Klasse dargestellt. Ähnlich wie bei einem record-Datentyp können der Klasse weitere Felder hinzugefügt werden. Dies kann allerdings auch später von Hand druchgeführt werden.

Zu jedem vorhandenen Datentyp kann auch eine Menge an Konstanten für diesen Datentyp definiert werden. Die Konstanten werden als Notiz<reef>UML-Notation</ref> an die Klasse angehängt. Die Konstanten können mit einem konkreten Wert des Datentyps belegt werden, allerdings ist es auch möglich, eine Konstante ohne Wert anzugeben. Im formalen Modell ist solch eine Konstante dann unspezifiziert und kann jeden beliebigen Wert annehmen.

Typen und Anzahl der Agenten im Deploymentdiagramm

Zusammen mit dem Agentendiagramm bildet das Deploymentdiagramm die statische Sicht der Anwendung auf das formale Modell ab. Während im Agentendiagramm hauptsächlich die verwendeten Datentypen definiert werden, kommen im Deploymentdiagramm einige anwendungsspezifische Axiome hinzu. Beispielsweise wird angegeben, welche Agententypen wirkliche Kartenprogramme (cardlet-agent) und welche Kartenterminals (terminal-agent) sind. Des weiteren wird jeweils die Anzahl der vorhandenen Agenteninstanzen bestimmt.

Alle Agententypen, die sich innerhalb eines Knotens SmartCard im Deploymentdiagramm befinden, kommen zu der Liste der Agententypen hinzu, für die das Prädikat cardlet-agent wahr wird. Ebenso wird mit den Agententypen verfahren, die sich in einem Knoten Terminal befinden. Die generierten Axiome entsprechen jeweils einer Liste von Agententypen, die über Disjunktionen verbunden sind. Im formalen Modell entstehen die folgenden Axiome (bei n Kartenprogrammen und m Kartenterinals):

---

cardlet-agent:

cardlet-agent(agent) $\leftrightarrow$ $\vee _{i=1}^{n}$ agent-type$_{i}$?(agent);

terminal-agent:

terminal-agent(agent) $\leftrightarrow$ $\vee _{i=n+1}^{n+m}$ agent-type$_{i}$?(agent);

---

Durch Annotationen der Agententypen-Knoten im Deploymentdiagramm wird angegeben, wie viele Agenteninstanzen des jeweiligen Typs in der Anwendung existieren. Für jeden Typ kommt dann entsprechend der Multiplizität eine Konstante zum formalen Modell hinzu, welche genau die Anzahl der verfügbaren Instanzen enthält.

Verbindungen im Deploymentdiagramm

Abschnitt 3.2 führte bereits das Konzept der Verbindungskanäle zwischen verschiedenen Agententypen ein. Diese Kanäle entsprechen Assoziationen im Deploymentdiagramm. Über diese Assoziationen werden die Prädikate endpoint-ok und conn-ok, welche in der Basisbibliothek noch unspezifiziert sind, mit Leben gefüllt. Sie geben an, wie der jeweilige Agententyp kommunizieren kann. Dazu wird an der Assoziation ein Tag eingeführt, welches beschreibt, über welche Kommunikationsendpunkte (endpoints) die Agenten kommunizieren. Mit Hilfe dieser Tags werden dann die notwendigen Axiome generiert, welche jeweils in einer eigenen Spezifikation abgelegt werden.

Da die Kommunikationsstruktur möglichst nahe an der Realität liegen soll, ist beim Entwurf der Kommunikationsstruktur eine gewisse Aufmerksamkeit gefordert. Beispielsweise macht es keinen Sinn, dass ein Kartenprogramm direkt mit dem Benutzer (user) kommunizieren kann. Die Kommunikation darf ausschließlich indirekt über ein Kartenterminal erfolgen.

Mit der Hilfe eines weiteren Tags werden für eine Verbindung die Möglichkeiten des Angreifers beschrieben. Ein Tag enthält dabei eine Teilmenge von {read, send, suppress}. Ist read in der Menge enthalten, so bedeutet dies, dass der Angreifer die Kommunikation abhören kann. Konkret könnte man sich hier z.B. einen gehackten Mailserver vorstellen, der alle empfangenen und gesendeten Nachrichten kopiert und an den Angreifer weiterleitet. send sagt aus, dass der Angreifer selbst Dokumente, die aus seinem Wissen generiert werden können, auf den Kanal legen kann. Er kann somit beliebige Dokumente an die an der Verbindung beteiligten Agententypen schicken. suppress bedeutet, dass der Angreifer Dokumente, die auf dem Kanal verschickt werden, entfernen kann. Er könnte somit jegliche Kommunikation zwischen den Agenten blockieren.

Über dieses Tag werden die entsprechenden Axiome für die Prädikate read, send und suppress in der Spezifikation attacker-axioms erzeugt.

Der Kontrollfluss im Activitydiagramm

Das Activitydiagramm beschreibt die dynamische Sicht auf die Anwendung. Die Übersetzung der Diagramme in ASM-Notation stellt den kompliziertesten Teil bei der Erstellung des formalen Modells dar.

Bei der Übersetzung wird mit den Aktivitätsknoten begonnen. Jede Zuweisung wird in eine entsprechende Zuweisung an eine state function in ASM übersetzt. Danach werden aus dem Kontrollfluss im Activitydiagramm die einzelnen Elemente wie z.B. Bedingungen (if-then-else), Beginnknoten (initial state) oder Sendeknoten (signal-sending-node) übersetzt.

Gleichzeitig wird über die Swimlanes bestimmt, für welchen Agententyp der jeweilige Protokollschritt ausgeführt wird. Dadurch können am Ende alle Protokollschritte, die ein Agententyp ausführen kann, in einer ASM-Regel für den spezifischen Agenten zusammengefasst werden. Dabei wird immer zwischen Kartenagenten und Nicht-Kartenagenten unterschieden, da die Kartenagenten noch zusätzliche Infrastrukturfunktionen in der ASM benötigen.

Am Ende dieses Schrittes liegt eine ASM vor, die das formale Modell der Anwendung darstellt. Mit Hilfe dieses Modelles können nun die Sicherheitseigenschaften der Anwendung formal nachgewiesen werden.

Am Beispiel von E-Wallet entstehen durch diesen Transformationsschritt z.B. die CARDLET- und TERMINAL-Markos, welche in Abschnitt 4.1 lediglich angesprochen wurden.

Verifikationsansatz

Für die Verifikation des formalen Modells ist Prosecco eng mit dem Theorembeweiser KIV ([KIV99]) verbunden. Das transformierte Modell liegt in KIV als DL-Programm vor und kann mit den dort vorhandenen Beweistechniken verifiziert werden. Die Grundidee ist das Eleminieren von Programmcode. Nacheinander werden die Zeilen des DL-Programmes abgearbeitet, und die entsprechenden Konstrukte in DL übersetzt. Eine Zuweisung wird beispielsweise über die assign right-Kalkülregel eleminiert. Für Scheifen und rekursive Prozeduren wird Induktion eingesetzt. Diese Technik nennt sich symbolisches Ausführen.

Typisch für Sicherheitseigenschaften ist, dass eine Eigenschaft in jedem Schritt der Anwendung gelten soll. Dazu werden Invariantenbeweise verwendet. Eine Invariante für könnte z.B. sein, dass sie geheime Schlüssel nie in die Hände des Angreifers gelangt. Um eine Invariante zu beweisen, wird in KIV ein Theorem formuliert, welches aussagt, dass wenn die Invariante vor dem Ausführen des Programmes gilt, sie auch nach jedem beliebigen Durchlauf durch das Programm gelten muss.

Neben einer Invariante für eine Sicherheitseigenschaft der Anwendung existieren in den meisten Fällen noch einige weitere Bedingungen, die zu jedem Zeitpunkt bei der Programmabarbeitung gelten müssen. Diese können ebenso beim Beweis der Sicherheitseigenschaft helfen. Hier wird z.B. gefordert, dass alle Variablen in der Anwendung einen wohldefinierten Wert besitzen. Diese Art der Bedingung an die Anwendung kann meistens nicht im Vorraus erkannt werden. Oft ergeben sich diese Eigenschaften, die die Anwendung zusätzlich garantieren muss während des Beweisens der Sicherheitseigenschaft. Daher ist es üblich, dass diese Bedingungen sukksessive zur Invariante hinzukommen.

Während des Beweisens stehen in KIV einige Heuristiken zur Verfügung, die viel Arbeit abnehmen. Manche Beweise können sogar vollautomatisch durchgeführt werden. Dazu sind auch geeignete Simplfierregeln nützlich. Durch sie können vorliegende Beweisziele mit bereits bewiesenen Eigenschaften verglichen werden und gegebenenfalls gleich geschlossen werden.

Fallstudien

Mit der Unterstützung von Prosecco wurden bereits einige Fallstudien durchgeführt. Im Folgenden sollen hier zwei davon näher betrachtet werden. Diese zwei wurden deswegen ausgewählt, weil sie sich in dem Maße, wie sie Prosecco verwenden, deutlich unterscheiden. Der erste, die E-Wallet-Fallstudie, beinhaltet den vollen Zyklus, den Prosecco vorschlägt, angefangen von den grafischen Diagrammen bis hin zur Transformation derselben in ASM-Code. Die zweite, die Mondex-Fallstudie, wurde ohne die grafischen Diagramme entworfen. Die ASM-Regeln für die Agenten sowie die fehlenden Axiome in der Basisbibliothek wurden lediglich mit Hilfe einer Vorlage erstellt.

E-Wallet

E-Wallet modelliert eine einfache Geldbörse. Man kann einen Geldbetrag auf der Börse speichern, und ihn auch wieder abheben. Das Be- und Entladen wird jeweils an den sogenannten Lade- und Bezahlstationen, durchgeführt.

Die Sicherheitseigenschaft, die für diese Fallstudie nachgewiesen wurde, sagt aus, dass kein Betrug möglich ist. Betrug heißt in diesem Fall, dass mehr Punkte von den Karten abgebucht wurden, als bei den Stationen geladen wurde. Es wurden also an einer Stelle Punkte aus dem Nichts erzeugt. Um die Eigenschaft formal zu fassen, müssen die geladenen (collected) und abgebuchten (issued) Punkte aller Terminals sowie die aktuell gespeicherten (value) Punkte aller im Umlauf befindlichen Karten in Beziehung gesetzt werden. Dies drückt die folgende Formal aus:

$\sum _{t\;\in \;Terminals}collected(t)+\sum _{c\;\in \;Cardlets}value(c)\leq \sum _{t\;\in \;Terminals}issued(t)$

Die Fallstudie durchlief alle Schritte, die von Prosecco für eine formale Verifikation von Smart Card-Anwendungen vorgeschlagen wurden. Zu Beginn wurde die entsprechenden Diagramme entworfen. Anschließend erfolgte die Transformation in ASM-Code. Schließlich wurde mit Hilfe von KIV die gewünschte Sicherheitseigenschaft als korrekt nachgewiesen.

Mondex

In der Mondex-Fallstudie wird ebenfalls eine Geldbörse modelliert. Diese unterscheidet sich allerdings in dem Sinne von der E-Wallet Geldbörse, da es möglich ist, Geld von einer Börse auf die andere zu übertragen. Es existieren also keine Lade- bzw. Bezahlstationen.

Für die Mondex-Geldbörse wurde ausgehend von einem Prosecco-Modell eine Java Card-Implementierung entwickelt. Anschließend wurde die Korrektheit des daraus resultierenden Refinements nachgewiesen. Im Modell selbst wurden zwei Komponenten entwickelt. Einmal ein Terminal, dass das Übertragen des Geldes zwischen zwei Geldbörse koordiniert, und dann die Geldbörse selbst. Der Benutzer und der Angreifer wurden von Prosecco übernommen. Eine Besonderheit an dieser Fallstudie ist, dass keine Diagramme entworfen wurden. Es wurde dirket mit Vorlage der E-Wallet-Fallstudie der ASM-Code implementiert.

Zusammenfassung und Ausblick

Durch Prosecco ist es möglich, die Sicherheit von Smart Card-Anwendungen mathematisch exakt nachzuweisen. Die ist interessant, da gerade im Bereich sicherheitskritischer Anwendungen die Chipkarten mit ihrem manipulationssicheren Speicher einen hohen Stellenwert einnehmen. Sie können z.B. sehr gut für Zugangskontrollsysteme oder Bezahlsyteme verwendet werden.

Da Smart Card-Anwendungen inhärent verteilt sind, spielt in jeder dieser Anwendungen die Kommunikation eine sehr wichtige Rolle. Neben der Integrität und Vertraulichkeit der versendeten Nachrichten ist es ebenso wichtig, dass die Karte funktional korrekt arbeitet. Das heißt, dass sie die intendierten Funktionen, selbst bei möglichen Angriffen oder fehlerhaft übertragenen Nachrichten, immer ausführt.

Prosecco schlägt ein durchgängiges Konzept vor, um die Sicherheit von Smart Card-Anwendungen zu beweisen. Zu Beginn werden an UML angelehnte Diagramme entworfen, welche die verwendeten Datentypen, die Kommunikationswege und den internen Zustand der Agenten definieren. Wichtig ist hier, dass das Angreifermodell sehr flexibel an die Anwendung angepasst werden kann. Für jeden Kommunikationsweg kann separat angegeben werden, welche Möglichkeiten der Angreifer hat. Das durch eine Transformation entstehende formale Modell kann mit Hilfe des Theorembeweisers KIV als sicher bezüglich der gewünschten Eigenschaften verifiziert werden. Gerade durch diese enge Verbindung mit einem starken formalen Werkzeug ist die Verifikation um vieles leichter.

Als nächste Schritte sind für Prosecco geplant, zusätzliche Beweisunterstützungen in das KIV System zu integrieren. Dazu zählen neben angepassten Heuristiksätzen z.B. auch die Verbesserung der Vorschlagsberechnung für Variableninstanzen. Ein weiterer großer Schritt ist die automatische Generierung des formalen Modells aus den grafischen Diagrammen. Dies schafft die Verbindung von der informellen Sicht der Diagramme hin zur formalen Sicht. Durch solch eine automatische Generierung wären auch gleichzeitig viele Fehlerquellen beseitigt, da das korrekte Formulieren der ASM auch mit Hilfe einer Vorlage ein kompliziertes Unterfangen ist.

Literatur

• [Han06] Haneberg D.: Sicherheit von Smart Card-Anwendungen. Logos Verlag, Berlin 2006, ISBN 978-3-8325-1597-3.
• [Jür02] Jürjens J.: UMLsec: Extending UML For Secure Systems Developement. Springer Verlag, Dresden 2002.
• [Pau98] Paulson L.: The Inductive Approach To Verifying Cryptographic Protocols. Journal of Computer Security, 1998
• [KIV99] Balser M., Reif W., Schellhorn G., Stenzel K.: KIV 3.0 For Provably Correct Systems. Springer Verlag, 1999, ISBN 3-540-66462-9
• [ASM] Börger, E., Stärk R. F.: Abstract State Machines - A Method For High-Level System Design And Analysis. Springer Verlag, Berlin 2003, ISBN 978-3540007029.
• [DOYA] Dolev D., Yao A.C.: On The Security Of Public Key Protocols. IEEE, 1981
• [NED] Lowe G.: Breaking And Fixing The Needham-Schroeder Public-Key Protocol Using FDR. Springer Verlag, 1996