计算机科学

计算机科学 ›› 2021, Vol. 48 ›› Issue (6A): 481-484.doi: 10.11896/jsjkx.200500074

• 信息安全 • 上一篇    下一篇

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

王然然1, 王勇1, 蔡雨桐1, 姜正涛2, 代桂平3   

  1. 1 北京工业大学信息学部计算机学院 北京100124
    2 中国传媒大学计算机与网络空间安全学院 北京100024
    3 北京工业大学信息学部人工智能与自动化学院 北京100124
  • 出版日期:2021-06-10 发布日期:2021-06-17
  • 通讯作者: 王勇(wangy@bjut.edu.cn)
  • 作者简介:1092526108@qq.com
  • 基金资助:
    广西密码学与信息安全重点实验室研究课题(GCIS201808)

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)

620

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

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

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

中图分类号: 

  • 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] 蔡雨桐, 王勇, 王然然, 姜正涛, 代桂平.
基于进程代数的Otway-Rees协议的形式化验证
Formal Verification of Otway-Rees Protocol Based on Process Algebra
计算机科学, 2021, 48(6A): 477-480. https://doi.org/10.11896/jsjkx.200500072
[2] 董奇颖, 单轩, 贾春福.
口令Zipf分布对相关安全协议的影响分析
Impact of Zipf's Law on Password-related Security Protocols
计算机科学, 2020, 47(11): 42-47. https://doi.org/10.11896/jsjkx.200500144
[3] 甘勇, 王凯, 贺蕾.
带TTP的多所有者内部权重变化所有权转换协议
Ownership Transfer Protocol for Multi-owners Internal Weight Changes with Trusted Third Party
计算机科学, 2019, 46(6A): 370-374.
[4] 张光华, 刘会梦, 陈振国.
云计算环境下基于属性的撤销方案
Attribute-based Revocation Scheme in Cloud Computing Environment
计算机科学, 2018, 45(8): 134-140. https://doi.org/10.11896/j.issn.1002-137X.2018.08.024
[5] 金瑜,蔡超,何亨,李鹏.
BTDA:基于半可信第三方的动态云数据更新审计方案
BTDA:Dynamic Cloud Data Updating Audit Scheme Based on Semi-trusted Third Party
计算机科学, 2018, 45(3): 144-150. https://doi.org/10.11896/j.issn.1002-137X.2018.03.023
[6] 林雷蕾,周华,代飞,何臻力,沈勇,康洪炜.
一种基于代数语义的软件体系结构求精方法
Method of Software Architecture Refinement Based on Algebraic Semantics
计算机科学, 2017, 44(7): 141-146. https://doi.org/10.11896/j.issn.1002-137X.2017.07.026
[7] 郑明,李彤,林英,周小煊,李响,明利.
构件系统建模及其动态演化一致性验证方法
Dynamic Evolution Consistency Verification Method for Component System Modeling
计算机科学, 2017, 44(11): 80-86. https://doi.org/10.11896/j.issn.1002-137X.2017.11.012
[8] 王佩雪,周华强.
多租户环境下基于可信第三方的云安全模型研究
Research on Cloud Security Model Based on Trusted Third Party on Multi-tenant Environment
计算机科学, 2014, 41(Z6): 363-365.
[9] 谢仲文,李晓燕,李彤,代飞,于倩,张璇.
一种将需求模型转换为软件体系结构模型的方法
Approach of Transformation from Requirements Models to Software Architecture Models
计算机科学, 2014, 41(5): 196-203. https://doi.org/10.11896/j.issn.1002-137X.2014.05.041
[10] 张威.
弱共变-逆变模拟的公理刻画
Axiomatizing Weak Covariant-contravariant Simulation Semantics
计算机科学, 2014, 41(11): 99-102. https://doi.org/10.11896/j.issn.1002-137X.2014.11.019
[11] 朱锐,李彤,莫启,张璇,王一荃,林雷蕾,代飞.
基于EPMM的软件过程行为偏离诊断研究
Research on Deviation Diagnostic of Software Process Behavior Based on EPMM Modelling
计算机科学, 2014, 41(11): 56-62. https://doi.org/10.11896/j.issn.1002-137X.2014.11.012
[12] 李德胜，邓 娜，程 渤，陈俊亮.
一种用于粒子群优化的服务选择的扩展Pi演算
Extended Pi-calculus for Service Selection Using Particle Swarm Optimization
计算机科学, 2012, 39(Z11): 259-269.
[13] 王 勇，易 翔，李 凯，刘美林.
可信连接架构的形式化验证
Formal Verification of Trusted Connection Architecture
计算机科学, 2012, 39(Z11): 230-233.
[14] 贺靖靖 刘景森 史强 傅慧明.
基于PMI角色模型的匿名认证方案
Anonymous Authentication Scheme Based on Role Model of PMI
计算机科学, 2012, 39(Z11): 33-35.
[15] 王精明，虞慧群.
基于安全进程代数的非演绎安全模型的分析与验证
Security Process Algebra-based Analysis and Verification of Non-deducibility Security Model
计算机科学, 2012, 39(2): 56-58.
Viewed
Full text


Abstract

Cited
  Shared   
  Discussed   
No Suggested Reading articles found!
渝ICP备16013121号-4
地址：重庆市渝北区洪湖西路18号    邮编：401121  
电话：023-63500828（编辑部） 023-67039612（会议/专题） 023-67039623（财务/发票）
E-mail：jsjkx12@163.com
本系统由北京玛格泰克科技发展有限公司设计开发