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

Formal Verification of Yahalom Protocol Based on Process Algebra

作　　者：王然然 王勇 蔡雨桐 姜正涛[2] 代桂平 WANG Ran-ran;WANG Yong;CAI Yu-tong;JIANG Zheng-tao;DAI Gui-ping(College of Computer Science and Technology,Faculty of Information Technology,Beijing University of Technology,Beijing 100124,China;School of Computer Science and Cybersecurity,Communication University of China,Beijing 100024,China;College of Artificial Intelligence and Automation,Faculty of Information Technology,Beijing University of Technology,Beijing 100124,China)

机构地区：[1]北京工业大学信息学部计算机学院,北京100124 [2]中国传媒大学计算机与网络空间安全学院,北京100024 [3]北京工业大学信息学部人工智能与自动化学院,北京100124

出　　处：《计算机科学》2021年第S01期481-484,共4页Computer Science

基　　金：广西密码学与信息安全重点实验室研究课题(GCIS201808)。

摘　　要：通信过程中为了使得通信双方之间的对话过程是安全传输的,在引入可信第三方的基础上,Yahalom协议借助于可信第三方为通信双方分配"好"的会话密钥,利用该共享密钥加密对话内容保证双方对话的安全。Yahalom协议的形式化验证具有很重要的意义。为了使可信第三方在通信双方之间安全地分配会话密钥,文中对通信过程进行理论化形式的验证。文中基于可信平台的随机会话密钥分配过程进行了抽象化的处理,给出了抽象模型中各个实体状态及状态变迁的操作语义描述,建立了Yahalom协议结构化的操作语义并发计算模型,主要通过ACP公理系统对Yahalom协议的状态变迁系统进行了形式化的验证,验证结果表明Yahalom协议系统地展示了期望的外部行为,从理论上证明了基于进程代数的Yahalom协议是可行的。In the process of communication, in order to make the conversation between the two sides safe, Yahalom protocol uses the trusted third party to distribute the "good" conversation key to the two sides of communication, and uses the shared key to encrypt the conversation content to ensure the security of the conversation between the two sides.The formal verification of Yahalom protocol is of great significance.In order to make the trusted third party distribute the session key safely between the two sides of communication, this paper makes a theoretical verification of the communication process.In this paper, the process of random session key distribution based on trusted platform is abstracted, the operational semantic description of each entity’s state and state transition in the abstract model is given, and the structural operational semantic concurrent computing model of Yahalom protocol is established.The formal verification of Yahalom protocol’s state transition system is mainly carried out through ACP public system.The results show the expected external behavior, and theoretically proves that Yahalom protocol based on process algebra is feasible.

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

分 类 号：TP301.2[自动化与计算机技术—计算机系统结构]