暗号および暗号プロトコルの研究において，その安全性解析は研究の生命線と言えるものです．
安全性解析に対するアプローチは，従来，暗号学者と数理的技法研究者の間で微妙に異なっていました．（それゆえ両者が交流することはほとんどありませんでした．）暗号学者によるものは計算論的アプローチと呼ばれ，根底にある暗号の脆弱性も考慮に入れつつ，主として確率的多項式時間限定Turing機械の枠組みを用いて暗号プロトコルの解析を行います．一方，数理的技法研究者によるものは記号的アプローチと呼ばれ，根底にある暗号は絶対に破られないという仮定のもとで，通信路に流れるメッセージを記号に抽象化して暗号プロトコルの検証を行います．
両者のアプローチはそれぞれ長所と短所をあわせ持ちます．いうまでもなく，計算論的アプローチは実際の暗号プロトコルの実装に即したものであり，現実的な解析を行うためには必須と言えます．しかしながら，このアプローチによる解析は一般に確率的多項式時間限定Turing機械の還元を中心とする煩雑なものとなり，しばしば解析に誤りが混入します．これに対して，後者の記号的なアプローチでは，数理論理学の知見を応用した数理的技法（Formal Methods，形式手法とも訳されます）を駆使し，定理証明系やモデル検査系などのツールを用いて，厳密かつ（部分的に）機械的なプロトコル検証を可能にしています．しかしながら，このアプローチは根底にある暗号を理想化しているため，暗号の特徴を利用した攻撃を扱うことができないという欠点がありました．
では両アプローチの「いいとこどり」はできないのでしょうか？その可能性は2000年にAbadiとRogawayによって初めて示されました．彼らは，記号的なアプローチによって安全性を証明しさえすれば（ある条件のもとで）自動的に計算論的アプローチにおける安全性も保証されること（計算論的健全性と呼ばれます）を初めて明らかにしたのです．これにより，実装に即した複雑な現実世界での安全性を，より簡略で機械化も可能な理想化した世界での安全性に帰着できる可能性が開けました．彼らの研究発表を契機に，暗号理論と数理的技法の境界領域が多くの研究者によって開拓され，新しい計算論的証明手法（汎用的結合可能性，ゲーム列による証明手法など）の進展ともあいまって，研究が急速に活性化しています．
私たちも，数理的技法の研究者の立場から，暗号理論の研究者と協力し，この新しい分野の進展に貢献したいと考えています．数理的技法の強力な検証技術を活用し，暗号理論に裏付けされたセキュリティを確立することに，積極的に取り組んでいきたいと思っています．