In order to analyze the security of authentication protocols, Michael Burrows, Martín Abadi and Roger Needham designed a logic of authentication, called the BAN-logic. This logic makes explicit what the assumptions of a protocol are, what the individual steps amount to in terms of knowledge, and what the final state of each agent is. Even though a protocol is usually described as the sending of messages (as shown before), this is usually not a very useful description to use in a formal logic. Therefore, the BAN logic we talk about messages that a participant might receive. However, BAN logic does have its limitations. For example, plain text messages are seen as irrelevant since anyone can read them. Furthermore, the BAN logic does not recognize hash functions.
Given these limitations, some problems cannot be usefully analyzed using BAN logic. For this reason, Li Gang, Roger Needham and Raphael Yahalom have extended the protocol to include more concepts. This logic is called the GNY logic.
In GNY logic, it is possible to reason about the beliefs of the individual participants. This means that, while someone might receive a message, he does not necessarily believe the content. Also, an agent might make assumptions about what other agents belief.
In order to analyze our described protocols with these logics, we first need to explain the statements possible in GNY.
Using this logic, and defining what assumptions agents make before the run of the protocol, it is possible to deduce what each agent knows at the end of the run. To demonstrate this, we will show an example for the simple case of OpenPGP. When this is done, we will try a harder example with the OTR encryption. After this, we will show what a malicious attacker can do to damage the communication between two agents using the OTR protocol.