More Web Proxy on the site http://driver.im/

article

Free access

Verifying security protocols with Brutus

Editor: Axel van Lamsweerde Authors:

W. MarreroAuthors Info & Claims

ACM Transactions on Software Engineering and Methodology (TOSEM), Volume 9, Issue 4

Pages 443 - 487

https://doi.org/10.1145/363516.363528

Published: 01 October 2000 Publication History

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.

References

[1]

BELLARE, M., GARAY, J., HAUSER, R., HERBERG, A., KRAWCZYK, H., STEINER, M., TSUDIK, G., AND WAIDNER, M. 1995. iKP-A family of secure electronic payment protocols. In Proceedings of the 1st USENIX Workshop on Electronic Commerce (July). USENIX Assoc., Berkeley, CA.]]

[2]

BURROWS, M., ABADI, M., AND NEEDHAM, R. 1989. A logic of authentication. Tech. Rep. 39 (February). DEC Systems Research Center.]]

[3]

CLARKE, E. M., ENDERS, R., FILKORN, T., AND JHA, S. 1996. Exploiting symmetry in temporal logic model checking. Formal Methods Syst. Des. 9, 1/2, 77-104.]]

[4]

CLARKE, E. M., JHA, S., AND MARRERO, W. 1998. Using state space exploration and a natural deduction style message derivation engine to verify security protocols. In Proceedings of the IFIP Working Conference on Programming Concepts and Methods (PROCOMET).]]

[5]

CLARKE, E. M., JHA, S., AND MARRERO, W. 2000. Partial order reductions for security protocol verification. In Proceedings on Tools and Algorithms for the Construction and Analysis of Systems (TACAS).]]

[6]

DOLEV, D. AND YAO, A. 1983. On the security of public key protocols. IEEE Trans. Inf. Theor. 29, 2, 198-208.]]

[7]

EMERSON, E. A. AND SISTLA, A. P. 1996. Symmetry and model checking. Formal Methods Syst. Des. 9, 1/2, 105-130.]]

[8]

GODEFROID, P., PELED, D., AND STASKAUSKAS, M. 1996. Using partial order methods in the formal validation of industrial concurrent programs. In Proceedings of the 1996 International Symposium on Software Testing and Analysis (ISSTA '96, San Diego, CA, Jan. 8-10), S. J. Zeil and W. Tracz, Eds. ACM Press, New York, NY, 261-269.]]

[9]

HOARE, C. A. R. 1985. Communicating Sequential Processes. Prentice-Hall International Series in Computer Science. Prentice-Hall, Inc., Upper Saddle River, NJ.]]

[10]

HOPPER, N., SESHIA, S., AND WING, J. 2000. Combining theory generation and model checking for security protocol analysis. CMU-CS-00-107.]]

[11]

IP, C. N. AND DILL, D. L. 1996. Better verification through symmetry. Formal Methods Syst. Des. 9, 1/2, 41-75.]]

[12]

JACKSON, D., JHA, S., AND DAMON, C. 1998. Isomorph-free model enumeration: A new method for checking relational specifications. ACM Trans. Program. Lang. Syst. 20, 6, 727-751.]]

[13]

JENSEN, K. 1996. Condensed state spaces for symmetrical coloured Petri nets. Formal Methods Syst. Des. 9, 1/2, 7-40.]]

[14]

KINDRED, D. AND WING, J. 1999. Theory generation for security protocols. Submitted.]]

[15]

LOWE, G. 1996. Breaking and fixing the Needham-Schroeder public-key protocol using FDR. In Proceedings of Second International Workshop on Tools and Algorithms for the Construction and Analysis of Systems (TACAS '96, Passau, Germany, Mar.). 146-166.]]

[16]

LOWE, G. 1997. Casper: A compiler for the analysis of security protocols. In Proceedings of the 1997 IEEE Computer Society Symposium on Research in Security and Privacy (Oakland, CA, May). IEEE Computer Society Press, Los Alamitos, CA, 18-30.]]

[17]

MEADOWS, C. 1994. The NRL protocol analyzer: An overview. In Proceedings of the Second International Conference on Practical Applications of Prolog.]]

[18]

