モデル検査 • 状態遷移系 • PLTL（propositional linear-time temporal logic） – 無限経路のもとでの論理式の解釈 • PLTLのモデル検査 – オートマトンの構成 – 無限経路に関する条件 – 状態遷移系との同期的合成 • fairnessの表現 • SPIN概要証明支援系 • PVSチュートリアル – – – – – – – http://www.csl.sri.com/papers/forte97/ 状態遷移系の記述モデル検査 invariantの検証抽象化抽象モデル検査抽象化の妥当性の検証抽象モデル検査：事例 • alternating bit protocol – – – – – sender: header, message receiver: header message queue ack queue verify queue • 抽象化 • レポート課題２認証プロトコルの検証 • 状態遷移系としてのプロトコル – 状態 • ストランドのマルチセット • メッセージの集合 – 遷移 • ストランドの伸長 • 攻撃者による偽メッセージの送信 • ストランドを用いた推論 – Needham-Schroeder公開鍵プロトコル Javaプログラムの検証 • JMLとESC/Java • ESC/Javaマニュアル – http://research.compaq.com/SRC/esc/download.html • 卒論紹介 – Verification of the Validity of Java Card Transactions • LOOP – JavaからPVSへの変換レポート課題１ • untilオペレータUの双対である releaseオペレータRを次のように導入し、その意味を定めよ。 φ R ψ ≡ ￢(￢φ U ￢ψ) • UとRを含む線形時間時相論理に対して、モデル検査の手続きを与えよ。レポート課題２ • キューを抽象化し、抽象状態を網羅することにより、 alternating bit protocolの安全性を検証せよ。（メッセージは0か1とする。） • 抽象化の正当性について議論せよ。 • alternating bit protocolの活性について議論せよ。レポート課題３ • 次のプロトコルの正しさについて議論せよ。 AB : {A,NA}KB BA : {NA,NB}KA AB : {B}NB • 次のプロトコルの正しさについて議論せよ。 AB : {A,NA}KB BA : {NA,NB}KA AB : {B,NA}KA －1 レポート課題４ • quicksortのJavaプログラムを書き、配列のインデックスが限界を超えないことを検証するためのESC/Javaのpragmaを各メソッドに挿入せよ。また、quicksortの正当性をpragmaによって表現してみよ。このために必要なloop invariantなどもできる限りprogmaとして表現せよ。４題のうち、２題を選んでレポートを提出して下さい。〆切は米澤先生の〆切と同じにします。