マイケル・バローズ

BAN論理（1989年、マルティン・アバディ、ロジャー・ニーダムとの共同）は、認証プロトコルの参加者が各メッセージの後に何を信じてよいかを形式的に推論しようとした、最初の本格的な試みの一つである。発表済みのプロトコルの欠陥を次々と洗い出し、Kerberosの解析を含む形式的プロトコル検証という分野全体のきっかけとなった。

1994年にはデビッド・ウィーラーとともに、のちにbzip2を可能にしたブロックソート変換を発表。AltaVistaのインデクサや、Google時代のロックサービスChubbyも書いた。これほど幅広い業績を、これほど少ないプレスリリースで積み上げた人は多くない。