基于进程代数的Yahalom协议正确性的形式化验证

摘要：

通信过程中为了使得通信双方之间的对话过程是安全传输的,在引入可信第三方的基础上,Yahalom协议借助于可信第三方为通信双方分配"好"的会话密钥,利用该共享密钥加密对话内容保证双方对话的安全.Yahalom协议的形式化验证具有很重要的意义.为了使可信第三方在通信双方之间安全地分配会话密钥,文中对通信过程进行理论化形式的验证.文中基于可信平台的随机会话密钥分配过程进行了抽象化的处理,给出了抽象模型中各个实体状态及状态变迁的操作语义描述,建立了Yahalom协议结构化的操作语义并发计算模型,主要通过ACP公理系统对Yahalom协议的状态变迁系统进行了形式化的验证,验证结果表明Yahalom协议系统地展示了期望的外部行为,从理论上证明了基于进程代数的Yahalom协议是可行的.

关键词：Yahalom协议、进程代数、形式化的验证、可信第三方、ACP公理系统

所属期刊栏目：48

分类号：TP301.2(计算技术、计算机技术)

资助基金：实验室研究项目GCIS201808

在线出版日期：2021-07-13（万方平台首次上网日期，不代表论文的发表时间）

页数：共4页

页码：481-484