暗号理論と数理的技法の融合による暗号プロトコルの新しい検証手法という、近年世界的に研究が活性化している分野に関する初の邦書。

本書では暗号理論と数理的技法の融合による、暗号プロトコルの新しい検証手法について、基礎的な概念と主要な方法論をわかりやすくコンパクトに解説している。
もくじ情報：第１章　数理的技法による情報セキュリティの検証；第２章　ｓｐｉ計算による暗号プロトコルの記号的検証；第３章　ゲーム列による安全性証明の基礎；第４章　ゲーム列による安全性証明の形式化と自動化―確率Ｈｏａｒｅ論理と確率プロセス計算によるアプローチ；第５章　タスク構造確率Ｉ／Ｏオートマトンを用いた安全性証明；第６章　汎用的結合可能性による暗号システムの安全性証明；第７章　識別不可能性の記号的な解析とその健全性・完全性；第８章　マッピング補題―計算論的トレースから記号論的トレースへ；第９章　セキュリティプロトコルの論理的検証法

萩谷　昌己(ハギヤ　マサミ)
１９５７年生まれ。１９８０年東京大学理学部情報科学科卒。現在、東京大学大学院情報理工学研究科教授。理学博士。専門は、計算機科学