Modelling and analysing an identity federation protocol: federated network providers scenario

We continue our work on modelling and analysing security issues of an identity federation protocol for convergent networks. This protocol was proposed by Telecom Italia as a solution to allow end users access to 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 an intermediate step towards a full-blown formal security analysis of this protocol, we specify one specific user scenario in the process algebra Crypto-CCS and verify its vulnerability w.r.t. a man-in-the-middle attack with the model checker PaMoChSA.