ついに最終章です。10. Case Study: Verifying a Security Protocol最後の章は、セキュリティプロトコルをモデル化し、その正しさを証明します。Needham-Schroeder公開鍵プロトコルを例として、Isabelleを使ったプロトコルの検証方法を見ていきます。 10.1 T…

9.2 Advanced Induction Techniques この節では、証明したい式が帰納法に適した形になっていない場合にどうすべきか、そして帰納法のための新たな定理をどのように導出し使うかということを見ていきます。 9.2.1 Massaging the Proposition 証明したい式が帰…