MITCHELL, J., MITCHELL, M., AND STERN, U. 1997. Automated analysis of cryptographic protocols using Mur f.InProceedings of the 1997 IEEE Symposium on Research in Security and Privacy. IEEE Computer Society Press, Los Alamitos, CA, 141-153.]]

[19]

NEEDHAM, R. AND SCHROEDER, M. 1978. Using encryption for authentication in large networks of computers. Commun. ACM 21, 12 (Dec.), 993-999.]]

[20]

PAULSON, L. 1997a. Mechanized proofs of security protocols: Needham-schroeder with public keys. Tech. Rep. 413. Cambridge Univ., Cambridge, MA.]]

[21]

PAULSON, L. 1997b. Proving properties of security protocols by induction. In Proceedings of the 1997 IEEE Computer Society Symposium on Research in Security and Privacy (Oakland, CA, May). IEEE Computer Society Press, Los Alamitos, CA, 70-83.]]

[22]

PELED, D. 1996. Combining partial order reductions with on-the-fly model-checking. Formal Methods Syst. Des. 8,1,39-64.]]

[23]

PRAWITZ, D. 1965. Natural Deduction: A Proof-Theoretical Study. Almquist and Wiskell International, Stockholm, Sweden.]]

[24]

SCHNEIER, B. 1996. Applied Cryptography: Protocols, Algorithms, and Source Code in C. 2nd ed. John Wiley and Sons, Inc., New York, NY.]]

[25]

SHMATIKOV, V. AND STERN, U. 1998. Efficient finite-state analysis for large security protocols. In Proceedings on 11th IEEE Computer Security Foundation Workshop (CSFW'98, Rockport, MA, June). IEEE Press, Piscataway, NJ.]]

[26]

SONG, D., BEREZIN, S., AND PERRIG, A. 2001. Athena: a novel approach to efficient automatic security protocol analysis. J. Comput. Secur. 7. To be published.]]

[27]

THAYER, F. J., HERZOG, J. C., AND GUTTMAN, J. D. 1998. Strand spaces: Why is a security protocol correct? In Proceedings of the 1998 IEEE Symposium on Security and Privacy (Oakland, CA, May). IEEE Computer Society Press, Los Alamitos, CA, 160-171.]]

[28]

VALMARI, A. 1991. Stubborn sets of colored petri nets. In Proceedings of the 12th International Conference on Application and Theory of Petri Nets (Gjern, Denmark). 102-121.]]

[29]

WOO, T. AND LAM, S. 1993. A semantic model for authentication protocols. In Proceedings of the 1993 IEEE Symposium on Security and Privacy. IEEE Press, Piscataway, NJ, 178-194.]]

Cited By

Wang Q(2024)Applying SPIN checker on 5G EAP-TLS authentication protocol analysisComputer Science and Information Systems10.2298/CSIS230611068W21:1(21-36)Online publication date: 2024
https://doi.org/10.2298/CSIS230611068W
Arias JOlarte CPenczek WPetrucci LSidoruk T(2024)Model Checking and Synthesis for Strategic Timed CTL using Strategies in Rewriting LogicProceedings of the 26th International Symposium on Principles and Practice of Declarative Programming10.1145/3678232.3678240(1-14)Online publication date: 9-Sep-2024
https://dl.acm.org/doi/10.1145/3678232.3678240
Zhang JGao XYang LFeng TLi DWang Q(2021)A Systematic Approach to Formal Analysis of QUIC Handshake Protocol Using Symbolic Model CheckingSecurity and Communication Networks10.1155/2021/16302232021Online publication date: 1-Jan-2021
https://dl.acm.org/doi/10.1155/2021/1630223
Show More Cited By

Index Terms

Verifying security protocols with Brutus

Recommendations

Verifying security properties of internet protocol stacks: The split verification approach

We propose a novel method to construct user-space internet protocol stacks whose security properties can be formally explored and verified. The proposed method allows construction of protocol stacks using a C++ subset. We define a formal state-...
Verification of security protocols using LOTOS-method and application

We explain how the formal language LOTOS can be used to specify security protocols and cryptographic operations. We describe how security properties can be modelled as safety properties and how a model-based verification method can be used to verify the ...
Verifying security protocols by knowledge analysis

