Towards Security Analyses of an Identity Federation Protocol for Web Services in Convergent Networks

We describe a formal approach to the analysis of security aspects of an identity federation protocol for Web services in convergent networks. This network protocol was proposed by Telecom Italia as a solution to allow end users to access services on the Web through different access networks without explicitly providing any credentials, while the service providers can trust the user´s identity information provided by the access networks and access some user data. As a first step towards a fullblown formal security analysis of the protocol, we specify three user scenarios in the process algebra Crypto-CCS and verify the vulnerability of one of these specifications w.r.t. a man-in-the-middle attack with the model checker PaMoChSA.