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 proceedingConference contributionAcademicpeer-review

    4 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 languageEnglish
    Title of host publicationFormal Methods for Open Object-Based Distributed Systems
    Subtitle of host publication7th IFIP WG 6.1 International Conference, FMOODS 2005, Athens, Greece, June 15-17, 2005. Proceedings
    EditorsMartin Steffen, Gianluigi Zavattaro
    Place of PublicationBerlin, Heidelberg
    PublisherSpringer
    Pages131-146
    Number of pages16
    ISBN (Electronic)978-3-540-31556-8
    ISBN (Print)978-3-540-26181-0
    DOIs
    Publication statusPublished - Jun 2005
    Event7th IFIP WG 6.1 International Conference on Formal Methods for Open Object-Based Distributed Systems, FMOODS 2005 - Athens, Greece
    Duration: 15 Jun 200517 Jun 2005
    Conference number: 7

    Publication series

    NameLecture Notes in Computer Science
    PublisherSpringer
    Volume3535
    ISSN (Print)0302-9743
    ISSN (Electronic)1611-3349

    Conference

    Conference7th IFIP WG 6.1 International Conference on Formal Methods for Open Object-Based Distributed Systems, FMOODS 2005
    Abbreviated titleFMOODS
    CountryGreece
    CityAthens
    Period15/06/0517/06/05

    Fingerprint

    Authentication
    Network protocols
    Application programs
    Defects
    Interfaces (computer)
    Gateways (computer networks)

    Keywords

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

    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). Berlin, Heidelberg: 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 = "6",
    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",

    }

    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 proceedingConference contributionAcademicpeer-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 -

    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