The use of logic in the analysis of cryptographic protocols

Logics for cryptographic protocol analysis are presented, and a study is made of the protocol features that they are appropriate for analyzing: some are appropriate for analyzing trust, others security. It is shown that both features can be adequately captured by a single properly designed logic. The goals and capabilities of M. Burrows, M. Abadi and R. Needham´s (1989) BAN logic are examined. It is found that there is confusion about these. While the logic is extremely useful heuristically, as a formal method it is seen to be ultimately unacceptable. Formal semantics is explored as a reasoning tool and the importance of soundness and completeness for protocol security is discussed. The KPL logic is used to resolve a debate over an alleged flaw in BAN logic and is shown to be uniquely capable of dealing with certain protocol security issues