| 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.
|
|
| 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.
|
  | | | | | | | | | | | | | | | | | | | Jun
11 | 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 | Apr
13 |
| Monat | Jun
11 | 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 | Apr
13 | | Startseite | 4 | 4 | | 2 | 1 | 3 | | 1 | | | 7 | 7 | 2 | | | | | 3 | 1 | | PDF | 9 | 22 | 10 | 5 | 9 | 12 | 8 | 13 | 7 | 17 | 11 | 32 | 16 | 15 | 24 | 20 | 17 | 25 | 20 |
Gesamtzahl der Zugriffe seit Jun 2011: - Startseite – 35 (1.84 pro Monat)
- PDF – 292 (15.37 pro Monat)
|
