A Formal Security Analysis of an OSA/Parlay Authentication Interface

R. Corin, G. Di Caprio, S. Etalle, S. Gnesi, Gabriele Lenzini, C. Moiso

    Research output: Book/ReportReportProfessional

    2 Citations (Scopus)
    54 Downloads (Pure)

    Abstract

    We report on an experience in analyzing the security of the Trust and Security Management (TSM) protocol, an authentication procedure within the OSA/Parlay Application Program Interfaces (APIs) of the Open Service Access and Parlay Group. The experience has been conducted jointly by research institutes, experienced in security, and an industry experts in telecommunication networking. OSA/Parlay APIs are designed to enable the creation of telecommunication applications outside the traditional network space and business model. Network operators consider the OSA/Parlay architecture promising for stimulating the development of web-service applications by third party providers which are not necessarily expert in telecommunication and security. The TSM protocol is executed by the gateways to OSA/Parlay networks; its role is to authenticate client applications trying to access the interfaces of some object representing an offered network capability. For this reason, potential security flaws in the TSM authentication strategy can cause the unauthorized use of network with evident damages to the operator and to the quality of services. This paper reports the rigorous formal analysis of the TSM specification originally given in UML; the design activity of the formal model, the tool-aided verification performed, and the security flaws discovered.
    Original languageEnglish
    Place of PublicationEnschede
    PublisherDistributed and Embedded Security (DIES)
    Number of pages16
    Publication statusPublished - Dec 2005

    Publication series

    NameCTIT Technical Report Series
    PublisherUniversity of Twente, Centre for Telematics and Information Technology (CTIT)
    No.TR-CTIT-05-62
    ISSN (Print)1381-3625

    Keywords

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

    Fingerprint Dive into the research topics of 'A Formal Security Analysis of an OSA/Parlay Authentication Interface'. Together they form a unique fingerprint.

  • 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. (CTIT Technical Report Series; No. TR-CTIT-05-62). Enschede: Distributed and Embedded Security (DIES).