Abstract
| Original language | English |
|---|---|
| Title of host publication | Formal Methods for Open Object-Based Distributed Systems |
| Subtitle of host publication | 7th IFIP WG 6.1 International Conference, FMOODS 2005, Athens, Greece, June 15-17, 2005. Proceedings |
| Editors | Martin Steffen, Gianluigi Zavattaro |
| Place of Publication | Berlin, Heidelberg |
| Publisher | Springer |
| Pages | 131-146 |
| Number of pages | 16 |
| ISBN (Electronic) | 978-3-540-31556-8 |
| ISBN (Print) | 978-3-540-26181-0 |
| DOIs | |
| Publication status | Published - Jun 2005 |
| Event | 7th IFIP WG 6.1 International Conference on Formal Methods for Open Object-Based Distributed Systems, FMOODS 2005 - Athens, Greece Duration: 15 Jun 2005 → 17 Jun 2005 Conference number: 7 |
Publication series
| Name | Lecture Notes in Computer Science |
|---|---|
| Publisher | Springer |
| Volume | 3535 |
| ISSN (Print) | 0302-9743 |
| ISSN (Electronic) | 1611-3349 |
Conference
| Conference | 7th IFIP WG 6.1 International Conference on Formal Methods for Open Object-Based Distributed Systems, FMOODS 2005 |
|---|---|
| Abbreviated title | FMOODS |
| Country | Greece |
| City | Athens |
| Period | 15/06/05 → 17/06/05 |
Fingerprint
Keywords
- SCS-Cybersecurity
- Formal verification of security
- OSA/Parlay API
- Industrial test case
Cite this
}
A Formal Security Analysis of an OSA/Parlay Authentication Interface. / Corin, Ricardo; Di Caprio, Gaetano; Etalle, Sandro; Gnesi, Stefania; Lenzini, Gabriele; Moiso, Corrado.
Formal Methods for Open Object-Based Distributed Systems: 7th IFIP WG 6.1 International Conference, FMOODS 2005, Athens, Greece, June 15-17, 2005. Proceedings. ed. / Martin Steffen; Gianluigi Zavattaro. Berlin, Heidelberg : Springer, 2005. p. 131-146 (Lecture Notes in Computer Science; Vol. 3535).Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review
TY - GEN
T1 - A Formal Security Analysis of an OSA/Parlay Authentication Interface
AU - Corin, Ricardo
AU - Di Caprio, Gaetano
AU - Etalle, Sandro
AU - Gnesi, Stefania
AU - Lenzini, Gabriele
AU - Moiso, Corrado
PY - 2005/6
Y1 - 2005/6
N2 - This paper analyzes the security of the Trust and Security Management (TSM) protocol, an authentication protocol which is part of the Parlay/OSA Application Program Interfaces (APIs). Architectures based on Parlay/OSA APIs allow third party service providers to develop new services that can access, in a controlled and secure way, to those network capabilities offered by the network operator. Role of the TSM protocol, run by network gateways, is to authenticate the client applications trying to access and use the network capabilities features offered. For this reason potential security flaws in its authentication strategy can bring to unauthorized use of network with evident damages to the operator and to the quality of the services. This paper shows how a rigorous formal analysis of TSM underlines serious weaknesses in the model describing its authentication procedure. This usually means that also the original system (i.e., the TSM protocol itself) hides the same flaws. The paper relates about the design activity of the formal model, the tool-aided verification performed and the security flaws discovered. This will allow us to discuss about how the security of the TSM protocol can be generally improved.
AB - This paper analyzes the security of the Trust and Security Management (TSM) protocol, an authentication protocol which is part of the Parlay/OSA Application Program Interfaces (APIs). Architectures based on Parlay/OSA APIs allow third party service providers to develop new services that can access, in a controlled and secure way, to those network capabilities offered by the network operator. Role of the TSM protocol, run by network gateways, is to authenticate the client applications trying to access and use the network capabilities features offered. For this reason potential security flaws in its authentication strategy can bring to unauthorized use of network with evident damages to the operator and to the quality of the services. This paper shows how a rigorous formal analysis of TSM underlines serious weaknesses in the model describing its authentication procedure. This usually means that also the original system (i.e., the TSM protocol itself) hides the same flaws. The paper relates about the design activity of the formal model, the tool-aided verification performed and the security flaws discovered. This will allow us to discuss about how the security of the TSM protocol can be generally improved.
KW - SCS-Cybersecurity
KW - Formal verification of security
KW - OSA/Parlay API
KW - Industrial test case
U2 - 10.1007/11494881_9
DO - 10.1007/11494881_9
M3 - Conference contribution
SN - 978-3-540-26181-0
T3 - Lecture Notes in Computer Science
SP - 131
EP - 146
BT - Formal Methods for Open Object-Based Distributed Systems
A2 - Steffen, Martin
A2 - Zavattaro, Gianluigi
PB - Springer
CY - Berlin, Heidelberg
ER -