Text

Formal correctness of security protocols

---

Contents:

1.Introduction
1.1 Motivation
1.2 Contribution
1.3 Notation
1.4 Contents Outline

2. The Analysis of Security Protocols
2.1 Formal Approaches
2.2 Interpreting the Findings

3. The Inductive Method
3.1 Isabelle
3.2 Theory Hierarchy
3.3 Agents
3.4 Cryptographic Keys
3.5 Compromised Agents
3.6 Messages
3.7 Events
3.8 Traces
3.9 Threat Model
3.10 Operators
3.11 Protocol Model

4. Verifying the Protocol Goals
4.1 The Reliability of the Protocol Model
4.2 Regularity
4.3 Authenticity
4.4 Unicity
4.5 Confidentiality
4.6 Authentication
4.7 Key Distribution

5. The Principle of Goal Availability
5.1 The Need for a Threat Model
5.2 Goal Availability
5.3 Past Incarnations of Goal Availability
5.4 Anticipating the Applications of Goal Availability

6. Modelling Timestamping and Verifying a Classical Protocol 73 6.1 Modelling Guessable Numbers
6.1 Modelling Time
6.2 The BAN Kerberos Protocol
6.3 Modelling BAN Kerberos
6.4 Verifying BAN Kerberos
6.5 A Temporal Modelling of Accidents

7. Verifying a Deployed Protocol
7.1 The Kerberos IV Protocol
7.2 Modelling Kerberos IV
7.3 Verifying Kerberos IV

8. Modelling Agents’ Knowledge of Messages
8.1 Agents’ Knowledge via Trace Inspection
8.2 Agents’ Knowledge via Message Reception
8.3 Revisiting the Guarantees on BAN Kerberos
8.4 Revisiting the Guarantees on Kerberos IV
8.5 Comparing the Two Approaches
8.6 Timestamps Versus Nonces on the Same Design

9. Verifying Another Deployed Protocol
9.1 The Kerberos V Protocol
9.2 Modelling Kerberos V
9.3 Verifying Kerberos V

10. Modelling Smartcards
10.1 Smartcards
10.2 Events
10.3 Agents’ Knowledge
10.4 Threat Model
10.5 Protocol Model

11. Verifying a Smartcard Protocol
11.1 The Shoup-Rubin Protocol
11.2 Modelling Shoup-Rubin
11.3 Verifying Shoup-Rubin
11.4 Verifying Shoup-Rubin-Bella

12. Modelling Accountability
12.1 Challenges for Formal Analysis
12.2 Facing the Challenges

13. Verifying Two Accountability Protocols
13.1 The Non-repudiation Protocol
13.2 The Certified E-mail Protocol
13.3 Discussion

14. Conclusions
14.1 Statistics

A. Proof Script Fragments for Kerberos IV
A.1 Reliability
A.2 Session-key Compromise
A.3 Session-key Confidentiality

B. Proof Script Fragments for Kerberos V
B.1 Unicity
B.2 Unicity Relying on Timestamps
B.3 Key Distribution and Non-injective Agreement

C. Proof Script Fragments for Shoup-Rubin
C.1 Function “initState”
C.2 Function “knows”
C.3 Authentication

D.Proof Script Fragments for Zhou-Gollmann
D.1 Validity of Main Evidence
D.2 Validity of Subsidiary Evidence
D.3 Fairness

---

Availability

Detail Information

Series Title

--

Call Number

005.8 BEL f

Publisher

New York : Springer., 2007

Collation

xviii, 274 hlm.; 24 cm.

Language

English

ISBN/ISSN

9783540681342

Classification

005.8

Content Type

-

Media Type

-

Carrier Type

-

Edition

--

Subject(s)

Computer networks--Security measures

Specific Detail Info

--

Statement of Responsibility

Giampaolo Bella

Other version/related

File Attachment

Comments

---

You must be logged in to post a comment