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)
    102 Downloads (Pure)


    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
    PublisherCentre for Telematics and Information Technology (CTIT)
    Number of pages16
    Publication statusPublished - Dec 2005

    Publication series

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


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


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

      Corin, R., Di Caprio, G., Etalle, S., Gnesi, S., Lenzini, G. & Moiso, C., Jun 2005, Formal Methods for Open Object-Based Distributed Systems: 7th IFIP WG 6.1 International Conference, FMOODS 2005, Athens, Greece, June 15-17, 2005. Proceedings. Steffen, M. & Zavattaro, G. (eds.). Berlin, Heidelberg: Springer, p. 131-146 16 p. (Lecture Notes in Computer Science; vol. 3535).

      Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

      Open Access
      16 Downloads (Pure)

    Cite this