基于进程代数的Otway-Rees协议的形式化验证

doi:10.11896/jsjkx.200500072

计算机科学 ›› 2021, Vol. 48 ›› Issue (6A): 477-480.doi: 10.11896/jsjkx.200500072

基于进程代数的Otway-Rees协议的形式化验证

蔡雨桐¹, 王勇¹, 王然然¹, 姜正涛², 代桂平³

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

出版日期:2021-06-10 发布日期:2021-06-17
通讯作者: 王勇(wangy@bjut.edu.cn)
作者简介:1241282400@qq.com
基金资助:
广西密码学与信息安全重点实验室研究课题(GCIS201808)

Formal Verification of Otway-Rees Protocol Based on Process Algebra

CAI Yu-tong¹, WANG Yong¹, WANG Ran-ran¹, JIANG Zheng-tao², DAI Gui-ping³

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:CAI Yu-tong,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).

摘要/Abstract

摘要： Otway-Rees协议的目的是完成发起者和响应者之间的双向认证,并且分发服务器产生的会话密钥。该协议的特点是简单实用,没有使用复杂的同步时钟机制或双重加密,仅用少量的信息提供了良好的时效性。此协议允许通过一个网络的个别通信认证自己的身份,还可以阻止重放攻击和窃听,允许修改检测。对安全协议的分析是信息时代无法回避的关键问题,事实证明,形式化方法是安全协议分析更为可靠和有效的途径。此协议的形式化验证对于工程实施具有重要意义。对Otway-Rees协议进行抽象处理,得到抽象模型,在此基础上给出基于进程代数的形式化描述,并进行形式化验证。验证结果表明,此协议形式的并行系统展现出了期望的外部行为。

关键词: Otway-Rees, 安全协议, 进程代数, 协议验证, 形式化

Abstract: Otway-Rees protocol is to complete the two-way authentication between the initiator and the responder,and to distri-bute the session key generated by the server.The feature of this protocol is simple and practical.It does not use complicated synchronous clock mechanism or double encryption,and provides good timeliness with only a small amount of information.This protocol allows individual communications to be authenticated through a network,while also preventing replay attacks and eavesdropping,as well as modifying detection.The analysis of security protocols is a key issue that cannot be avoided in the information age.Formal method,which is based on strict mathematical and mechanical methods,is an important method to improve and ensure the quality of computing system.Its model,technology and tools have become an important carrier of computing thinking.The formal method can accurately reveal all kinds of logic rules,make corresponding logic rules,and make all kinds of theoretical systems more rigorous.Formal method is a mathematical description of what a program does,a description of the function of a program written in a formal language with precise semantics.It is not only the starting point of designing and programming,but also the basis of verifying whether a program is correct,so as to improve the reliability and robustness of the design.By abstracting the Otway-Rees protocol,we can get the abstract model.On this basis,the formal description based on process algebra is gi-ven and the formal verification is carried out.The verification results show that the parallel system in the form of this protocol shows the expected external behavior.

Key words: Formalization, Otway-Rees, Process algebra, Protocol verification, Security protoco

中图分类号:

TP301.2

蔡雨桐, 王勇, 王然然, 姜正涛, 代桂平. 基于进程代数的Otway-Rees协议的形式化验证[J]. 计算机科学, 2021, 48(6A): 477-480. https://doi.org/10.11896/jsjkx.200500072

CAI Yu-tong, WANG Yong, WANG Ran-ran, JIANG Zheng-tao, DAI Gui-ping. Formal Verification of Otway-Rees Protocol Based on Process Algebra[J]. Computer Science, 2021, 48(6A): 477-480. https://doi.org/10.11896/jsjkx.200500072

参考文献

[1] ZAJAC B P.Applied cryptography:Protocols, algorithms, and source code in C[J].Computers & Security,1994,13(3):217-218.
[2] OROS H,BOIAN F.Spi calculus analysis of Otway-Rees protocol[J].International Journal of Computers,Communications & Control (IJCCC),2008,3(3):427-432.
[3] Fokkink.Introduction to Process Algebra[J].Texts in Theoretical 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,O'HEARN P.Separation Logic Semantics for Communicating Processes[J].Electronic Notes in Theoretical Computer Science,2008,212:3-25.
[6] BERGSTRA J A,KLOP J W.Algebra of communicating processes with abstraction[J].Theoretical Computer Science,1985,37(85):77-121.
[7] 王勇,许荣强,任兴田,等.可信计算中信任链建立的形式化验证[J].北京工业大学学报,2016,42(3):73-78.
[8] 王勇,方娟,任兴田,等.基于进程代数的TCG远程证明协议的形式化验证[J].计算机研究与发展,2013(2):103-109.

相关文章 15

