基于密钥链的认证邮件协议的扩展及形式化验证

摘要

随着电子商务的发展，认证邮件协议作为一种能够使协议的参与方都满足公平性的邮件协议，越来越受到人们的关注。认证邮件协议是公平交换协议的一种，它是指一个发送方需要将邮件的内容与接收方收到邮件的证据进行公平交换的协议。
　　 本论文首先研究了Cerderquist等人提出的基于密钥链的认证邮件协议，该协议采用密钥链来减少对可信第三方TTP(Trusted Third Party)的存储要求，并满足公平性、有效性和有限等待，但是并不能满足TTP透明性。TTP透明性是指任何人都无法判断TTP是否参与过邮件协议的执行过程，因此能保护TTP免于恶意曝光。鉴于TTP透明性在安全的认证邮件协议中的重要性，本课题采用一种基于双线性对的可验证加密签名机制将该协议进行扩展，使其在满足原有属性的基础上，能够满足可信第三方透明性。实验结果表明，扩展后的协议是满足属性最多，并且最高效的认证邮件协议之一。
　　 为了验证上述扩展协议的正确性，本课题采用了形式化验证方法对协议进行属性验证。形式化验证是指能够利用某一工具来自动的检测某一系统的模型是否能够满足所需属性的技术。该方法具有自动检测功能，因此检测比较全面，但是对系统建模和属性描述的精确性及技巧性要求极高。在验证扩展认证邮件协议的过程中，本课题首先选用模型检测工具Mocha来完成对公平性、有效性和有限等待这三种属性的形式化验证。Mocha允许的输入协议模型使用守卫命令语言来描述，需要检验的属性也均用转换时态逻辑ATL来描述。利用Mocha所建立的协议模型具有博弈属性，其参与方被模拟成不同的玩家，并且协议的属性也是用具有博弈性的语义逻辑来描述，因此，利用Mocha对认证邮件协议进行验证的过程就相当于博弈论中对获胜战略的计算过程。该方法能比较好的验证邮件协议是否满足公平性、有限等待和有效性。
　　 此外，对于可信第三方的透明性验证，本文的主要思路采用一种代数形式的语言μCRL来为协议建模，并在CADP工具的支持下得到获取证据的路径踪迹，然后进行比较。通过对这些路径踪迹的比较，最终得到了对透明性的验证结果。形式化验证的结果表明，本文所扩展的认证邮件协议完全满足公平性、有效性、有限等待和可信第三方透明性。

目录

文摘

英文文摘

第1章 绪论

1.1 论文的选题背景

1.1.1 研究背景

1.1.2 研究问题

1.2 国内外发展现状

1.2.1 认证邮件协议的发展现状

1.2.2 形式化验证的发展现状

1.3 论文的主要贡献

1.4 论文的主要工作

第2章 基于密钥连的认证邮件协议的扩展

2.1 基于密钥链的认证邮件协议

2.2 可信第三方TTP透明性

2.2.1 协议扩展

2.2.2 安全性分析

2.2.3 可验证加密机制

2.3 协议比较

第3章 认证邮件协议的形式化验证

3.1 Mocha中的形式化验证

3.1.1 ATS和ATL

3.1.2 模型检测工具Mocha

3.1.3 认证邮件协议建模-Mocha

3.1.4 认证邮件协议的属性描述

3.2 μCRL中的形式化验证

第4章 扩展协议的模型检测

4.1 扩展协议的自动化分析-Mocha

4.1.1 协议模型

4.1.2 模型分析

4.2 扩展协议的自动化分析-μCRL

4.2.1 数据类型

4.2.2 行为描述

4.2.3 协议模型

4.2.4 结果分析

第5章 总结和展望

参考文献

致谢

攻读学位期间发表的学术论文目录

攻读学位期间参与科研项目及获奖情况

学位论文评阅及答辩情况表