A security protocol is a distributed program that can be executed by several actors. Since several runs of the protocol within the same execution are allowed, the protocol models are often infinite and very hard to analyze. In this paper we present a formal reasoning for evaluating security protocol correctness with respect to secrecy and authentication. We build a bounding model for multi-session cryptoprotocol attacks and prove that this model is appropriate for the analysis of the intruder's possible behavior and for demonstrating protocol correctness with respect to both secrecy and authentication. The result allows us to evaluate accurately the intruder's knowledge and his potential actions for building winning strategies during an attack.
IOS Press, Inc.
6751 Tepper Drive
Clifton, VA 20124
Tel.: +1 703 830 6300
Fax: +1 703 830 2300 firstname.lastname@example.org
(Corporate matters and books only) IOS Press c/o Accucoms US, Inc.
For North America Sales and Customer Service
West Point Commons
Lansdale PA 19446
Tel.: +1 866 855 8967
Fax: +1 215 660 5042 email@example.com