Abstract: Formal method is an important way of verifying cryptographic protocols. Based on the deduction rules of Debbabi, a new approach is presented, which abstracts some data structures, such as principals’ids and keys, from the protocol, and then builds up the architecture of reasoning logic. By adverse deduction, all paths of attacks on Woo Lam protocol can be obained in terms of chart and all the flaws of the protocol can be analyzed thoroughly. Finally, suggestions about making the protocol more secure are given.