Security Protocols And Ban Logic Analysis

Nowadays, information security has already become a bottleneck that restricts applications of computer network. The security of information needs not only some good encryption algorithms but also some security theories, security measures and security technologies. In these theories, measures and technologies, the security protocol is playing very important role. In practical applications, people requires credible mechanism to verify identity of communicating parties and distribute keys. This forces people to have to research and design various security protocols. Generally speaking, security protocols are protocols that use cryptography to distribute keys and authenticate principals and data over a network and are a basic guarantee of secure communication through open and unprotected network. But proved by practice, design and analysis of security protocol has been recognized as much more difficult than initially thought and needs a rigorous formal approach to provide credible analysis guarantee. The complicated network environment makes the attackers to enable realizing various attacks by means of flaws and leaks of security protocols, illegally obtain the network resources and unauthorized information, and consequently endanger security and application of a network. Therefore, the security of security protocols has become one of the key problems of network security. To verify the security of security protocols is called security protocol analysis and a current research hot spot on network security. At present, most wildly used protocol verification method is various formal ones. By means of the formal mothods, we may make a model for security protocol using formal language or model and then verify its security according to assumptions and verification rules.How to ensure the security of security protocol is our starting point on network security in the paper. We research and analyze symmetric key cryptograph, public key cryptograph, elliptic curve cryptograph, and digital signature algorithms, etc. We further discuss some typical authentication protocols, key management and distribution methods, etc., and analyze informal methods and formal methods of security protocol, especially BAN logic. And then, we analyze a few authentication protocols with BAN logic.Some examples that have been analyzed with BAN, have shown that the BAN logic has the active effect in analyzing the authentication protocols, and finds some flaws and redundancy that were not discovered before. But through analyzing two authentication protocols, BAN logic defect in protocol analysis about man-in-the-middle attack and key guessing attack was pointed out, and the improved protocol against a man-in-the-middle attack and one against key guessing attack are given in the paper. Finally, we put forward three security schemes based on security protocal, the first for electronic official-documents interchange based on ECC, the second for message interchange based on ECC, and the last for message interchange signcrypting based on ECC. The elliptic curve cryptographic technique has been brought in message interchange schemes. The primary advantage that elliptic curve systems have over systems based on the multiplicative group of a finite field (and also over systems based on the intractability of integer factorization) is the absence of a subexponential-time algorithm that could find disaete logarithms in these groups. Consequently, we can use an elliptic curve group that is smaller in size while maintaining the same level of security. The result is smaller key sizes, bandwidth savings, and faster implementations. In other words, use of elliptic curve cryptographic techniques provide greater security using fewer bits, resulting in a protocol which requires low computational overhead, and thus, making it suitable for digital signature, key agreement and exchange and more secure and faster message interchange in network.