CAJ | 학술논문

通过应用实例研究了如何用Casper/FDR和串空间两种分析方法对通信协议进行形式化分析：用Casper/FDR对协议的有穷状态进行穷举验证，当发现协议漏洞时会自动给出攻击的迹，但是此方法会产生状态爆炸的问题；串空间方法正好可以解决状态爆炸问题，用串空间对协议的各种状态进行证明，但是如果发现了协议漏洞，该方法不能给出攻击者的迹。
통과응용실례연구료여하용Casper/FDR화천공간량충분석방법대통신협의진행형식화분석：용Casper/FDR대협의적유궁상태진행궁거험증，당발현협의루동시회자동급출공격적적，단시차방법회산생상태폭작적문제；천공간방법정호가이해결상태폭작문제，용천공간대협의적각충상태진행증명，단시여과발현료협의루동，해방법불능급출공격자적적。
Casper/FDR method and strand space method are studied with application examples.These exam-ples 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 meth-od 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.