A Survey on Computationally Sound Formal Analysis of Cryptographic Protocols

There are two different approaches in analysis of cryptographic protocols.One is based on formal methods,and the other is based on computational complexity as modern cryptography does.Abadi and Rogaway tried to reconcile these two approaches in their seminal work. They set up a relation for some formal results that if a security property is proved in formal model, then the corresponding property is also valid in computational model.Motivated by this work, many works appeared in this area.In this survey,we will summarize various approaches on computational soundness of formal methods in analysis cryptographic protocols,present their main ideas,and point out the future research directions in this area.