Automated detection of confidentiality goals

The security goals of an authentication protocol specify the high level properties of a protocol. Despite the importance of goals, these are rarely specified explicitly. Yet, a qualified analysis of a security protocol requires that the goals are stated explicitly. We propose a novel approach to find confidentiality goals in an automated way, based only on the protocol specification. The benefits of the method are: (i) Manual specification of goals is replaced by fully automated methods, (ii) the algorithm constructs the entire protection domain of a protocol, that is, all private and shared secrets, and (iii) the goal of an attack can be found, explaining which compromised entities are shared between the attacker and the honest principals.