A Formal Security Analysis of an OSA/Parlay Authentication Interface

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.