Formal Analysis Of Security Protocols Based On SPI Calculus

A safe cryptographic protocol is the basis of composing information security systems, and it is one of absolutely necessary components of the communication of networks and its applications. However, many existing security protocols are proven not to be so reliable as what were expected. Owing to the subtlety of security goal, the complexity of network environment, the uncertainty of the penetrator's ability and the high parallelization of protocol run, verification of a security protocol can be very difficult, so we must analyze security protocols by formal methods.Since the 1970's, some formal methods of security protocol analysis have been proposed, these methods are mainly of three kinds: methods based on modal logic of knowledge and belief, methods based on theorem proof and methods based on process calculus. And among the three methods mentioned above, the process calculus can model the protocols very precisely. The Spi calculus, which is based on the theory of process calculus, can define cryptographic operations and is fit for the analysis of the protocols which operate concurrently in multiple runs.In this article, a detailed analysis is given to the formal verification methods of security protocols. We pay our attention to the Spi calculus, and validate the protocols through bisimulation. The main contents and contributions are as follows:1) Some formal methods for the analysis of security protocols are summarized and discussed. We devote much effort into the discussion of the one which is based on process calculus. We also show how a protocol is analyzed based on Spi calculus and the theory of bisimulation.2) The necessity of the Spi calculus is introduced in the discussion of how to use pi calculus to describe security protocols. We point out that strong bisimulation is too strict in the analysis of security protocols. Furthermore, test equivalent is introduced to model the security properties.3) In order to simplify the verification of protocols, framed bisimulation and barbed bisimulation are introduced, and compared with the test equivalent. The syntax and semantic of the Spi calculus under asymmetric cryptosystem are also discussed. Finally, we use the Spi calculus to analyze two typical security protocols.