Algebra model and security analysis for cryptographic protocols

被引:9
|
作者
Huai, JP [1 ]
Li, XX [1 ]
机构
[1] Beijing Univ Aeronaut & Astronaut, Sch Comp, Beijing 100083, Peoples R China
来源
基金
中国国家自然科学基金;
关键词
cryptographic protocol; formal analysis; information security; algebra system;
D O I
10.1360/02yf0185
中图分类号
TP [自动化技术、计算机技术];
学科分类号
0812 ;
摘要
More and more cryptographic protocols have been used to achieve various security requirements of distributed systems in the open network environment. However cryptographic protocols are very difficult to design and analyze due to the complexity of the cryptographic protocol execution, and a large number of problems are unsolved that range from the theory framework to the concrete analysis technique. In this paper, we build a new algebra called cryptographic protocol algebra (CPA) for describing the message operations with many cryptographic primitives, and proposed a new algebra model for cryptographic protocols based on the CPA. In the model, expanding processes of the participant's knowledge on the protocol runs are characterized with some algebraic notions such as subalgebra, free generator and polynomial algebra, and attack processes are modeled with a new notion similar to that of the exact sequence used in homological algebra. Then we develope a mathematical approach to the cryptographic protocol security analysis. By using algebraic techniques, we have shown that for those cryptographic protocols with some symmetric properties, the execution space generated by an arbitrary number of participants may boil down to a smaller space generated by several honest participants and attackers. Furthermore we discuss the composability problem of cryptographic protocols and give a sufficient condition under which the protocol composed of two correct cryptographic protocols is still correct, and we finally offer a counterexample to show that the statement may not be true when the condition is not met.
引用
收藏
页码:199 / 220
页数:22
相关论文
共 50 条
  • [41] CVS: a compiler for the analysis of cryptographic protocols
    Durante, A
    Focardi, R
    Gorrieri, R
    [J]. PROCEEDINGS OF THE 12TH IEEE COMPUTER SECURITY FOUNDATIONS WORKSHOP, 1999, : 203 - 212
  • [42] New analysis method of cryptographic protocols
    Qian, Y.
    Zhang, Y.
    Bai, Y.C.
    [J]. Jisuanji Gongcheng/Computer Engineering, 2001, 27 (03):
  • [43] Model Driven Security Analysis of IDaaS Protocols
    Kumar, Apurva
    [J]. SERVICE-ORIENTED COMPUTING, 2011, 7084 : 312 - 327
  • [44] Game-Based Automated Security Proofs for Cryptographic Protocols
    Gu Chunxiang
    Guang Yan
    Zhu Yuefei
    [J]. CHINA COMMUNICATIONS, 2011, 8 (04) : 50 - 57
  • [45] Mechanizing the Proof of Adaptive, Information-theoretic Security of Cryptographic Protocols in the Random Oracle Model
    Stoughton, Alley
    Varia, Mayank
    [J]. 2017 IEEE 30TH COMPUTER SECURITY FOUNDATIONS SYMPOSIUM (CSF), 2017, : 83 - 99
  • [46] A Study on Fine-Grained Security Properties of Cryptographic Protocols for Formal Analysis Method with Reasoning
    Yan, Jingchen
    Ishibashi, Sho
    Goto, Yuichi
    Cheng, Jingde
    [J]. 2018 IEEE SMARTWORLD, UBIQUITOUS INTELLIGENCE & COMPUTING, ADVANCED & TRUSTED COMPUTING, SCALABLE COMPUTING & COMMUNICATIONS, CLOUD & BIG DATA COMPUTING, INTERNET OF PEOPLE AND SMART CITY INNOVATION (SMARTWORLD/SCALCOM/UIC/ATC/CBDCOM/IOP/SCI), 2018, : 210 - 215
  • [47] Model-based testing of cryptographic protocols
    Rosenzweig, D
    Runje, D
    Schulte, W
    [J]. TRUSTWORTHY GLOBAL COMPUTING, 2005, 3705 : 33 - 60
  • [48] A cryptographic model for better information security
    Kumar, Sunil
    Kumar, Manish
    Budhiraja, Rajat
    Das, M. K.
    Singh, Sanjeev
    [J]. JOURNAL OF INFORMATION SECURITY AND APPLICATIONS, 2018, 43 : 123 - 138
  • [49] Deciding Security Properties for Cryptographic Protocols. Application to Key Cycles
    Comon-Lundh, Hubert
    Cortier, Veronique
    Zalinescu, Eugen
    [J]. ACM TRANSACTIONS ON COMPUTATIONAL LOGIC, 2010, 11 (02)
  • [50] Tracking Security Flaws in Cryptographic Protocols Using Witness-Functions
    Fattahi, Jaouhar
    Mejri, Mohamed
    Pricop, Emil
    [J]. 2015 IEEE INTERNATIONAL CONFERENCE ON SYSTEMS, MAN, AND CYBERNETICS (SMC 2015): BIG DATA ANALYTICS FOR HUMAN-CENTRIC SYSTEMS, 2015, : 1189 - 1196