Brutus: a model checker for security protocols
W. Marrero, Edmund M. Clarke · 2001
Abstract As more resources are added to computer networks, and as more vendors look to the world wide web as a viable marketplace, the importance of being able to restrict access and to ensure some kind of acceptable behavior, even in the presence of malicious adversaries, becomes paramount. Many researchers have proposed the use of security protocols to provide these security guarantees. In this thesis, I describe a method of verifying these protocols using a special purpose model checker, Brutus, which performs an exhaustive state space search of a protocol model. This tool also includes a natural deduction style derivation engine which models the capabilities of an adversary trying to attack the protocol. Since the models are necessarily abstractions, one cannot prove a protocol correct. However, the tool is extremely useful as a debugger. I have used this tool to analyze fifteen different security protocols, and have found the previously reported attacks for them.