Verifying security protocols with Brutus
- 1 October 2000
- journal article
- Published by Association for Computing Machinery (ACM) in ACM Transactions on Software Engineering and Methodology
- Vol. 9 (4) , 443-487
- https://doi.org/10.1145/363516.363528
Abstract
Due to the rapid growth of the “Internet” and the “World Wide Web” security has become a very important concern in the design and implementation of software systems. Since security has become an important issue, the number of protocols in this domain has become very large. These protocols are very diverse in nature. If a software architect wants to deploy some of these protocols in a system, they have to be sure that the protocol has the right properties as dictated by the requirements of the system. In this article we present BRUTUS, a tool for verifying properties of security protocols. This tool can be viewed as a special-purpose model checker for security protocols. We also present reduction techniques that make the tool efficient. Experimental results are provided to demonstrate the efficiency of BRUTUS.Keywords
This publication has 10 references indexed in Scilit:
- Combining Theory Generation and Model Checking for Security Protocol Analysis,Published by Defense Technical Information Center (DTIC) ,2000
- Isomorph-free model enumerationACM Transactions on Programming Languages and Systems, 1998
- Symmetry and model checkingFormal Methods in System Design, 1996
- Exploiting symmetry in temporal logic model checkingFormal Methods in System Design, 1996
- Better verification through symmetryFormal Methods in System Design, 1996
- Condensed state spaces for symmetrical Coloured Petri NetsFormal Methods in System Design, 1996
- Using partial-order methods in the formal validation of industrial concurrent programsPublished by Association for Computing Machinery (ACM) ,1996
- Combining partial order reductions with on-the-fly model-checkingFormal Methods in System Design, 1996
- On the security of public key protocolsIEEE Transactions on Information Theory, 1983
- Using encryption for authentication in large networks of computersCommunications of the ACM, 1978