安全协议形式化分析技术的应用与研究

作     者：冯皓楠 

作者单位：北京邮电大学 

学位级别：硕士

导师姓名：李晖

授予年度：2021年

学科分类：07[理学] 070104[理学-应用数学] 0701[理学-数学] 

主      题：安全协议 形式化分析 ProVerif FIDO UAF 

摘      要：安全协议运用密码算法,实现认证和密钥分配等目标。但是安全协议本身仍然存在安全隐患,对安全协议的各类攻击,导致个人、企业或国家机密信息泄露,造成财产损失。借助计算机和数学手段,形式化分析技术可以自动、快速和全面地对安全协议进行分析,不但能寻找安全协议的漏洞,还可以证明协议的安全性。该技术自提出以来,已经被应用到大量协议的分析中,促进了安全协议的研究与发展。但是,形式化分析技术目前仍旧不够成熟。本文对安全协议的形式化分析技术进行应用与研究,深入探讨了ProVerif形式化分析工具的原理,提出了利用ProVerif工具对安全协议进行形式化分析的方法,并以FIDO UAF为例进行了验证分析,最后对ProVerif和形式化分析方法进行了评估,找到了 ProVerif工具以及形式化分析方法的相关缺陷,并提出了改进方案。本文的主要工作和创新点包括:(1)提出了一种基于ProVerif的安全协议形式化分析方法,该方法提出了进程通信模型下恶意实体的建模方法、不可链接性的验证方法以及最小化假设的验证方法。(2)使用本文提出的方法对UAF协议进行形式化分析。首先对UAF协议的文档进行梳理,并对协议流程、安全假设、安全目标进行形式化翻译。其次提出UAF协议的ProVerif模型,开发UAFVerif工具,对UAF协议的所有可能场景进行分析,并自动寻找协议的最小化安全假设。在此基础上,论文提出针对UAF协议的攻击方式,成功将认证器重绑定攻击实施在两类应用中,获得CNNVD漏洞。最后提出了对UAF协议的改进建议。(3)总结ProVerif工具以及形式化分析过程的缺陷并提出了改进方案,其中包括ProVerif难以支持非Dolev-Yao模型下的协议分析、难以支持复杂的数学操作和计数器模型、不支持实体操作可变下认证性的分析以及难以支持实体遭到破坏的场景下不可链接性的分析等。