Cuomo, Nicola
(2010)
Verification of Timed Security Protocols.
[Tesi di dottorato]
(Inedito)
| Tipologia del documento: |
Tesi di dottorato
|
| Lingua: |
English |
| Titolo: |
Verification of Timed Security Protocols |
| Autori: |
| Autore | Email |
|---|
| Cuomo, Nicola | [non definito] |
|
| Data: |
Novembre 2010 |
| Numero di pagine: |
152 |
| Istituzione: |
Università degli Studi di Napoli Federico II |
| Dipartimento: |
Matematica e applicazioni "Renato Caccioppoli" |
| Scuola di dottorato: |
Scienze matematiche e informatiche |
| Dottorato: |
Scienze computazionali e informatiche |
| Ciclo di dottorato: |
22 |
| Coordinatore del Corso di dottorato: |
| nome | email |
|---|
| Ricciardi, Luigi Maria | [non definito] |
|
| Tutor: |
| nome | email |
|---|
| Bonatti, Piero | [non definito] |
|
| Data: |
Novembre 2010 |
| Numero di pagine: |
152 |
| Parole chiave: |
Timed Security Protocols, Formal Methods, Timed Automata |
| Settori scientifico-disciplinari del MIUR: |
Area 01 - Scienze matematiche e informatiche > INF/01 - Informatica |
[error in script]
[error in script]
| Depositato il: |
02 Dic 2010 15:13 |
| Ultima modifica: |
30 Apr 2014 19:44 |
| URI: |
http://www.fedoa.unina.it/id/eprint/8056 |
| DOI: |
10.6092/UNINA/FEDOA/8056 |
Abstract
Security protocols are communication protocols that aim at enforcing security properties through heavy use of cryptographic primitives. These protocols are at the core of security-sensitive applications in a variety of domains (e.g. transportation, health-care, online banking and commerce). Failures are not a option as may cause heavy loss of capitals, time and even humans life. In spite of their apparent simplicity, security protocols are notoriously error-prone and so a number of verification techniques were developed to cope with the verification of such protocols.
However most of the proposed protocol specification languages and verification techniques are limited to cryptographic protocols where quantitative temporal information is not crucial (e.g. delay, timeout, timed disclosure or expiration of information do not affect the correctness of the protocol), and details about some low level timing aspects of the protocol are abstracted away (e.g.: timestamps,
duration of channel delivery, etc.).
In this thesis we face the problem of specifying and verifying security protocols where temporal aspects explicitly appear in the description.
For these kinds of protocols we have designed a specification formalism, which consists of a state-transition graph for each participant of the protocol, with
edges labelled by trigger/action clauses.
The specification of a protocol is translated into a Timed Automaton on which standard techniques of model checking can be exploited (properties to be checked can be expressed in a linear/branching untimed/timed temporal logic).
We also study the protocol insecurity problem for time dependent security protocols with a finite number of sessions, extending to the timed case the results of M. Rusinowitch and M. Turuanistated for the untimed
case. We show that the extension to time and the increased power of the intruder model we propose do not affect the complexity of the problem which remains NP--Complete.
Downloads per month over past year
Actions (login required)
 |
Modifica documento |
