The security of cryptographic protocols has become indispensable in modern network society. To analyze cryptographic protocols, researchers have developed two approaches: symbolic and computational. The symbolic approach is based on a symbolic (Dolev-Yao) model of protocol executions, where cryptographic primitives are treated as black boxes. With this approach, security proofs are simplified significantly and can often be automated for quite large, complex protocols. However, the guarantees that this approach provides with respect to a deployed protocol have been rather unclear. The computational approach is based on a computational (complexity-theoretic) model where adversaries are treated as probabilistic polynomial-time interactive Turing machines. This approach captures a strong concept of security, which is guaranteed against all these adversaries. However, proofs in this model are rather complicated and less successful for complex protocols.
Recently, the relationship between the symbolic model and the computational model has been being actively investigated. For example, in some cases the symbolic analysis is shown to be sound with respect to the computational model. A more direct approach that considers symbolic proofs in the computational model has also been investigated. These investigations are being accelerated in conjunction with the progress in the computational approach, including universal composability and proofs by game transformation.
Based on the recent research trends mentioned above, we have started a research project dedicated to providing a computational justification for the symbolic analysis methods that we have proposed so far. We expect that our efforts will lead to a computationally sound framework of automated security analysis for complex cryptographic protocols.