Gavin Lowe

Needham et Schroeder avaient publié leur protocole à clé publique en 1978, et il avait été examiné à la main comme avec des logiques formelles. Lowe l'a modélisé dans l'algèbre de processus CSP, a laissé le model checker FDR chercher, et a obtenu une trace MITM où une partie honnête est amenée à parler au mauvais interlocuteur. Le correctif tient en une identité ajoutée à un message ; le protocole s'appelle depuis Needham–Schroeder–Lowe.

Ce résultat est devenu l'argument classique pour vérifier les protocoles de sécurité par machine plutôt que par relecture attentive. Lowe a ensuite créé Casper, qui compile des descriptions de protocoles en CSP pour que moins de gens aient à écrire les modèles à la main.