Research On Formal Analysis Of Security Protocols

It is recognised that the design and verification of security protocols is avery challenging task, since protocols that appear secure can contain subtleflaws and vulnerabilities that attackers can exploit. Many facts show that thereare still some leaks in the security protocols which have been carefullyanalyzed and designed by security experts. Some security protocols areattacked after using many years.A number of techniques exist for the analysis of security protocol. Eachof the techniques currently available is not capable of detecting every possibleflaw or attack against a protocol when used in isolation. However, whencombined, these techniques all complement each other and allow a protocolengineer to obtain a more accurate overview of the security of a protocol thatis being designed. For protocol analyzers, it is possibly difficult to use theseautomatic tools.Our research is on formal analysis of security protocols. We propose acombined analysis method for security protocols. By specifying securityprotocols using CAPSL, then convert CAPSL specification into formal inputsfor other analysis tools by connector. This method can utilize the advantage ofvarious analysis tools and ensure the accuracy of formal analysis. Meanwhile,it is convenient for analyzer.We design two CAPSL connectors. One is from CAPSL to Casper/FDR;the other is from CAPSL to HLPSL/OFMC. We give a converting result ofNeedham-Schroeder Public Protocol by the both connectors and test results onClark-Jacob protocol library. It is shown that our method is effective.