Formale Methoden für den sicheren Einsatz von Java Chipkarten

点击翻译按钮获取中文摘要

Ziel des Vorhabens ist die Bereitstellung formaler Methoden* zur abstrakten, modularen Spezifikation von Abläufen und Anwendungsszenarien für Java Chipkarten,* zum Nachweis anwendungsspezifischer Sicherheitsziele,* zur Verifikation der JavaCard Applets* und zur Entwicklung einer Sicherheitspolitik für die Koexistenz nachladbarer, kommunizierender, potentiell 'feindlicher' Applets auf einer Java Karte.Hierfür müssen zum einen vorhandene formale Methoden an die Besonderheiten von Java Chipkarten angepaßt, zum anderen neue Methoden entwickelt werden. Die Arbeiten umfassen sowohl theoretische als auch methodische Untersuchungen sowie die Entwicklung einer prototypischen Werkzeugunterstützung. Kleinere Fallstudien dienen als Entwicklungsregulativ. Die Praxistauglichkeit der entstehenden Ergebnisse wird in Zusammenarbeit mit einem Industriepartner (Deutsche Telekom) in einer realistischen Pilotanwendung (z. B. aus dem Bereich Mobilkommunikation) evaluiert. Durch die vereinbarte Zusammenarbeit mit dem Bundesamt für Sicherheit in der Informationstechnik (BSI) soll erreicht werden, daß die entstehende Technologie möglichst direkt für die Evaluierung und Zertifizierung von Chipkarten-Anwendungen nach den hohen Stufen der Kriterienwerke ITSEC bzw. CC eingesetzt werden kann.