This paper describes a new interactive method to analyse knowledge of participants involved in security protocols and further to verify the correctness of the protocols. The method can detect attacks and flaws involving interleaving sessions besides ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Transactions on Software Engineering and Methodology

ACM Transactions on Software Engineering and Methodology Volume 9, Issue 4

Oct. 2000

188 pages

ISSN:1049-331X

EISSN:1557-7392

DOI:10.1145/363516

Editor:
Axel van Lamsweerde
Univ. Catholique de Louvain, Louvain-la-Neuve, Belgium

Issue’s Table of Contents

Copyright © 2000 ACM.

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 01 October 2000

Published in TOSEM Volume 9, Issue 4

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

87
Total Citations
View Citations
1,521
Total Downloads

Downloads (Last 12 months)104
Downloads (Last 6 weeks)8

Reflects downloads up to 30 Dec 2024

Other Metrics

View Author Metrics

Citations

Cited By

Wang Q(2024)Applying SPIN checker on 5G EAP-TLS authentication protocol analysisComputer Science and Information Systems10.2298/CSIS230611068W21:1(21-36)Online publication date: 2024
https://doi.org/10.2298/CSIS230611068W
Arias JOlarte CPenczek WPetrucci LSidoruk T(2024)Model Checking and Synthesis for Strategic Timed CTL using Strategies in Rewriting LogicProceedings of the 26th International Symposium on Principles and Practice of Declarative Programming10.1145/3678232.3678240(1-14)Online publication date: 9-Sep-2024
https://dl.acm.org/doi/10.1145/3678232.3678240
Zhang JGao XYang LFeng TLi DWang Q(2021)A Systematic Approach to Formal Analysis of QUIC Handshake Protocol Using Symbolic Model CheckingSecurity and Communication Networks10.1155/2021/16302232021Online publication date: 1-Jan-2021
https://dl.acm.org/doi/10.1155/2021/1630223
Hassan AIshaq IMinilla J(2021)Automated verification tools for cryptographic protocols2021 International Conference on Promising Electronic Technologies (ICPET)10.1109/ICPET53277.2021.00017(58-65)Online publication date: Nov-2021
https://doi.org/10.1109/ICPET53277.2021.00017
Zhang JYang LGao XTang GZhang JWang Q(2021)Formal Analysis of QUIC Handshake Protocol Using Symbolic Model CheckingIEEE Access10.1109/ACCESS.2021.30525789(14836-14848)Online publication date: 2021
https://doi.org/10.1109/ACCESS.2021.3052578
Aribi NLebbah Y(2020)A SAT-Based Planning Approach for Finding Logical Attacks on Cryptographic ProtocolsInternational Journal of Information Security and Privacy10.4018/IJISP.202010010114:4(1-21)Online publication date: 1-Oct-2020
https://doi.org/10.4018/IJISP.2020100101
Zhang JYang LGao XWang Q(2020)Formal analysis of QUIC handshake protocol using ProVerif2020 7th IEEE International Conference on Cyber Security and Cloud Computing (CSCloud)/2020 6th IEEE International Conference on Edge Computing and Scalable Cloud (EdgeCom)10.1109/CSCloud-EdgeCom49738.2020.00030(132-138)Online publication date: Aug-2020
https://doi.org/10.1109/CSCloud-EdgeCom49738.2020.00030
Zhang JYang LCao WWang Q(2020)Formal Analysis of 5G EAP-TLS Authentication Protocol Using ProverifIEEE Access10.1109/ACCESS.2020.29694748(23674-23688)Online publication date: 2020
https://doi.org/10.1109/ACCESS.2020.2969474
Basin DCremers CMeadows C(2018)Model Checking Security ProtocolsHandbook of Model Checking10.1007/978-3-319-10575-8_22(727-762)Online publication date: 19-May-2018
https://doi.org/10.1007/978-3-319-10575-8_22
Chau SChowdhury OHoque EGe HKate ANita-Rotaru CLi N(2017)SymCerts: Practical Symbolic Execution for Exposing Noncompliance in X.509 Certificate Validation Implementations2017 IEEE Symposium on Security and Privacy (SP)10.1109/SP.2017.40(503-520)Online publication date: May-2017
https://doi.org/10.1109/SP.2017.40
Show More Cited By

View Options

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Article

Media

Figures

Other

Tables

View Issue’s Table of Contents