書評

『シリーズ応用数理 【1】巻 数理的技法による情報セキュリティ』（日本応用数理学会 監修・萩谷 昌己・塚田 恭章編）

正しい証明を書くのは難しい。著名な数学者でさえ、飛躍や誤りのある証明を書いてしまうことがある。証明の間違いをなくすには、証明の細部を省略せずに記述するのが良いかもしれない。その場合、長過ぎる証明を書くのは人手では困難を伴い、また退屈で間違いの元になるので、コンピュータの利用が欠かせない。そこで、数理論理学やプログラミング言語理論の研究者は、コンピュータを用いて証明を行う方法について、過去数十年に亘って盛んに研究してきた。これは、単にコンピュータを道具として使うことには留まらず、じつは数理的にも大変興味深いものである。

本書は、暗号の安全性をどのように数学的に定式化し証明するか、そして定義や定理や証明をコンピュータの助けを借りて記述し、機械的に正しさを確かめるにはどうしたらいいのかを学ぶための入門書である。もともと暗号の研究では、様々な暗号方式の安全性が数学的に証明されてきたが、その証明は確率、計算量、並行性を扱っていて煩雑であり、間違いが見つかることもしばしばであった。そこで、暗号の安全性証明をコンピュータ上で形式的に記述して機械的に検証する研究が過去20年近くの間、盛んに研究されてきた。日本応用数理学会においても「数理的技法による情報セキュリティ」研究部会が2006年に設立され、その中で議論が活発に行われてきた。本書は、この研究部会の参加者を中心として、暗号理論の専門家と形式検証技術（数理的技法）の専門家によって分担執筆されている。

◇

そもそも現代のコンピュータは、依然として、人が書いた証明の意味を理解してくれるわけではない。コンピュータが行うのは、ある記号列を別の記号列に書き換えるという「記号操作」の繰り返しに過ぎず、「記号操作」が何を意味するのかは人が解釈することである。したがって、暗号の安全性を証明したい場合は、コンピュータ上での個々の「記号操作」に対し、その意味として「暗号で用いられる数学的対象」を対応付ける。これにより、「記号操作の繰り返し」を暗号の安全性証明だと見なすことが可能となる。これは、一見すると大したことのないように見えるかもしれないが、「記号操作の世界」と「検証対象（暗号で用いられる数学）の世界」を区別し、これらの間に対応関係を定義し、数理的に厳密に取り扱うところに、形式検証技術の研究の面白さのひとつがある。

本書では、まず、「記号操作」の繰り返しによって暗号プロトコル（暗号を用いた通信の手順）の安全性を検証する手法が紹介される（第2章）。ここでは、暗号プロトコルをプロセス（記号列）で表現し、規則に従ってプロセスを少しずつ変形していくことにより、記号的な安全性を証明している。（記号的な安全性というのは、単純化のために、暗号プロトコルの部品が理想的な安全性を持つと仮定し、これに対する攻撃の確率や計算量を考慮しない場合の安全性である。）

一方で、「記号操作」を用いずに人手で暗号プロトコルの計算量的な安全性を証明する方法（暗号理論の入門）も紹介される（第3章、第6章）。第3章では、暗号プロトコルの振る舞いを「攻撃者と挑戦者によるゲーム」と見なし、ゲームを少しずつ変形していくことにより、暗号プロトコルの計算量的安全性を証明する方法が紹介される。その後、このゲームの変形の繰り返しによる計算量的安全性の証明を「記号操作の繰り返し」として記述する枠組みとして、確率ホーア論理（第4章）とタスク構造確率I/Oオートマトン（第5章）が紹介される。

これらのアプローチでは、計算量的安全性の証明をほとんどそのまま記述するため、コンピュータによる自動証明が容易でないという欠点もある。そこで、記号的な安全性を自動検証するだけで、計算量的な安全性を証明してしまおうという別のアプローチがある。具体的には、記号的な安全性を持つ暗号プロトコルが計算量的な安全性を持つためには、暗号プロトコルの部品がどのような性質を満たせば十分なのかを明らかにする研究（第7章、第8章）が紹介される。ここでは、「記号操作の世界」と「暗号で用いられる数学の世界」の間の対応関係が数理的に論じられる。これを踏まえて、第9章では、暗号プロトコルの記号的な安全性を証明するための論理推論体系が紹介され、その証明が計算量的な安全性を保証することが示される。

◇

本書は、この分野の入門書としては、日本語で書かれた唯一のものであり、出版から7年を経た今もなお、暗号理論や形式検証技術に興味を持つ学生や研究者にとって有益なものである。なお、本書に含まれない最近の研究、特に定理証明支援系を用いた暗号の安全性証明については、拙著論文『暗号系の安全性検証 — 入門から計算機による証明まで』（コンピュータソフトウェア，Vol.33 No.4, pp.67-83，2016年）を参照されたい。