| 引用本文： |
-
张磊,许弘可,肖超恩,王建新,郑玉崝.基于进程代数的SP网络结构密码形式化设计研究[J].信息安全学报,已采用 [点击复制]
- ZHANG Lei,XU Hongke,XIAO Chaoen,WANG Jianxin,ZHENG Yuzheng.Research on Formal Design of SP Network Cipher based on Process Algebra[J].Journal of Cyber Security,Accept [点击复制]
|
|
| 摘要: |
| 针对以往代换-置换（SP）网络结构密码算法的设计与实现主要依赖设计者的经验手工实现，导致设计过程中不可避免的主观性和不一致性的问题，本文提出了一种基于进程代数从组件层次描述SP网络结构密码的形式化设计方法。首先提出了面向密码算法开发的MCL元密码语言设计原则，为后续形式化描述奠定基础。其次，通过对SP网络结构密码的特点进行分析，基于进程代数提出了四大组件，对四大组件在设计SP网络结构密码算法中的使用进行了说明，用于对SP结构密码进行形式化设计描述。最后，通过该形式化设计方法，建立了TANGRAM密码算法和SM4密码算法的形式化模型，阐述了形式化模型设计在处理复杂的SP网络结构密码算法的关键难点和技术挑战，基于形式化模型搭建了密码算法的MCL元密码模型，同时在MetaCrypto平台下进行了正确性验证。验证结果表明，基于本方法能实现轻量级TANGRAM加密算法的设计与实现；同时，针对SM4密码算法中的SP网络结构也能正确的建模与实现；并与传统设计方法比较，形式化设计方法在系统性、准确性、可维护性和适用性方面均优于传统设计方法。这一设计方法不仅为SP网络结构密码的设计过程提供了坚实的理论基础，确保了设计的系统性和准确性，还为密码算法的形式化设计提供了一种创新性的途径。 |
| 关键词: MCL元密码语言，形式化设计，SP网络结构密码，进程代数，TANGRAM |
| DOI： |
| 投稿时间：2024-03-31修订日期：2024-09-24 |
| 基金项目:中央高校基本科研业务费资金资助（328202205，328202271，328202269）；中央高校基本科研业务费（应用研究类）（2023A03）；教育部新工科研究与实践项目（E-AQGABQ20202704）；北京高等教育“本科教学改革创新项目”（202110018002）；北京电子科技学院一流学科建设项目（20210064Z0401、20210056Z0402） |
|
| Research on Formal Design of SP Network Cipher based on Process Algebra |
|
ZHANG Lei, XU Hongke, XIAO Chaoen, WANG Jianxin, ZHENG Yuzheng
|
| (北京电子科技学院) |
| Abstract: |
| In view of the problem that subjectivity and inconsistency in the design and implementation of traditional Substitu-tion-Permutation (SP) network structure cryptographic algorithms, which mainly rely on the designer's experience and manual implementation, this paper proposes a formal design method based on process algebra to describe the structure of SP network cipher algorithms from the component level. Firstly, the design principles of MCL (MetaCrypto Language) oriented to cryptographic algorithm development are proposed, which lays a foundation for the subsequent formal de-scription.. Secondly, through the analysis of the characteristics of SP network structure cryptography algorithm, four components based on process algebra are proposed based on process algebra, and the use of the four components in de-signing SP network structure ciphers is explained, which is used to formally design and describe SP structure ciphers. Finally, the formal models of TANGRAM cryptography algorithm and SM4 cryptography algorithm are established by using the formal design method, and the key difficulties and technical challenges of formal model design in dealing with complex SP network structure cryptographic algorithms are described. Based on the formal model, MCL model of cipher algorithm is built, which provides a solid theoretical support for the design of block cipher algorithm based on MCL. The correctness is verified by MetaCrypto platform. The verification results show that the design and implementation of lightweight TANGRAM encryption algorithm can be realized based on this method. At the same time, the SP network structure in SM4 cryptographic algorithm can be modeled and implemented correctly. Compared with traditional design methods, formal design methods are superior to traditional design methods in terms of systematicness, accuracy, maintainability and applicability. The proposed design method not only provides a solid theoretical foundation for the design process of SP network structure cryptography, ensuring systematic and accurate design, but also offers an innovative path for the formal design of cryptographic algorithms. |
| Key words: MetaCrypto Language, Formal Design, SP Network Cipher, Process Algebra, TANGRAM |
