Specification and verification of security policies for smart cards [Elektronische Ressource] / von Matthias Schwan

-

English
223 pages
Obtenez un accès à la bibliothèque pour le consulter en ligne
En savoir plus

Description

Specification and Verification ofSecurity Policies for Smart CardsDISSERTATIONzur Erlangung des akademischen Gradesdoctor rerum naturalium(Dr. rer. nat.)im Fach Informatikeingereicht an derMathematisch-Naturwissenschaftlichen Fakultät IIHumboldt-Universität zu BerlinvonHerr Dipl.-Inf. Matthias Schwangeboren am 08.08.1973Präsident der Humboldt-Universität zu Berlin:Prof. Dr. Christoph MarkschiesDekan der Mathematisch-Naturwissenschaftlichen Fakultät II:Prof. Dr. Wolfgang CoyGutachter:1. Prof.Dr.Johannes Köbler2. Prof.Dr.Ernst-Günter Giessmann3. PD Dr.habil.Werner StephanTag der mündlichen Prüfung: 13.Februar 2008iiAbstractSecurity systems that use smart cards are nowadays an important part ofour daily life, which becomes increasingly dependent on the reliability ofsuch systems, for example cash cards, electronic health cards or identificationdocuments. Since a security policy states both the main security objectivesand the security functions of a certain security system, it is the basis for thereliable system development.This work focuses on multi-applicative smart card operating systems andaddresses new security objectives regarding the applications running on thecard. As the quality of the operating system is determined by the underly-ing security policy, its correctness is of crucial importance. A formalizationof it first provides an unambiguous interpretation and second allows for theanalysis with mathematical precision.

Sujets

Informations

Publié par
Publié le 01 janvier 2008
Nombre de lectures 19
Langue English
Poids de l'ouvrage 3 Mo
Signaler un problème

