Catherine Meadows

1990年代初頭のNRL Protocol Analyzerは、「攻撃者が鍵を知っている」という好ましくない状態から逆向きに探索し、そこへ到達しうるかどうかを調べる、初期のツールの一つだった。1990年代後半にはこれをIPsecの鍵交換であるIKEに適用し、すでにルータに実装されていた仕様の弱点とあいまいさを見つけ出した。

後継のMaude-NPAは、Santiago EscobarやJosé Meseguerとの共同開発で、XORやDiffie–Hellmanの冪乗といった代数的性質を扱える。単純なモデルが捨象してしまい、攻撃者が見逃さない部分である。