Bisimulation Equivalence Verification In Security Protocols

With more and more information service and commercial activities provided on the open network, the soundness of network security protocols, which are utilized to guarantee the above service, attract many people's attention. However, suffering from severe attacks and lack of systematic design and verification method, network security protocols become very fragile and error-prone.Formal method provides an effective way for analyzing security protocols. It makes use of formal language to modelize these complex protocols and verifies their correctness or traces out the deficiencies by advanced deduction or proof system. Bisimulation equivalence verification method is among these. By the virtue of actuate algebraic semantic model-Spi calculus, as well as very effective bisimulation equivalence method, it appeals many researchers in the recent year. However, there're some deficiencies in this model and what's more the bisimulation relation now can only be proved by hands, not by computer.We intend to enrich Spi language, and build new bisimulation equivalence on it, whose proof can be automized , therefore design automatic verification tools for security protocols on this relation. In summary, the contributions of our work lie in the following three aspects:1). Enrich the language of Spi calculus, built a new spi model for cryptographic communication protocols. We built some operation primitives for public encryption system so as to describing full encryption system in security protocols. We modified concurrent semantics of spi calculus to model the direct interaction between communication principles and the open environment, which more actually depicts real running of security protocols.2). Design symbolic operational semantics and symbolic bisimulation. Our symbolic semantics requires the input process only accept symbolic message terms deductive from its environment, by which the infinite branches of input process can be successfully solved. Our symbolic reefed bisimulation insures two processes are executed in finite tracsitions in the bisimulation games.3). Build and prove the soundness relation between symbolic reefed bisimulation and previous concrete bisimulation, and furthermore the automatic verification tools on bisimulation equivalence can be developed.In the end of this thesis, we made a summary and discussed four prospective views in the further work.