Uncovering attacks on security protocols

Security protocols are indispensable in secure communication. We give an operational semantics of security protocols in terms of a Prolog-like language. With this semantics, we can uncover attacks on a security protocol that are possible with no more than a given number of rounds. Though our approach is exhaustive testing, the majority of fruitless search is cut off by selecting a small number of representative values that could be sent by an attacker. Hence, the number of scenarios is relatively small and our method is quite practical. Furthermore, our method not only reports possible attacks but also describes the attacks in great detail. This description would be very helpful to protocol designers and analyzers.