Technologies in cryptography and cryptographic information security have become indispensable for the modern network society and their use is becoming more and more wide-spread. Since security problems in a system relying on such technologies would cause enormous social damage, it is of extreme importance even from the practical viewpoint to rigorously verify the security of cryptography and cryptographic applications.
To date, as a standard method for verifying the security of cryptography and cryptographic applications the computational proof method, based on computational complexity, has been established in the theory of cryptography. On the other hand, much effort has also been spent for guaranteeing the security from the standpoint of formal methods by investigating the symbolic proof method. However, the relationship between the two methods had not been studied until a few years ago.
Recently, the relationship between the two is being actively investigated in conjunction with the progress in the computational proof method, including universal composability and proofs by game transformation. For example, the soundness and completeness of the symbolic proof method with respect to the computational counterpart are under investigation. Consequently, formal methods are now considered effective in simplifying and mechanizing computational proofs. Since formal methods increase the modularity and transparency of proofs by (partially) mechanizing proof generation and verification, they are believed to contribute to cope with ever increasing complexity of security proofs of cryptographic protocols and applications.
Based on the recent research trends mentioned above, this special interest group has been founded to give opportunities for presenting research results and promoting discussions on security proofs of cryptography and cryptographic applications based on formal methods. In particular, it will provide a forum where researchers in the two fields, cryptography and formal methods, who have seldom met together, to exchange ideas and begin collaboration.
Yoshikazu Hanatani (Toshiba Corporation)
Hideki Sakurada (ZEN University)
Mitsuharu Yamamoto (Chiba University)
Kazuki Yoneyama (Ibaraki University)
Maki Yoshida (NICT) Chair
© JSIAM-FAIS [Japanese | English]