Dolev-Yao一回目
Formal Methodってどんなんだろうね, と思ってDolev-Yaoを眺めてみた.
完全に安全な暗号系を最初に仮定するところが気になるが, まぁ, そういうものが存在するとして, 安全なプロトコルは可能か? という話らしい. Man-in-the-Middleを如何にして防ぐかという雰囲気か.
2章までの雰囲気だけメモしておく.
プロトコルの各ラウンドで行う計算を関数の適用と見る. すると正規ユーザーの各ラウンドを関数と見ることが出来る. 敵は正規ユーザーと通信を行うことにより自分が得た情報に関数を適用できる. ということで, 関数の適用によって敵が所望の情報を取り出せるかどうかを調べていく. 実際に評価を行う際には関数を文字列と見做して文法的な観点から評価を行うようだ.
ちょっとすっきりした.