Security analysis of parlay/OSA framework

This paper reports an analysis of the security of the Trust and Security Management (TSM) protocol, an authentication protocol which is part of the Parlay/OSA Application Program Interfaces (APIs). Parlay/OSA APIs allow third party service providers to develop new services that can access, in a controlled and secure way, the network capabilities offered by the network operator. The role of the TSM protocol, run by network gateways, is to authenticate the client applications trying to access and to use the services offered. For this reason, potential security flaws in the authentication protocol can lead to unauthorized use of the network with evident damages to the operator and to the quality of services. This paper shows how a rigorous formal analysis of the TSM protocol allowed us to discover serious weaknesses in the model describing its authentication procedure. The paper reports on the design activity of the formal model, the toolaided verification we carried out and the security flaws we discovered. This allows us to discuss how the security of the TSM protocol can be generally improved.