edoc-Server der Humboldt-Universität zu Berlin

Dissertation

Autor(en): Matthias Schwan
Titel: Specification and verification of security policies for smart cards
Gutachter: Johannes Köhler; Ernst-Günter Giessmann; Werner Stephan
Erscheinungsdatum: 23.05.2008
Volltext: pdf (urn:nbn:de:kobv:11-10089830)
Fachgebiet(e): Informatik
Schlagwörter (ger): IT-Sicherheit, Chipkarten, Sicherheitspolitik, Formale Verifikation
Schlagwörter (eng): IT Security, Smart Cards, Security Policy, Formal Verification
Einrichtung: Humboldt-Universität zu Berlin, Mathematisch-Naturwissenschaftliche Fakultät II
Zitationshinweis: Schwan, Matthias: Specification and verification of security policies for smart cards; Dissertation, Humboldt-Universität zu Berlin, Mathematisch-Naturwissenschaftliche Fakultät II , publiziert am 23.05.2008, urn:nbn:de:kobv:11-10089830
Metadatenexport: Um den gesamten Metadatensatz im Endnote- oder Bibtex-Format zu speichern, klicken Sie bitte auf den entsprechenden Link. Endnote   Bibtex  
print on demand: Wenn Sie auf dieses Icon klicken, können Sie ein Druckexemplar dieser Publikation bestellen.
Diese Seite taggen: Diese Icons führen auf so genannte Social-Bookmark-Systeme, auf denen Sie Lesezeichen anlegen, persönliche Tags vergeben und Lesezeichen anderer Nutzer ansehen können.
  • connotea
  • del.icio.us
  • Furl
  • RawSugar

Abstract (ger):
Chipkarten sind ein fester Bestandteil unseres täglichen Lebens, das immer stärker von der Zuverlässigkeit derartiger Sicherheitssysteme abhängt, zum Beispiel Bezahlkarten, elektronische Gesundheitskarten oder Ausweisdokumente. Eine Sicherheitspolitik beschreibt die wichtigsten Sicherheitsziele und Sicherheitsfunktionen eines Systems und bildet die Grundlage für dessen zuverlässige Entwicklung. In der Arbeit konzentrieren wir uns auf multi-applikative Chipkartenbetriebssysteme und betrachten neue zusätzliche Sicherheitsziele, die dem Schutz der Kartenanwendungen dienen. Da die Qualität des Betriebssystems von der umgesetzten Sicherheitspolitik abhängt, ist deren Korrektheit von entscheidender Bedeutung. Mit einer Formalisierung können Zweideutigkeiten in der Interpretation ausgeschlossen und formale Beweistechniken angewendet werden. Bisherige formale Verifikationen von Sicherheitspolitiken beinhalten im allgemeinen den Nachweis von Safety-Eigenschaften. Wir verlangen zusätzlich die Betrachtung von Security-Eigenschaften, wobei aus heutiger Sicht beide Arten von Eigenschaften stets getrennt in unterschiedlichen Formalismen verifiziert werden. Die Arbeit stellt eine gemeinsame Spezifikations- und Verifikationsmethodik mit Hilfe von Observer-Modellen vor, die sowohl den Nachweis von Safety-Eigenschaften in einem TLA-Modell als auch den Nachweis von Security-Eigenschaften kryptografischer Protokolle in einem induktiven Modell erlaubt. Da wir alle Spezifikationen und Verifikationen im Werkzeug VSE-II durchführen, bietet das formale Modell der Sicherheitspolitik nicht nur einen abstrakten Blick auf das System, sondern dient gleichzeitig als abstrakte Systemspezifikation, die es in weiteren Entwicklungsschritten in VSE-II zu verfeinern gilt. Die vorgestellte Methodik der Integration beider Systemmodelle in VSE-II führt somit zu einer erhöhten und nachweisbaren Qualität von Sicherheitspolitiken und von Sicherheitssystemen.
Abstract (eng):
Security systems that use smart cards are nowadays an important part of our daily life, which becomes increasingly dependent on the reliability of such systems, for example cash cards, electronic health cards or identification documents. Since a security policy states both the main security objectives and the security functions of a certain security system, it is the basis for the reliable system development. This work focuses on multi-applicative smart card operating systems and addresses new security objectives regarding the applications running on the card. As the quality of the operating system is determined by the underlying security policy, its correctness is of crucial importance. A formalization of it first provides an unambiguous interpretation and second allows for the analysis with mathematical precision. The formal verification of a security policy generally requires the verification of so-called safety properties; but in the proposed security policy we are additionally confronting security properties. At present, safety and security properties of formal system models are verified separately using different formalisms. In this work we first formalize a security policy in a TLA system specification to analyze safety properties and then separately verify security properties using an inductive model of cryptographic protocols. We provide a framework for combining both models with the help of an observer methodology. Since all specifications and proofs are performed with the tool VSE-II, the verified formal model of the security policy is not just an abstract view on the security system but becomes its high level specification, which shall be refined in further development steps also to be performed with the tool. Hence, the integration of the two approaches within the tool VSE-II leads to a new quality level of security policies and ultimately of the development of security systems.
Zugriffsstatistik: Die Daten für die Zugriffsstatistik der einzelnen Dokumente wurden aus den durch AWStats aggregierten Webserver-Logs erstellt. Sie beziehen sich auf den monatlichen Zugriff auf den Volltext sowie auf die Startseite. Die Zugriffsstatistik wird nicht standardisiert erfasst und kann maschinelle Zugriffe enthalten.
 
