Research On Attack Sequence Reconstruction Technology For Security Protocols

In recent years, formal analysis and automatic verification technology of security protocols obtain more and more attention, but the research of attack reconstruction technology based on security protocols formal analysis theory is still at its elementary stage, though attack reconstruction can not only prove the validity of the formal analysis methods but also give reference to attacking the net of enemies.Based on process algebra theory and first-order logic theory, the dissertation does profound research on the attack reconstruction technology. The main contributions of the dissertation are summarized as follows:1. Different attack methods on security protocols are researched, the damage of these attack methods is analyzed and compared. Then various attack reconstruction technology methods are searched, and the advantages and disadvantages of the methods are compared;2. After analyzing a variety of attack methods and formal analysis methods, the dissertation adopted process algebra theory and first-order logic theory to model security protocol, then a security protocol model is presented which fits to reconstruction of attacks, by adding senders and receivers of messages, session identifier and step information of protocols. Security protocol process algebra syntax and semantics, as well as first-order logic syntax and semantics are presented, and after that the transition rules between the two sets of syntax and semantics are given, the deduction consistency is proved;3. In order to realize automatic reconstruction of the attack sequence, attack reconstruction mechanism based on first-order logic is presented, a variety of conditions are discussed deeply, logic rules are classified by different properties in rule classification strategy; the unification of rules are related to the run of protocols in rule unification strategy; the information of rule classification, rule unification, sender and receiver of messages and session identifier are record in logic information record strategy; attack process is translated from logic deduction in logic deduction interpretation strategy. At last a example by the simplified Needham-Schroeder protocol shows the application of these strategies;4. On the basis of the security protocol model and the attack reconstruction strategies, attack reconstruction algorithm is presented, rule unification, implication verification and rule simplification algorithms are improved. These algorithms cooperate to reconstruct attack process automatically;5. Based on verification algorithm and attack reconstruction algorithm, an automatic verification prototype system of security protocols called ASPV-AR is designed and implemented. The architectonics, functions and interfaces of each module are introduceddetailedly. In the end the efficiency of the ASPV-AR is tested.