Design And Analysis Of Security Authentication Protocols

Security protocols play a very important role in the information security. In practical applications, people require credible mechanism to verify the identity of communicating parties and distribute keys. However, it is often proved that security protocols are not as safe as the designers hope. The complicated network environment makes the attackers to enable realizing various attacks by means of flaws and leaks of security protocols. The safety of security protocols has become one of the key problems of network security. Two aspects are included in the study of security protocols: study of methods of security protocol analysis and study of design and analysis of all kinds of practical security protocols. Design and analysis of security protocols is very complicated .Lots of facts show that it is still very difficult to design a correct security protocol without security leaks, even if there are a few main bodies and exchange messages in the whole protocol. So, it is very necessary to design security authentication protocols with formal methods, and analyze protocols strictly with formal methods.Nowadays, people emphasize on formal analysis in the research on security protocols. There are three typical security protocol analysis methods: analysis method of modal logic based on knowledge and believes, analysis method based on model checking, and analysis method based on theorem proving. The research on formal analysis of security protocols mostly promotes the development of security protocol design. However, there are some methods and theories of security protocol design, but there are very few practical methods and tools which are easy to perform.This paper mainly studies security protocols from three aspects: firstly, this paper develops a scheme PCDS of designing security authentication protocols with formal methods, establishes its mathematical model and presents a method for its specific realization. Secondly, this paper analyzes security authentication protocols with formal methods. Thirdly, this paper proposes a new protocol APVC which verifies video conference quickly and safely.In the design of security protocols: based on the idea of Datta, this paper develops a scheme of designing security authentication protocols with formal methods, establishes its mathematical model and presents a method for its specific realization. This scheme is on the basis of Diffle-Hellman algorithm. It divides the design of security protocols into three levels. The first level is realizing basic key exchange and identity verification. The second level is the efficiency promotion and realization mechanism of defending Denial-of-service Attacks. The third level is formal analysis of the security properties and verifying the security properties by automatic test tools. This system can implement formal design of security authentication protocols, give many candidate protocols according to different environment and requirements, verify the safety of protocols, and it can be conveniently extended and transplanted as required. With this method, we can design present practical authentication protocols such as IKE and so on.In the formal analysis of security protocols, this paper mainly studies PCL, a logical deduction system used for proving the security properties of network protocols. PCL has BAN logic's legibility, and also has the same safety proof grade as PIM based on participant and intruder model. By PCL, we can prove the authentication and confidentiality of security protocols. This paper proves the authentication and confidentiality of the two designed security protocols by PCL.In the automatic test of security protocols: this paper mainly studies HLPSL (High-Level Protocol Specification Language) and the automatic test tool AVISPA. This paper also tests some protocols by AVISPA, and has gotten some significant testing results.At last, this paper studies frequently-used identity verification methods of present video conference system, and analyzes its safety and flaws. According to the problem of safety and efficiency, this paper proposes a new protocol APVC which verifies video conference quickly and safely. This paper also analyzes its safety and efficiency. Proved By PCL and AVISPA in the D-Y model, this protocol not only has the security of certificate-based public key Cryptosystem, but also the efficiency of symmetric cryptosystem.