ゲーム列による安全性証明の形式化と自動化－確率Hoare論理と確率プロセス計算によるアプローチ [萩谷昌己, 塚田恭章 (編), 数理的技法による情報セキュリティ, 日本応用数理学会監修, シリーズ応用数理, 第1巻]