A Formal Security Analysis of an OSA/Parlay Authentication Interface

Ricardo Corin; Gaetano Di Caprio; Sandro Etalle; Stefania Gnesi; Gabriele Lenzini; Corrado Moiso

doi:10.1007/11494881_9

A Formal Security Analysis of an OSA/Parlay Authentication Interface

Ricardo Corin, Gaetano Di Caprio, Sandro Etalle, Stefania Gnesi, Gabriele Lenzini, Corrado Moiso

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

9 Downloads (Pure)

Abstract

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.

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	https://doi.org/10.1007/11494881_9
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/Territory	Greece
City	Athens
Period	15/06/05 → 17/06/05

Keywords

SCS-Cybersecurity
Formal verification of security
OSA/Parlay API
Industrial test case

Access to Document

10.1007/11494881_9

Corin2005formalAccepted author version, 206 KB

Cite this

Corin, R., Di Caprio, G., Etalle, S., Gnesi, S., Lenzini, G., & Moiso, C. (2005). A Formal Security Analysis of an OSA/Parlay Authentication Interface. In M. Steffen, & G. Zavattaro (Eds.), Formal Methods for Open Object-Based Distributed Systems: 7th IFIP WG 6.1 International Conference, FMOODS 2005, Athens, Greece, June 15-17, 2005. Proceedings (pp. 131-146). (Lecture Notes in Computer Science; Vol. 3535). Springer. https://doi.org/10.1007/11494881_9

Corin, Ricardo ; Di Caprio, Gaetano ; Etalle, Sandro ; Gnesi, Stefania ; Lenzini, Gabriele ; Moiso, Corrado. / A Formal Security Analysis of an OSA/Parlay Authentication Interface. Formal Methods for Open Object-Based Distributed Systems: 7th IFIP WG 6.1 International Conference, FMOODS 2005, Athens, Greece, June 15-17, 2005. Proceedings. editor / Martin Steffen ; Gianluigi Zavattaro. Berlin, Heidelberg : Springer, 2005. pp. 131-146 (Lecture Notes in Computer Science).

@inproceedings{c288b942784c4370bd68c65b272bb764,

title = "A Formal Security Analysis of an OSA/Parlay Authentication Interface",

abstract = "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.",

keywords = "SCS-Cybersecurity, Formal verification of security, OSA/Parlay API, Industrial test case",

author = "Ricardo Corin and {Di Caprio}, Gaetano and Sandro Etalle and Stefania Gnesi and Gabriele Lenzini and Corrado Moiso",

year = "2005",

month = jun,

doi = "10.1007/11494881_9",

language = "English",

isbn = "978-3-540-26181-0",

series = "Lecture Notes in Computer Science",

publisher = "Springer",

pages = "131--146",

editor = "Martin Steffen and Gianluigi Zavattaro",

booktitle = "Formal Methods for Open Object-Based Distributed Systems",

address = "Netherlands",

note = "7th IFIP WG 6.1 International Conference on Formal Methods for Open Object-Based Distributed Systems, FMOODS 2005, FMOODS ; Conference date: 15-06-2005 Through 17-06-2005",

}

Corin, R, Di Caprio, G, Etalle, S, Gnesi, S, Lenzini, G & Moiso, C 2005, A Formal Security Analysis of an OSA/Parlay Authentication Interface. in M Steffen & G Zavattaro (eds), Formal Methods for Open Object-Based Distributed Systems: 7th IFIP WG 6.1 International Conference, FMOODS 2005, Athens, Greece, June 15-17, 2005. Proceedings. Lecture Notes in Computer Science, vol. 3535, Springer, Berlin, Heidelberg, pp. 131-146, 7th IFIP WG 6.1 International Conference on Formal Methods for Open Object-Based Distributed Systems, FMOODS 2005, Athens, Greece, 15/06/05. https://doi.org/10.1007/11494881_9

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

N1 - Conference code: 7

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

T2 - 7th IFIP WG 6.1 International Conference on Formal Methods for Open Object-Based Distributed Systems, FMOODS 2005

Y2 - 15 June 2005 through 17 June 2005

ER -

Corin R, Di Caprio G, Etalle S, Gnesi S, Lenzini G, Moiso C. A Formal Security Analysis of an OSA/Parlay Authentication Interface. In Steffen M, Zavattaro G, editors, Formal Methods for Open Object-Based Distributed Systems: 7th IFIP WG 6.1 International Conference, FMOODS 2005, Athens, Greece, June 15-17, 2005. Proceedings. Berlin, Heidelberg: Springer. 2005. p. 131-146. (Lecture Notes in Computer Science). https://doi.org/10.1007/11494881_9

A Formal Security Analysis of an OSA/Parlay Authentication Interface

Abstract

Publication series

Conference

Keywords

Access to Document

Fingerprint

Cite this