Under CopyrightGürgens, S.S.GürgensPeralta, R.R.Peralta2022-03-0707.08.20021998https://publica.fraunhofer.de/handle/publica/28981010.24406/publica-fhg-289810We present a search method for detecting potential security flaws in cryptographic protocols. The method can find flaws which are inherent in the design of the protocol as well as flaws 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.1 Introduction S.3 2 Cryptographic protocols S.4-8 - 2.1 Types of protocol aws S.6-8 3 The communication and attack model S.9-10 4 Automatic testing of protocol instantiations S.11-12 - see(action list,knowledge list,from agent,to agent,message, : : :) check( : : :) ::: S.11 - send(update(action list),update(knowledge list),new from agent, new to agent, new message, : : :). S.11 - 4.1 Known and new attacks S.11-12 5 Conclusions S.13 - Acknowledgments S.13 References S.14 A Appendix S.15-17enauthentication protocolsecurity analysisautomatic theorem provingcryptographic protocolmodel checkingcryptographyformal modelprotocol005004report