目前,安全协议的形式化分析方法大致可以分为3类:形式逻辑方法、模型检测方法和定理证明方法。其中,模型检测方法也称作状态空间搜索法。模型检测技术采用形式化方法精确地证明一个系统能够按照预定目标正确工作。模型检测的基本思路是把安全协议看成一个分布式系统,而每个主体执行协议的过程构成局部状态,所有的局部状态则构成系统的全局状态,每个主体的消息接收和发送动作都会引起局部状态的改变,进而引起全局状态的改变,因此需要在系统可达的每个全局状态,对于安全协议分析来讲,模型检测技术已被证明是一条非常成功的途径。首先,这种方法的自动化程度高,在验证过程中不需要用户参与;其次,如果协议存在缺陷,能够自动产生反例。但因为容易产生状态空间爆炸问题,所以模型检测方法不能用于比较复杂的安全协议分析。
声明:本文内容及配图由入驻作者撰写或者入驻合作网站授权转载。文章观点仅代表作者本人,不代表电子发烧友网立场。文章及其配图仅供工程师学习之用,如有内容侵权或者其他违规问题,请联系本站处理。 举报投诉
全部0条评论
快来发表一下你的评论吧 !