ギャビン・ロウ

ニーダムとシュローダーは1978年に公開鍵プロトコルを発表し、手作業や形式論理による検証を受けてきた。ロウはこれをプロセス代数CSPでモデル化し、モデル検査器FDRに探索させた。すると、正直な当事者が誤った相手と通信させられる中間者攻撃のトレースが返ってきた。修正は、あるメッセージに識別子を一つ加えるだけだった。このプロトコルはそれ以来、ニーダム＝シュローダー＝ロウと呼ばれる。

この成果は、セキュリティプロトコルは注意深く読むより機械で検査すべきだという、定番の論拠になった。ロウはその後、プロトコル記述をCSPに変換するCasperも作り、モデルを手書きする人を減らした。