Specification and Verification of
Security Policies for Smart Cards
DISSERTATION
zur Erlangung des akademischen Grades
doctor rerum naturalium
(Dr. rer. nat.)
im Fach Informatik
eingereicht an der
Mathematisch-Naturwissenschaftlichen Fakultät II
Humboldt-Universität zu Berlin
von
Herr Dipl.-Inf. Matthias Schwan
geboren am 08.08.1973
Präsident der Humboldt-Universität zu Berlin:
Prof. Dr. Christoph Markschies
Dekan der Mathematisch-Naturwissenschaftlichen Fakultät II:
Prof. Dr. Wolfgang Coy
Gutachter:
1. Prof.Dr.Johannes Köbler
2. Prof.Dr.Ernst-Günter Giessmann
3. PD Dr.habil.Werner Stephan
Tag der mündlichen Prüfung: 13.Februar 2008iiAbstract
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 underly-
ing 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 proper-
ties. 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 specifi-
cation to analyze safety properties and then separately verify security prop-
erties using an inductive model of cryptographic protocols. We provide a
framework for combining both models with the help of an observer method-
ology. 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.
Keywords:
IT Security, Smart Cards, Security Policy, Formal VerificationivZusammenfassung
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 Ausweisdoku-
mente. Eine Sicherheitspolitik beschreibt die wichtigsten Sicherheitsziele und
Sicherheitsfunktionen eines Systems und bildet die Grundlage für dessen zu-
verlässige Entwicklung.
In der Arbeit konzentrieren wir uns auf multi-applikative Chipkarten-
betriebssysteme und betrachten neue zusätzliche Sicherheitsziele, die dem
Schutz der Kartenanwendungen dienen. Da die Qualität des Betriebssys-
tems von der umgesetzten Sicherheitspolitik abhängt, ist deren Korrektheit
von entscheidender Bedeutung. Mit einer Formalisierung können Zweideu-
tigkeiten in der Interpretation ausgeschlossen und formale Beweistechniken
angewendet werden. Bisherige formale Verifikationen von Sicherheitspoliti-
ken 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 unterschied-
lichen Formalismen verifiziert werden.
DieArbeitstellteinegemeinsameSpezifikations-undVerifikationsmetho-
dikmitHilfevonObserver-Modellenvor,diesowohldenNachweisvonSafety-
Eigenschaften in einem TLA-Modell als auch den Nachweis von Security- kryptografischer Protokolle in einem induktiven Modell er-
laubt. 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 Systemmo-
delle in VSE-II führt somit zu einer erhöhten und nachweisbaren Qualität
von Sicherheitspolitiken und von Sicherheitssystemen.
Schlagwörter:
IT-Sicherheit, Chipkarten, Sicherheitspolitik, Formale VerifikationviAcknowledgments
First of all I would like to thank my advisers Prof. Johannes Köbler from
Humboldt-University and Prof. Ernst-Günter Giessmann from T-Systems
for their constant and inspiring support during the preparation of this thesis
and beyond. To work with them has been very diversified and exciting.
Because this work has been funded by Deutsche Telekom AG and is
1
strongly related to the R&D project Verisoft run at T-Systems I had the
great chance to experience research in an industrial context. In this regard I
would like to express my thanks to Dr.Gunter Laßmann and the whole secu-
rity group at T-Systems who all gave valuable advice and a fruitful working
environment.
My special thanks also go to PD Dr.Werner Stephan from German Re-
search Center for Artificial Intelligence (DFKI) in Saarbrücken for his help-
ful suggestions and for refereeing this thesis. He and his group, particularly
Dr.Georg Rock, Lassaad Cheikhrouhou and Bruno Langenstein, were the
main partners in the project and of my work and gave maximum support.
Moreover, without the encouragement of my family and friends this work
would not have been finished yet, thank you all.
1http://www.verisoft.de
viiviiiContents
Contents ix
List of Figures xiii
List of Tables xv
1 Introduction 1
1.1 Overview . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 1
1.2 Overall structure . . . . . . . . . . . . . . . . . . . . . . . . . 5
1.3 Publications . . . . . . . . . . . . . . . . . . . . . . . . . . . . 6
2 Case studies 7
2.1 Multilevel access control . . . . . . . . . . . . . . . . . . . . . 7
2.2 Airline loyalty program . . . . . . . . . . . . . . . . . . . . . . 9
2.3 Electronic signatures and biometrics . . . . . . . . . . . . . . 10
2.3.1 Electronic signature requirements . . . . . . . . . . . . 10
2.3.2 Biometric identification systems . . . . . . . . . . . . . 11
2.3.3 The BioSig example . . . . . . . . . . . . . . . . . . . 12
2.4 Electronic health card . . . . . . . . . . . . . . . . . . . . . . 14
2.5 Conclusion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 16
3 Smart card security requirements 17
3.1 Security policies . . . . . . . . . . . . . . . . . . . . . . . . . . 17
3.2y threats for smart cards . . . . . . . . . . . . . . . . . 19
3.3 Security objectives of smart cards . . . . . . . . . . . . . . . . 23
4 Survey of smart card designs 27
4.1 Java Card . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
4.2 Multos . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
4.3 SMaCOS . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
4.4 BasicCard . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
4.5 Limitations of the security policies . . . . . . . . . . . . . . . 33
ix5 The extended security policy 37
5.1 The SMaCOS security model . . . . . . . . . . . . . . . . . . 37
5.1.1 Communication channels . . . . . . . . . . . . . . . . . 40
5.1.2 Loading new applications . . . . . . . . . . . . . . . . . 43
5.2 External applications and devices . . . . . . . . . . . . . . . . 44
5.2.1 The basic idea . . . . . . . . . . . . . . . . . . . . . . . 44
5.2.2 Electronic signatures . . . . . . . . . . . . . . . . . . . 45
5.2.3 The extended security model . . . . . . . . . . . . . . . 47
5.3 Summary of security functions . . . . . . . . . . . . . . . . . . 49
5.4 Application to the BioSig example . . . . . . . . . . . . . . . . 52
5.5 Alternative design decisions . . . . . . . . . . . . . . . . . . . 58
5.6 Conclusion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 60
6 The analysis of security policies 63
6.1 Security triangle relations . . . . . . . . . . . . . . . . . . . . 63
6.2 Application of formal methods . . . . . . . . . . . . . . . . . . 66
6.2.1 Formal models of security policies . . . . . . . . . . . . 67
6.2.2 Formal analysis of cryptographic protocols . . . . . . . 70
6.2.3 Safety versus security properties? . . . . . . . . . . . . 72
6.3 Security evaluation criteria . . . . . . . . . . . . . . . . . . . . 75
6.4 Conclusion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 84
7 Safety properties of state-based systems 87
7.1 The Temporal Logic of Actions (TLA) . . . . . . . . . . . . . 87
7.1.1 The basic formalism . . . . . . . . . . . . . . . . . . . 88
7.1.2 System verification . . . . . . . . . . . . . . . . . . . . 93
7.2 A smart card system model . . . . . . . . . . . . . . . . . . . 96
7.2.1 System specification . . . . . . . . . . . . . . . . . . . 97
7.2.2 Safety properties . . . . . . . . . . . . . . . . . . . . . 102
7.3 Formalization in VSE-II . . . . . . . . . . . . . . . . . . . . . 104
7.3.1 Verification Support Environment VSE-II . . . . . . . 104
7.3.2 Formalization of the system components . . . . . . . . 105
7.3.3 Fairness and concurrency . . . . . . . . . . . . . . . . . 113
7.3.4 Verification of safety properties . . . . . . . . . . . . . 115
7.4 Conclusion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 121
8 Security properties of protocols 123
8.1 Paulson’s inductive approach . . . . . . . . . . . . . . . . . . . 123
8.1.1 The basic formalism . . . . . . . . . . . . . . . . . . . 124
8.1.2 Protocol verification . . . . . . . . . . . . . . . . . . . 126
8.2 A smart card authentication protocol . . . . . . . . . . . . . . 128
x