Bundesamt für Sicherheit in der Informationstechnik

Fallstudie

Formale Analyse der Abläufe zur Erzeugung und Prüfung digitaler Signaturen mit Hilfe von VSE

September 1998

Abstract: Der Einsatz formaler Methoden spielt im wesentlichen bisher im Bereich der IT-Sicherheit nur im Rahmen der Evaluierung/Zertifizierung sicherheitstechnischer Produkte und Komponenten nach ITSEC ab E4 eine Rolle. Ab dieser Stufe ist für die Evaluierung eines entsprechenden Produktes ein formales Sicherheitsmodell notwendig.

Der nutzbringende Einsatz formaler Methoden im Rahmen des Sicherheitsengineerings ist hierauf aber nicht beschränkt. Insbesondere die Behandlung des Zusammenspiels von Abläufen sind ein vielversprechendes Einsatzgebiet formaler Entwicklungstechniken. Diese Fallstudie soll dies dokumentieren. Das ausgewählte Anwendungsszenario ist die Erzeugung und Prüfung digitaler Signaturen.

Mit dem Einsatz digitaler Signaturen wird das Ziel verfolgt, an signierten elektronischen Daten (Dokumenten) sowohl Integritätsverletzungen als auch die Authentizität des Absenders feststellen zu können. Diese und Folgeeigenschaften sind von großem Interesse vor dem Hintergrund, daß zukünftig vermehrt Daten (Dokumente) elektronisch ausgetauscht werden und der Empfänger sich von der Unversehrtheit der erhaltenen Daten (Dokumente) als auch der Authentizität des Absenders überzeugen möchte.

Innerhalb dieser Fallstudie wurde in einer mathematischen Form aufgeschrieben, was bei der Erzeugung und Prüfung digitaler Signaturen eigentlich passiert. Diese mathematische Formulierung

  • vermeidet potentielle Unschärfen einer umgangssprachlichen Formulierung
  • legt genau fest, welche Handlungen möglich sind, worauf diese wirken, sowie in welcher Art und Weise diese wirken und
  • eröffnet spezielle mathematische Analysemöglichkeiten.

Die formale Spezifikation als auch die zugehörige Erläuterung stehen Ihnen als PDF-Dokument zur Verfügung.

Formale Spezifikation in VSE-SL (SigSpez.pdf)

zugehörige Erläuterung (FmSig.pdf)