[1]	蹇奇芮, 陈泽茂, 武晓康. 面向无人机通信的认证和密钥协商协议 Authentication and Key Agreement Protocol for UAV Communication 计算机科学, 2022, 49(8): 306-313. https://doi.org/10.11896/jsjkx.220200098
[2]	杜金莲, 孙鹏飞, 金雪云. 一种用于威胁检测的反目标攻击树模型 Anti-target Attack Tree Model for Threat Detection 计算机科学, 2021, 48(6A): 468-476. https://doi.org/10.11896/jsjkx.200900205
[3]	王然然, 王勇, 蔡雨桐, 姜正涛, 代桂平. 基于进程代数的Yahalom协议正确性的形式化验证 Formal Verification of Yahalom Protocol Based on Process Algebra 计算机科学, 2021, 48(6A): 481-484. https://doi.org/10.11896/jsjkx.200500074
[4]	汪文轩, 胡军, 胡建成, 康介祥, 王辉, 高忠杰. 一种面向形式化表格需求模型的测试用例生成方法 Test Case Generation Method Oriented to Tabular Form Formal Requirement Model 计算机科学, 2021, 48(5): 16-24. https://doi.org/10.11896/jsjkx.201000048
[5]	倪亮, 王念平, 谷威力, 张茜, 刘伎昭, 单芳芳. 基于格的抗量子认证密钥协商协议研究综述 Research on Lattice-based Quantum-resistant Authenticated Key Agreement Protocols:A Survey 计算机科学, 2020, 47(9): 293-303. https://doi.org/10.11896/jsjkx.200400138
[6]	杨萍, 王生原. CompCert编译器目标代码生成机制分析 Analysis of Target Code Generation Mechanism of CompCert Compiler 计算机科学, 2020, 47(9): 17-23. https://doi.org/10.11896/jsjkx.200400018
[7]	李凌, 李璜华, 王生原. 在可信编译器设计中实践CompCert编译器的语法分析器形式化验证过程 Experiment on Formal Verification Process of Parser of CompCert Compiler in Trusted Compiler Design 计算机科学, 2020, 47(6): 8-15. https://doi.org/10.11896/jsjkx.191000173
[8]	纪程宇,朱雪峰. 设计模式组合操作优化研究 Study on Optimization of Design Pattern Combination Operation 计算机科学, 2020, 47(3): 19-24. https://doi.org/10.11896/jsjkx.190100046
[9]	范永乾, 陈钢, 崔敏. 基于COQ的有限域GF(2ⁿ)的形式化研究 Formalization of Finite Field GF(2ⁿ) Based on COQ 计算机科学, 2020, 47(12): 311-318. https://doi.org/10.11896/jsjkx.190900197
[10]	董奇颖, 单轩, 贾春福. 口令Zipf分布对相关安全协议的影响分析 Impact of Zipf's Law on Password-related Security Protocols 计算机科学, 2020, 47(11): 42-47. https://doi.org/10.11896/jsjkx.200500144
[11]	马振威,陈钢. 基于Coq记录的矩阵形式化方法 Matrix Formalization Based on Coq Record 计算机科学, 2019, 46(7): 139-145. https://doi.org/10.11896/j.issn.1002-137X.2019.07.022
[12]	陈昊,罗蕾,李允,陈丽蓉. 安全虚拟机监视器的形式化验证研究 Study on Formal Verification of Secure Virtual Machine Monitor 计算机科学, 2019, 46(3): 170-179. https://doi.org/10.11896/j.issn.1002-137X.2019.03.026
[13]	陈平,梁启明,孙伟. 面向系统能力的形式化分析和测试方法 System Capability-oriented Approach for Formalized Software Requirements Analysing and Testing 计算机科学, 2017, 44(Z6): 534-538. https://doi.org/10.11896/j.issn.1002-137X.2017.6A.119
[14]	王瑞云,赵国磊,常朝稳,王雪健. 典型安全网关的形式化设计与证明 Formal Design and Verification for Typical Security Gateway 计算机科学, 2017, 44(9): 142-147. https://doi.org/10.11896/j.issn.1002-137X.2017.09.028
[15]	宋岚,薛锦云,胡启敏,谢武平,江东明,游珍. 无线射频RFID识别协议自动验证方法研究 Research of Automatic Verification Method about Radio Frequency Identification Protocol 计算机科学, 2017, 44(9): 99-104. https://doi.org/10.11896/j.issn.1002-137X.2017.09.020

Metrics

Viewed

Full text

Abstract

Cited

Shared

Discussed

基于进程代数的Otway-Rees协议的形式化验证

Formal Verification of Otway-Rees Protocol Based on Process Algebra

PDF (PC)

摘要/Abstract

引用本文

使用本文

参考文献

相关文章 15

Metrics

本文评价

推荐阅读 0