Structured Intuition: A Methodology to Analyse Entity Authentication

Entity authentication is a process of verifying a claimed identity of a network party. It may appear to be a simple goal, but, depending on the application and context, it entails a number of modalities, such as whether the party is currently active on the network, whether the party is willing to communicate, and whether the party knows that it has been authenticated. Combining such goals in different ways leads to different flavours of entity authentication.

On an unauthenticated channel, an adversary can present a false claim of identity. Clearly, if the adversary succeeds, it may have serious consequences for the security of the system, e.g., private information of legitimate parties may be leaked or the security policy of a trusted system may be violated. At a corporate level, such a failure of authentication may result in loss of proprietary technology or customers' credit card information. Sometimes, a single failure of authentication affects the system for a long time, e.g., if an adversary is able to install a malicious program, such as a root kit, back door, key logger, bot, or other malware. Therefore, security protocols, which can resist a resourceful adversary, are used to authenticate network parties.

Verification of an authentication protocol to show that it is secure is a hard problem. Most of the reported flaws in authentication protocols are not due to some weakness in the cryptographic primitives used in these protocols. The usual problems lie in improper use of cryptographic primitives, and failure to unambiguously specify protocol assumptions and goals. Therefore, it is important that an authentication protocol is analysed with clear goals and explicitly stated assumptions.

There are many different formal definitions of authentication goals, and the decision of which definition is most appropriate depends on the requirements and constraints imposed by the larger system. Whether a reported flaw in a protocol is exploitable depends on the protocol goals and the environment in which the protocol is deployed. Whether a \secure" protocol is indeed secure depends on the security model and the level of abstraction used in the analysis. Thus, the goal of developing a high level methodology that can be used with different notions of security, authentication, and abstraction is worth considering.

In this thesis, we propose a new methodology, called the structured intuition (SI), which addresses the issues mentioned above. In the SI, we divide entity authentication into fine grained properties, which we call FLAGs (fine level authentication goals). FLAGs are protocol independent goals and represent one's expectations in an authentication-as-a-service paradigm. There is a single notion of security in our methodology, which is called canonicity, which is a weaker form of message authenticity. As compared to many contemporary analysis techniques, an SI based analysis provides detailed results regarding the design rationales and entity authentication goals of a protocol.