Bei Formatversionen eines Dokuments, die aus mehreren Dateien bestehen (insbesondere HTML), wird jeweils der monatlich höchste Zugriffswert auf eine der Dateien (Kapitel) des Dokuments angezeigt.
 
Um die detaillierten Zugriffszahlen zu sehen, fahren Sie bitte mit dem Mauszeiger über die einzelnen Balken des Diagramms.
Startseite: 4 Zugriffe PDF: 22 Zugriffe PDF: 10 Zugriffe Startseite: 2 Zugriffe PDF: 5 Zugriffe Startseite: 1 Zugriffe PDF: 9 Zugriffe Startseite: 3 Zugriffe PDF: 12 Zugriffe PDF: 8 Zugriffe Startseite: 1 Zugriffe PDF: 13 Zugriffe PDF: 7 Zugriffe PDF: 17 Zugriffe Startseite: 7 Zugriffe PDF: 11 Zugriffe Startseite: 7 Zugriffe PDF: 32 Zugriffe Startseite: 2 Zugriffe PDF: 16 Zugriffe PDF: 15 Zugriffe PDF: 24 Zugriffe PDF: 20 Zugriffe PDF: 17 Zugriffe Startseite: 3 Zugriffe PDF: 25 Zugriffe Startseite: 2 Zugriffe PDF: 22 Zugriffe Startseite: 2 Zugriffe PDF: 26 Zugriffe Startseite: 1 Zugriffe PDF: 20 Zugriffe Startseite: 2 Zugriffe PDF: 32 Zugriffe Startseite: 3 Zugriffe PDF: 34 Zugriffe Startseite: 3 Zugriffe PDF: 32 Zugriffe Startseite: 3 Zugriffe PDF: 30 Zugriffe Startseite: 1 Zugriffe PDF: 37 Zugriffe Startseite: 3 Zugriffe PDF: 38 Zugriffe Startseite: 5 Zugriffe PDF: 36 Zugriffe PDF: 36 Zugriffe Startseite: 2 Zugriffe PDF: 51 Zugriffe Startseite: 2 Zugriffe PDF: 56 Zugriffe Startseite: 1 Zugriffe PDF: 51 Zugriffe Startseite: 1 Zugriffe PDF: 46 Zugriffe PDF: 52 Zugriffe Startseite: 2 Zugriffe PDF: 50 Zugriffe Startseite: 3 Zugriffe PDF: 46 Zugriffe Startseite: 1 Zugriffe PDF: 28 Zugriffe Startseite: 2 Zugriffe PDF: 33 Zugriffe
Jul
11
Aug
11
Sep
11
Oct
11
Nov
11
Dec
11
Feb
12
Apr
12
May
12
Jun
12
Jul
12
Aug
12
Sep
12
Oct
12
Nov
12
Dec
12
Jan
13
Feb
13
Mar
13
Apr
13
May
13
Jun
13
Jul
13
Aug
13
Sep
13
Oct
13
Nov
13
Dec
13
Jan
14
Feb
14
Mar
14
Apr
14
May
14
Jun
14
Jul
14
Aug
14
Sep
14
Monat Jul
11
Aug
11
Sep
11
Oct
11
Nov
11
Dec
11
Feb
12
Apr
12
May
12
Jun
12
Jul
12
Aug
12
Sep
12
Oct
12
Nov
12
Dec
12
Jan
13
Feb
13
Mar
13
Apr
13
May
13
Jun
13
Jul
13
Aug
13
Sep
13
Oct
13
Nov
13
Dec
13
Jan
14
Feb
14
Mar
14
Apr
14
May
14
Jun
14
Jul
14
Aug
14
Sep
14
Startseite 4   2 1 3   1     7 7 2         3 2 2 1 2 3 3 3 1 3 5   2 2 1 1   2 3 1 2
PDF 22 10 5 9 12 8 13 7 17 11 32 16 15 24 20 17 25 22 26 20 32 34 32 30 37 38 36 36 51 56 51 46 52 50 46 28 33

Gesamtzahl der Zugriffe seit Jul 2011:

  • Startseite – 69 (1.86 pro Monat)
  • PDF – 1019 (27.54 pro Monat)
 
 
Generiert am 24.10.2014, 05:11:51