Modeling and Analyzing Security Protocols with Brutus
        Will Marrero (marrero@cs.cmu.edu)
        Department of Computer Science
        Carnegie Mellon University

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 insure some kind of acceptable
behavior even in the presence of malicious adversaries becomes
paramount. Researchers have looked to cryptography to help solve many

of these problems.  However, cryptography itself is only a tool.  The
security of a system depends not only on the cryptosystem being used,
but also on how it is used in a protocol.  In this talk, I present a
method for verifying these protocols using BRUTUS, a special purpose
{\em model checker} for security protocols.  The tool automatically
models the capabilities of an adversary trying to attack a protocol
and checks all possible behaviors of the protocol in the presence of
such an adversary.  These traces are checked against a specification
given in logic of knowledge which can express properties such as
authentication, secrecy, anonymity, and integrity of transactions.
The tool also exploits symmetry and independence of actions to perform
state space reductions during the search.  The tool has been used to
analyze 14 different authentication protocols, and 3 electronic
commerce protocols.