Research On Formal Analysis Of Three-party Cryptographic Protocols

Today three-party cryptographic protocols, whose securities directly affect the ones of networks, are widely used in cryptographic systems. How to detect the flaws which exist in three-party cryptographic protocols and how to improve these protocols are mainly researched in this thesis. So far many methods are applied to detect these flaws. Among those methods, the best known and most influential one is BAN logic that developed by Burows, Abadi, Needham. But BAN logic and series of BAN-like logic appeared later often have some limitation and largely don't fit to the analysis of three-party cryptographic protocols.This thesis studies formal analytical method of three-party cryptographic protocols. And my main works are listed as follow:1. The significant flaws in BAN logic are summarized. And these flaws' influences on protocols' security analysis are illustrated with examples.2. Aim at the problem that the BAN logic can't effectively analyse three-party cryptographic protocols, several BAN logic rules are supplemented or improved, and the authentication target of BAN logic is enhanced.3. An improved BAN logic is devised. With the supplemented or improved rules, two classical examples named NSSK Protocol and Otway-Rees Protocol are analysed, which proves that the devised mothod is effectual and accurate.4. The Three-party and authenticated Key Exchange protocol is analyzed with the methods of Formal analysis, which shows that the protocol has no obvious flaw.