中文摘要：

通过应用实例研究了如何用Casper/FDR和串空间两种分析方法对通信协议进行形式化分析：用Casper/FDR对协议的有穷状态进行穷举验证，当发现协议漏洞时会自动给出攻击的迹，但是此方法会产生状态爆炸的问题；串空间方法正好可以解决状态爆炸问题，用串空间对协议的各种状态进行证明，但是如果发现了协议漏洞，该方法不能给出攻击者的迹。

英文摘要：

Casper/FDR method and strand space method are studied with application examples. These examples show how to use these methods to analyze protocol. The Casper/FDR method can verify the status of the protocol, and the number of status is limited. When a loophole of the protocol is found, the tracks of attacker will be automatically given. This method will produce a state explosion problem. However, strand space method can solve this problem. Strand space for a variety of state protocol is proved. If a loophole in the protocol appears, the tracks of attacker cannot be found.