Validation of Cryptographic Protocols by Efficient Automated Testing

Sigrid Gürgens, German National Research Center for Information Technology, Germany; and René Peralta, Yale University, USA

We present a method for validating cryptographic protocols. The method can find aws which are inherent in the design of the protocol as well as aws arising from the particular implementation of the protocol. The latter possibility arises from the fact that there is no universally accepted standard for describing either the cryptographic protocols themselves or their implementation. Thus, security can (and in practice does) depend on decisions made by the implementer, who may not have the necessary expertise. Our method relies on automatic theorem proving tools. Specifically, we used Otter, an automatic theorem proving software developed at Argonne National Laboratories.

This page is copyrighted by AAAI. All rights reserved. Your use of this site constitutes acceptance of all of AAAI's terms and conditions and privacy policy.