Computer Science

Computer Science ›› 2021, Vol. 48 ›› Issue (6A): 481-484.doi: 10.11896/jsjkx.200500074

• Information Security • Previous Articles     Next Articles

Formal Verification of Yahalom Protocol Based on Process Algebra

WANG Ran-ran1, WANG Yong1, CAI Yu-tong1, JIANG Zheng-tao2, DAI Gui-ping3   

  1. 1 College of Computer Science and Technology,Faculty of Information Technology,Beijing University of Technology,Beijing 100124,China
    2 School of Computer Science and Cybersecurity,Communication University of China,Beijing 100024,China
    3 College of Artificial Intelligence and Automation,Faculty of Information Technology,Beijing University of Technology,Beijing 100124,China
  • Online:2021-06-10 Published:2021-06-17
  • About author:WANG Ran-ran,born in 1996,postgraduate.Her main research interests include big data and deep learning.
  • Supported by:
    Guangxi Key Laboratory of Cryptography and Information Security Research Project(GCIS201808).

PDF (PC)

624

Abstract: 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.

Key words: ACP axiom system, Algebra process, Formal verification, Trusted third party, Yahalom protocol

CLC Number: 

  • TP301.2
[1] CHOO K K R.A Proof of Revised Yahalom Protocol in the Bellare and Rogaway (1993) Model[J].The Computer Journal,2007,50:591-601.
[2] ZAJAC B P.Applied cryptography:Protocols,algorithms,andsource code in C[J].Computers & Security,1994,13(3):217-218.
[3] FOKKINK W.Introduction to Process Algebra[J].Texts inTheoretical Computer Science An Eatcs,2000:1-163.
[4] VAGLINI G.Communication and concurrency:R Milner Prentice Hall (1989) 260pp 17.95 softback[J].Information and Software Technology,1991,33(6):462.
[5] HOARE T,HEARN P O.Separation Logic Semantics for Communicating Processes[J].NULL,2008,212:3-25.
[6] BERGSTRA J A,KLOP J W.Algebra of communicating processes with abstraction[J].Theoretical Computer Science,1985,37:77-121.
[7] 王勇,许荣强,任兴田,等.可信计算中信任链建立的形式化验证[J].北京工业大学学报,2016,42(3):73-78.
[8] 王勇,方娟,任兴田,等.基于进程代数的TCG远程证明协议的形式化验证[J].计算机研究与发展,2013(2):103-109.
[1] JIAN Qi-rui, CHEN Ze-mao, WU Xiao-kang. Authentication and Key Agreement Protocol for UAV Communication [J]. Computer Science, 2022, 49(8): 306-313.
[2] LI Ling, LI Huang-hua, WANG Sheng-yuan. Experiment on Formal Verification Process of Parser of CompCert Compiler in Trusted Compiler Design [J]. Computer Science, 2020, 47(6): 8-15.
[3] FAN Yong-qian, CHEN Gang, CUI Min. Formalization of Finite Field GF(2n) Based on COQ [J]. Computer Science, 2020, 47(12): 311-318.
[4] DONG Qi-ying, SHAN Xuan, JIA Chun-fu. Impact of Zipf's Law on Password-related Security Protocols [J]. Computer Science, 2020, 47(11): 42-47.
[5] MA Zhen-wei,CHEN Gang. Matrix Formalization Based on Coq Record [J]. Computer Science, 2019, 46(7): 139-145.
[6] GAN Yong, WANG Kai, HE Lei. Ownership Transfer Protocol for Multi-owners Internal Weight Changes with Trusted Third Party [J]. Computer Science, 2019, 46(6A): 370-374.
[7] CHEN Hao, LUO Lei, LI Yun, CHEN Li-rong. Study on Formal Verification of Secure Virtual Machine Monitor [J]. Computer Science, 2019, 46(3): 170-179.
[8] ZHANG Guang-hua, LIU Hui-meng, CHEN Zhen-guo. Attribute-based Revocation Scheme in Cloud Computing Environment [J]. Computer Science, 2018, 45(8): 134-140.
[9] JIN Yu, CAI Chao, HE Heng and LI Peng. BTDA:Dynamic Cloud Data Updating Audit Scheme Based on Semi-trusted Third Party [J]. Computer Science, 2018, 45(3): 144-150.
[10] LI Yan-chun, LI Xiao-juan, GUAN Yong, WANG Rui, ZHANG Jie and WEI Hong-xing. xMAS-based Formal Verification of SpaceWire Credit Logic [J]. Computer Science, 2016, 43(2): 113-117.
[11] YANG Xiu-mei, GUAN Yong, SHI Zhi-ping, WU Ai-xuan, ZHANG Qian-ying and ZHANG Jie. Higher-order Logic Formalization of Function Matrix and its Calculus [J]. Computer Science, 2016, 43(11): 24-29.
[12] CHEN Li-rong, LI Yun and LUO Lei. Research on Formal Verification of Embedded Operating System [J]. Computer Science, 2015, 42(8): 203-214.
[13] WANG Pei-xue and ZHOU Hua-qiang. Research on Cloud Security Model Based on Trusted Third Party on Multi-tenant Environment [J]. Computer Science, 2014, 41(Z6): 363-365.
[14] LIU Yang,YANG Fei,SHI Gang,YAN Xin,WANG Sheng-yuan and DONG Yuan. Brief Overview of Translation Validation Method in Trusted Compiler Construction [J]. Computer Science, 2014, 41(Z6): 334-338.
[15] ZHOU Kuan-jiu,REN Long-tao,WANG Xiao-long,YONG Jia-wei and HOU Gang. Modeling and Formal Verification for Software Designs Based on Hierarchical Timed State Transition Matrix [J]. Computer Science, 2014, 41(8): 42-46.
Viewed
Full text


Abstract

Cited
  Shared   
  Discussed   
No Suggested Reading articles found!
渝ICP备16013121号-4
Add:18# Honghu West Rd., Yubei ,Chongqing,China    Post Code: 401121
Tel: 023-63500828/023-67039612/023-67039623
E-mail: jsjkx12@163.com
Powered by Beijing Magtech Co., Ltd.