| Security protocols are designed for communication over insecure network. Security protocols work as core components of network security, so their correctness is crucial to network security. The designing and analyzing of security protocols remains a challenge for the subtlety of security goals, the uncertainty of penetrator model, the complexity of the running environment, and the high concurrency of protocol sessions. Formal methods contribute to define security goal of protocols precisely, describe behavior of protocol accurately, and verify whether the protocol meet the target correctly. Through nearly three decades of development, formal analysis of security protocols is immature yet. The emergence of strand space theory sets off a new upsurge of security protocols formal analysis. Strand space theory attracts sights of researchers soon for its compact model, precise definition and efficient proof. Authentication test based upon challenge-response mechanism is a novel method derived from strand space theory. It inherits advantages of strand space, simplifies proving process further, and provides more powerful analysis capabilities on authentication properties.This thesis makes an in-depth study of authentication test's application in analyzing and designing of security protocols, expands authentication test theory in three aspects, and then designs an automatic protocol verification algorithm based on enhanced authentication test. Related efforts result in following major innovative achievements:1. Taxonomic study of replay attacks which may do great harm to security of protocols. Proposed a new classification method based on the underlying reasons for success of attacks. For each category, examples of successful attacks are listed and the methods against those attacks in principle are presented.2. Minimal-element method, ideal-honest method and authentication test method are separately used to verify secrecy and agreement properties of Otway-Rees protocol, followed by summarizing the characteristics of each method through comparison. It shows that authentication test is the most concise and efficient one for protocol analysis. As a case study, secrecy and agreement properties of X.509, an asymmetric key protocol, are verified, then found and amended the flaws in it.3. Applied authentication test to auxiliary protocol designing. Described the thought and procedure of designing protocols in terms of authentication test from standpoint of protocol analysis. Especially discussed the difference in constructing authentication test under symmetric-key and asymmetric-key cryptography. Designed a new mutual authentication protocol with key negotiation using that approach.4. Standardized the proving process of protocols' security attributes with authentication test to make it more rigorous, formal and easy to implement in automatic tools. BAN-Yahalom is analyzed with the standardized proving method, and found a normal form of an attack to it.5. Illustrated the essential cause of limitation of authentication test, that test component cannot occurs as proper subterm of other component. Pointed out the deficiency in Perrig and Song's authentication test version, then proposed the improved authentication test and proved its soundness both in formal and case study.6. With the idea of forced type checkage, defined different types for terms in messages, designed the inspection rules of authentication test method, so as to detect type-flaw-attacks on different levels according to application requirements. Confirmed the effectiveness of our improvements by analyzing Otway-Rees, Andrew RPC and Woo-Lam protocols.7. Imitating the manual proving process, designed an automatic protocol verification algorithm ATAPA based on improved authentication test theory mentioned above. With the programming implementation of the algorithm, verified the attributes of NSL and Woo-Lam protocols. Proved the soundness of both the algorithm and the improved authentication test theory.
|
PDF Full Text Request