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

• 全文链接
• 请求原文

作   者：

王然然;  王勇;  蔡雨桐;  姜正涛;  代桂平; 

作者机构：

北京工业大学信息学部计算机学院;  北京工业大学信息学部人工智能与自动化学院;  中国传媒大学计算机与网络空间安全学院; 

关键词：

Yahalom协议;  可信第三方;  进程代数;  ACP公理系统;  形式化的验证; 

期刊名称：

计算机科学

i s s n：

1002-137X

年卷期：

2021 年 0S1 期

页   码：

481-484

摘   要：

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