Sicherheit von Smart-Card-Anwendungen

Smart Cards sind kompakte Computer, die in den Geldbeutel passen. Sie sind manipulationssichere Speicher und sichere Ausführungseinheiten für Programme. Das heißt, die auf einer Chipkarte gespeicherten Daten können von Unberechtigten nicht verändert oder ausgelesen werden. Dadurch sind Smart Cards ideal für eine Vielzahl von sicherheitskritischen Anwendungen. Obwohl Chipkarten manipulationssicher sind, garantieren sie dennoch alleine noch keine sicheren Anwendungen. Chipkartenanwendungen sind typischerweise verteilte Anwendungen, in denen Kommunikation eine wichtige Rolle spielt. In diesen Anwendungen werden oftmals sicherheitskritische Daten übertragen, seien dies nun vertrauliche Daten von Personen oder elektronische Wirtschaftsgüter. Bekannte Beispiele sind die GeldKarte, ein elektronisches Zahlungsverfahren, bei dem das elektronische Geld vor Vervielfältigung geschützt werden muss und der elektronische Reisepass, dessen biometrische Daten zu schützen sind. Um sicherheitskritische Daten bei der Übertragung zu schützen, kommen kryptographische Protokolle zum Einsatz, die durch die Kombination kryptographischer Primitive entstehen. Die Erfahrung zeigt aber, dass die Entwicklung kryptographischer Protokolle schwierig und fehleranfällig ist. Um Fehler auszuschließen und korrekte Protokolle zu erhalten, kommen oftmals formale Methoden zum Einsatz. Diese Arbeit präsentiert dazu PROSECCO, eine Modellierungstechnik für Chipkartenanwendungen und eine Verifikationstechnik für die in der Anwendung benutzten kryptographischen Protokolle. PROSECCO bietet eine graphische Modellierungssprache für kryptographische Protokolle kombiniert mit einem formalen Modell der Protokolle, welches auf Abstract State Machines (ASM) basiert. Der Theorembeweiser KIV dient als Verifikationswerkzeug für die PROSECCO-Modelle. Dominik Haneberg geboren 1975 in Ulm, studierte von 1995 bis 2000 Informatik mit Nebenfach Wirtschaftswissenschaften an der Universität Ulm. Anschließend arbeitete er bis zur Promotion 2006 als wissenschaftlicher Mitarbeiter bei Prof. Dr. Wolfgang Reif am Lehrstuhl für Softwaretechnik und Programmiersprachen der Universität Augsburg.