Fair exchange protocols play a critical role in enabling two distrustful entities to conduct electronic data exchanges in a fair and secure manner.These protocols are widely used in electronic payment systems and elec...Fair exchange protocols play a critical role in enabling two distrustful entities to conduct electronic data exchanges in a fair and secure manner.These protocols are widely used in electronic payment systems and electronic contract signing,ensuring the reliability and security of network transactions.In order to address the limitations of current research methods and enhance the analytical capabilities for fair exchange protocols,this paper proposes a formal model for analyzing such protocols.The proposed model begins with a thorough analysis of fair exchange protocols,followed by the formal definition of fairness.This definition accurately captures the inherent requirements of fair exchange protocols.Building upon event logic,the model incorporates the time factor into predicates and introduces knowledge set axioms.This enhancement empowers the improved logic to effectively describe the state and knowledge of protocol participants at different time points,facilitating reasoning about their acquired knowledge.To maximize the intruder’s capabilities,channel errors are translated into the behaviors of the intruder.The participants are further categorized into honest participants and malicious participants,enabling a comprehensive evaluation of the intruder’s potential impact.By employing a typical fair exchange protocol as an illustrative example,this paper demonstrates the detailed steps of utilizing the proposed model for protocol analysis.The entire process of protocol execution under attack scenarios is presented,shedding light on the underlying reasons for the attacks and proposing corresponding countermeasures.The developedmodel enhances the ability to reason about and evaluate the security properties of fair exchange protocols,thereby contributing to the advancement of secure network transactions.展开更多
An efficient approach to analyzing cryptographic protocols is to develop automatic analysis tools based on formal methods. However, the approach has encountered the high computational complexity problem due to reasons...An efficient approach to analyzing cryptographic protocols is to develop automatic analysis tools based on formal methods. However, the approach has encountered the high computational complexity problem due to reasons that participants of protocols are arbitrary, their message concurrent. We propose an efficient structures are complex and their executions are automatic verifying algorithm for analyzing cryptographic protocols based on the Cryptographic Protocol Algebra （CPA） model proposed recently, in which algebraic techniques are used to simplify the description of cryptographic protocols and their executions. Redundant states generated in the analysis processes are much reduced by introducing a new algebraic technique called Universal Polynomial Equation and the algorithm can be used to verify the correctness of protocols in the infinite states space. We have implemented an efficient automatic analysis tool for cryptographic protocols, called ACT-SPA, based on this algorithm, and used the tool to check more than 20 cryptographic protocols. The analysis results show that this tool is more efficient, and an attack instance not offered previously is checked by using this tool.展开更多
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 an...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 participants 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.展开更多
探讨了形式化分析在设计密码认证协议中的作用;基于Needham Schroeder共享密钥协议和Ot way Rees协议,提出了新的认证协议,并用BAN逻辑对它进行形式分析,发现了潜在的攻击方法,指出形式分析可以辅助发现协议的设计缺陷;并讨论了这种分...探讨了形式化分析在设计密码认证协议中的作用;基于Needham Schroeder共享密钥协议和Ot way Rees协议,提出了新的认证协议,并用BAN逻辑对它进行形式分析,发现了潜在的攻击方法,指出形式分析可以辅助发现协议的设计缺陷;并讨论了这种分析的局限性以及可能的改进方向.展开更多
基金the National Natural Science Foundation of China(Nos.61562026,61962020)Academic and Technical Leaders of Major Disciplines in Jiangxi Province(No.20172BCB22015)+1 种基金Special Fund Project for Postgraduate Innovation in Jiangxi Province(No.YC2020-B1141)Jiangxi Provincial Natural Science Foundation(No.20224ACB202006).
文摘Fair exchange protocols play a critical role in enabling two distrustful entities to conduct electronic data exchanges in a fair and secure manner.These protocols are widely used in electronic payment systems and electronic contract signing,ensuring the reliability and security of network transactions.In order to address the limitations of current research methods and enhance the analytical capabilities for fair exchange protocols,this paper proposes a formal model for analyzing such protocols.The proposed model begins with a thorough analysis of fair exchange protocols,followed by the formal definition of fairness.This definition accurately captures the inherent requirements of fair exchange protocols.Building upon event logic,the model incorporates the time factor into predicates and introduces knowledge set axioms.This enhancement empowers the improved logic to effectively describe the state and knowledge of protocol participants at different time points,facilitating reasoning about their acquired knowledge.To maximize the intruder’s capabilities,channel errors are translated into the behaviors of the intruder.The participants are further categorized into honest participants and malicious participants,enabling a comprehensive evaluation of the intruder’s potential impact.By employing a typical fair exchange protocol as an illustrative example,this paper demonstrates the detailed steps of utilizing the proposed model for protocol analysis.The entire process of protocol execution under attack scenarios is presented,shedding light on the underlying reasons for the attacks and proposing corresponding countermeasures.The developedmodel enhances the ability to reason about and evaluate the security properties of fair exchange protocols,thereby contributing to the advancement of secure network transactions.
基金supported by the National Natural Science Foundation of China(Grant No.90412011)the State Key Basic Research Program(973)(Grant No.2005CB321803)the State"863"High-tech Research and Development Project(Grant No.2003AA 144150).
文摘An efficient approach to analyzing cryptographic protocols is to develop automatic analysis tools based on formal methods. However, the approach has encountered the high computational complexity problem due to reasons that participants of protocols are arbitrary, their message concurrent. We propose an efficient structures are complex and their executions are automatic verifying algorithm for analyzing cryptographic protocols based on the Cryptographic Protocol Algebra （CPA） model proposed recently, in which algebraic techniques are used to simplify the description of cryptographic protocols and their executions. Redundant states generated in the analysis processes are much reduced by introducing a new algebraic technique called Universal Polynomial Equation and the algorithm can be used to verify the correctness of protocols in the infinite states space. We have implemented an efficient automatic analysis tool for cryptographic protocols, called ACT-SPA, based on this algorithm, and used the tool to check more than 20 cryptographic protocols. The analysis results show that this tool is more efficient, and an attack instance not offered previously is checked by using this tool.
文摘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 participants 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.
