caeruiro
ついに最終章です。 10. Case Study: Verifying a Security Protocol 最後の章は、セキュリティプロトコルをモデル化し、その正しさを証明します。Needham-Schroeder公開鍵プロトコルを例として、Isabelleを使ったプロトコルの検証方法を見ていきます。 10.1 The Needham-Schroeder Public-Key Protocol このプロトコルは公開鍵暗号を使用します。アリスがボブにメッセージを送るにはボブの公開鍵で暗号化し、ボブの持っている秘密鍵のみがこの暗号文を正しく復号することができます。 Needham-Schroederプロトコルには三つの重要なメッセージがあります。 最初のメッセージは、アリスが作成したノンス(Na)とアリスの名前(A)を、ボブの公開鍵(Kb)で暗号化したメッセージをアリスからボブへ送信するこ
1
リリース、障害情報などのサービスのお知らせ
最新の人気エントリーの配信
処理を実行中です
j次のブックマーク
k前のブックマーク
lあとで読む
eコメント一覧を開く
oページを開く
ソフトウェア開発を工学にする形式手法の紹介 - formal_methods.pdf
