A Logic of Authentication Burrows Abadi Needham, 1990 ========================= Big Picture ----------- The paper proposes a formal framework for specification and analysis of authentication protocols. It illustrates the approach with several real world examples. Overview -------- The set of players is a set of "principals" who want to satisfy each other as regards the identity of each other. In particular, the goal usually is for two principals to be convinced that they have a shared secret which they are using to communicate. The paper presents the syntax of their logic. It then ascribes semantics to each syntactic symbol. The semantics capture real world notions like "belief", "delegation", "freshness", etc. It also lays down proof rules for deducing new beliefs from existing ones. See the paper for details. It contains a clear description of the various symbols and their semantics. A protocol starts with an initial state where the principals have an initial set of beliefs. As each subsequent messate is sent, the beliefs of the receiver of the message are augmented using the proof rules of the logic. When the protocol ends, the principals should believe what they had set out for (for example, the beliefs that both A and B share a secret which they will subsequently use for secure communication). The paper analysis several well known protocols including Kerberos, Needham-Shroeder, Andrew-secure-RPC and CCITT. Their logic is able to identify the well-known weakness of Needham-Shroeder protocol. -- What makes this logic different from traditional logic? In authentication, there are notions of "belief", "trust" and "delegation", which are not captured by the semantics of logics used for traditional verification (circuits, programs, protocols). -- Other advantages of using this framework? Apart from proving correctness, the process of protocol analysis can also identify redundancies, for example, (a) whether the protocol makes more assumptions than necessary, (b) whther the protocol can be made simpler by removing some pieces (messages, parts of messages) without weakening it, (c) whether something that is sent in ciphertext can be sent in plaintext without compromising correctness. -- Caveats? Using this logic is not a complete proof that a protocol works. Some issues that are not under the purview of the logic, need be addressed separately: e.g., proving hardness of the encryption technique, proving that a specific implementation is correct, etc. The paper does not propose an "automatic" proving procedure. The goal of this paper was to lay down the syntax, semantics and proof rules for the logic. Making a real package that helps a protocol designer rectify her design (e.g., by automatically suggesting changes to the protocol or changes to the initial set of assumptions) would be the next step.