Research of TSM security property in Parlay/OSA based on formal analysis

As a key service providing technology in NGN, the Parlay/OSA realizes the separation between service creation and lower layers network completely. Parlay/OSA open the network recourses to the 3^rd party, and makes use of the Parlay framework interface to suit service creation by 3rd party. However, it is inevitable that there are some security hidden troubles in providing application programming interfaces (APIs). In this paper, we focus on authentication process on Parlay/OSA framework interface, and make use of formal analysis instrument to analyze the security of Parlay/OSA. As a result of this analysis, some security flaws have been present.