论文部分内容阅读
安全协议的分析和验证是保证所设计的协议满足其安全性质的重要技术手段,而借助形式化的方法或工具分析安全协议是非常有效和有必要的。然而,形式化分析方法都将密码学原语抽象成符号化的操作,缺乏对于这些抽象的正确性的证明。因此,这些形式化方法不能用来证明当抽象的原语被实际简单协议或者密码学体制替换时,协议仍然是安全的。近年来,有学者提出将两种方法结合起来的框架:在保持形式化方法相对简单的情况下,使之也满足密码学可靠性。其中,UCSA(Universally Composable Symbolic Analysis)分析框架将形式化模型与UC框架结合起来,给出了证明一类协议密码学可靠性的一般方法。UCSA框架将Dolev-Yao模型中密码学抽象操作与UC框架中的理想功能进行了结合,使得通过形式化分析方法可以证明安全协议的在密码学环境下的一些性质。然而,UCSA框架在能够分析协议类型上有一定限制,只能分析一类顺序执行的有限状态协议,并且在协议中只能使用由不需要通信的本地算法所表示的密码学操作,如标准的公钥加密操作,或者标准签名操作。本文主要的工作是对UCSA框架进行扩展,主要成果和创新如下:1.对UCSA中的形式化分析框架进行了扩展,定义了基于PAPi演算的形式化分析框架。一方面,以进程演算为描述语言的协议能够直观的体现协议交互的特点;另一方面,PAPi演算中概率选择操作算子为形式化模型中的协议加入了在行为层进行概率选择的能力,扩展了形式化模型中能够描述和分析的协议类型;2.对网络通信假设进行了扩展。在扩展后的模型中支持敌手控制通信、认证通信、匿名通信(发送者匿名)等不同通信假设。而不同的假设是通过不同的辅助理想进程所描述,可以根据所分析的协议选择不同的通信模型;3.对密码学原语的抽象进行了扩展,加入了基于两方协议的密码学原语的抽象,如盲签协议,承诺协议等。描述理想协议抽象的辅助进程对应于UC框架下相应的理想功能,这使得形式化分析框架能够保持其UC框架可靠的性质;4.扩展了UC框架对应与形式化框架下简单协议的定义,使其能够使用更多的密码学操作和协议原语,并且具有在协议行为层进行概率选择的能力。5.以公平投掷硬币协议为例,给出了相应的形式化模型中安全判定准则和UC框架中相应理想功能的对应关系。