Denial of Service Distributed Denial of Service （DOS） attack, especially （DDoS） attack, is one of the greatest threats to Internet. Much research has been done for it by now, however, it is always concentrated in ...Denial of Service Distributed Denial of Service （DOS） attack, especially （DDoS） attack, is one of the greatest threats to Internet. Much research has been done for it by now, however, it is always concentrated in the behaviors of the network and can not deal with the problem exactly. In this paper, we start from the security of the protocol, then we propose a novel theory for security protocol analysis of Denial of Service in order to deal with the DoS attack. We first introduce the conception of weighted graph to extend the strand space model, then we extend the penetrator model and define the goal of anti-DoS attack through the conception of the DoS-stop protocol, finally we propose two kinds of DoS test model and erect the novel formal theory for security protocol analysis of Denial of Service. Our new formal theory is applied in two example protocols. It is proved that the Internet key exchange （IKE） easily suffers from the DoS attacks, and the efficient DoS- resistant secure key exchange protocol （JFK） is resistant against DoS attack for the server, respectively.展开更多
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.展开更多
To analyze the security of two-step quantum direct communication protocol （QDCP） by using Einstein-Podolsky Rosen pair proposed by Deng et al. [Phys. Rev. A 68 （2003）042317] in collective-rotation noise channel, a...To analyze the security of two-step quantum direct communication protocol （QDCP） by using Einstein-Podolsky Rosen pair proposed by Deng et al. [Phys. Rev. A 68 （2003）042317] in collective-rotation noise channel, an excellent model of noise analysis is proposed. In the security analysis, the method of the entropy theory is introduced, and is compared with QDCP, an error rate point Qo（M ： （Q0, 1.0）） is given. In different noise levels, if Eve wants to obtain the same amount of information, the error rate Q is distinguishable. The larger the noise level ~ is, the larger the error rate Q is. When the noise level ~ is lower than 11%, the high error rate is 0.153 without eavesdropping. Lastly, the security of the proposed protocol is discussed. It turns out that the quantum channel will be safe when Q 〈 0.153. Similarly, if error rate Q〉 0.153 = Q0, eavesdropping information I 〉 1, which means that there exist eavesdroppers in the quantum channel, and the quantum channel will not be safe anymore.展开更多
Security protocol is specified as the procedure of challenge-response, which uses applied cryptography to confirm the existence of other principals and fulfill some data negotiation such as session keys. Most of the e...Security protocol is specified as the procedure of challenge-response, which uses applied cryptography to confirm the existence of other principals and fulfill some data negotiation such as session keys. Most of the existing analysis methods, which either adopt theorem proving techniques such as state exploration or logic reasoning techniques such as authentication logic, face the conflicts between analysis power and operability. To solve the problem, a new efficient method is proposed that provides SSM semantics-based definition of secrecy and authentication goals and applies authentication logic as fundamental analysis techniques, in which secrecy analysis is split into two parts： Explicit-lnformaUon-Leakage and Implicit-Information-Leakage, and correspondence analysis is concluded as the analysis of the existence relationship of Strands and the agreement of Strand pa- rameters. This new method owns both the power of the Strand Space Model and concision of authentication logic.展开更多
This study developed a mail server program using Socket API and Python.The program uses the Hypertext Transfer Protocol(HTTP)to receive emails from browser clients and forward them to actual email service providers vi...This study developed a mail server program using Socket API and Python.The program uses the Hypertext Transfer Protocol(HTTP)to receive emails from browser clients and forward them to actual email service providers via the Simple Mail Transfer Protocol(SMTP).As a web server,it handles Transmission Control Protocol(TCP)connection requests from browsers,receives HTTP commands and email data,and temporarily stores the emails in a file.Simultaneously,as an SMTP client,the program establishes a TCP connection with the actual mail server,sends SMTP commands,and transmits the previously saved emails.In addition,we also analyzed security issues and the efficiency and availability of this server,providing insights into the design of SMTP mail servers.展开更多
Network protocol software is usually characterized by complicated functions and a vast state space.In this type of program,a massive number of stateful variables that are used to represent the evolution of the states ...Network protocol software is usually characterized by complicated functions and a vast state space.In this type of program,a massive number of stateful variables that are used to represent the evolution of the states and store some information about the sessions are prone to potentialflaws caused by violations of protocol specification requirements and program logic.Discovering such variables is significant in discovering and exploiting vulnerabilities in protocol software,and still needs massive manual verifications.In this paper,we propose a novel method that could automatically discover the use of stateful variables in network protocol software.The core idea is that a stateful variable features information of the communication entities and the software states,so it will exist in the form of a global or static variable during program execution.Based on recording and replaying a protocol program’s execution,varieties of variables in the life cycle can be tracked with the technique of dynamic instrument.We draw up some rules from multiple dimensions by taking full advantage of the existing vulnerability knowledge to determine whether the data stored in critical memory areas have stateful characteristics.We also implement a prototype system that can discover stateful variables automatically and then perform it on nine programs in Pro FuzzBench and two complex real-world software programs.With the help of available open-source code,the evaluation results show that the average true positive rate(TPR)can reach 82%and the average precision can be approximately up to 96%.展开更多
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.展开更多
IEEE 802.16e, as an amendment and corrigendum to the IEEE 802.16-2004, published on 28 February 2006, and intended to update and expand IEEE 802.16-2004 to allow for mobile subscriber stations. This paper summarizes t...IEEE 802.16e, as an amendment and corrigendum to the IEEE 802.16-2004, published on 28 February 2006, and intended to update and expand IEEE 802.16-2004 to allow for mobile subscriber stations. This paper summarizes the key management protocol belonging to security part of the IEEE 802.16e, which includes security negotiation, authorization, key derivation, handshake, and key transportation. While these building blocks are well designed, we point out some unwelcome features for these building blocks. We also give out suggestions to diminish the proposed problems.展开更多
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.展开更多
基金This work is supported by National Natural Science Foundation of China under contract 60902008.
文摘Denial of Service Distributed Denial of Service （DOS） attack, especially （DDoS） attack, is one of the greatest threats to Internet. Much research has been done for it by now, however, it is always concentrated in the behaviors of the network and can not deal with the problem exactly. In this paper, we start from the security of the protocol, then we propose a novel theory for security protocol analysis of Denial of Service in order to deal with the DoS attack. We first introduce the conception of weighted graph to extend the strand space model, then we extend the penetrator model and define the goal of anti-DoS attack through the conception of the DoS-stop protocol, finally we propose two kinds of DoS test model and erect the novel formal theory for security protocol analysis of Denial of Service. Our new formal theory is applied in two example protocols. It is proved that the Internet key exchange （IKE） easily suffers from the DoS attacks, and the efficient DoS- resistant secure key exchange protocol （JFK） is resistant against DoS attack for the server, respectively.
基金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 under Grant Nos 61472048,61402058,61272511,61472046,61202082 and 61370194the Beijing Natural Science Foundation under Grant No 4152038the China Postdoctoral Science Foundation Funded Project under Grant No 2014M561826
文摘To analyze the security of two-step quantum direct communication protocol （QDCP） by using Einstein-Podolsky Rosen pair proposed by Deng et al. [Phys. Rev. A 68 （2003）042317] in collective-rotation noise channel, an excellent model of noise analysis is proposed. In the security analysis, the method of the entropy theory is introduced, and is compared with QDCP, an error rate point Qo（M ： （Q0, 1.0）） is given. In different noise levels, if Eve wants to obtain the same amount of information, the error rate Q is distinguishable. The larger the noise level ~ is, the larger the error rate Q is. When the noise level ~ is lower than 11%, the high error rate is 0.153 without eavesdropping. Lastly, the security of the proposed protocol is discussed. It turns out that the quantum channel will be safe when Q 〈 0.153. Similarly, if error rate Q〉 0.153 = Q0, eavesdropping information I 〉 1, which means that there exist eavesdroppers in the quantum channel, and the quantum channel will not be safe anymore.
基金National Natural Science Foundation of China (Grant Nos. 90412014 and 90604004)Jiangsu Provincial Key Laboratory of Network and Information Security (Grant No. BM2003201)Jiangsu Provincial High-Tech Research Program (Grant No. BG2004036)
文摘Security protocol is specified as the procedure of challenge-response, which uses applied cryptography to confirm the existence of other principals and fulfill some data negotiation such as session keys. Most of the existing analysis methods, which either adopt theorem proving techniques such as state exploration or logic reasoning techniques such as authentication logic, face the conflicts between analysis power and operability. To solve the problem, a new efficient method is proposed that provides SSM semantics-based definition of secrecy and authentication goals and applies authentication logic as fundamental analysis techniques, in which secrecy analysis is split into two parts： Explicit-lnformaUon-Leakage and Implicit-Information-Leakage, and correspondence analysis is concluded as the analysis of the existence relationship of Strands and the agreement of Strand pa- rameters. This new method owns both the power of the Strand Space Model and concision of authentication logic.
文摘This study developed a mail server program using Socket API and Python.The program uses the Hypertext Transfer Protocol(HTTP)to receive emails from browser clients and forward them to actual email service providers via the Simple Mail Transfer Protocol(SMTP).As a web server,it handles Transmission Control Protocol(TCP)connection requests from browsers,receives HTTP commands and email data,and temporarily stores the emails in a file.Simultaneously,as an SMTP client,the program establishes a TCP connection with the actual mail server,sends SMTP commands,and transmits the previously saved emails.In addition,we also analyzed security issues and the efficiency and availability of this server,providing insights into the design of SMTP mail servers.
基金Project supported by the National Natural Science Foundation of China(Nos.61902416 and 61902412)the Natural Science Foundation of Hunan Province,China(No.2019JJ50729)。
文摘Network protocol software is usually characterized by complicated functions and a vast state space.In this type of program,a massive number of stateful variables that are used to represent the evolution of the states and store some information about the sessions are prone to potentialflaws caused by violations of protocol specification requirements and program logic.Discovering such variables is significant in discovering and exploiting vulnerabilities in protocol software,and still needs massive manual verifications.In this paper,we propose a novel method that could automatically discover the use of stateful variables in network protocol software.The core idea is that a stateful variable features information of the communication entities and the software states,so it will exist in the form of a global or static variable during program execution.Based on recording and replaying a protocol program’s execution,varieties of variables in the life cycle can be tracked with the technique of dynamic instrument.We draw up some rules from multiple dimensions by taking full advantage of the existing vulnerability knowledge to determine whether the data stored in critical memory areas have stateful characteristics.We also implement a prototype system that can discover stateful variables automatically and then perform it on nine programs in Pro FuzzBench and two complex real-world software programs.With the help of available open-source code,the evaluation results show that the average true positive rate(TPR)can reach 82%and the average precision can be approximately up to 96%.
文摘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.
基金Supported by the National Natural Science Foundation of China (60473027)
文摘IEEE 802.16e, as an amendment and corrigendum to the IEEE 802.16-2004, published on 28 February 2006, and intended to update and expand IEEE 802.16-2004 to allow for mobile subscriber stations. This paper summarizes the key management protocol belonging to security part of the IEEE 802.16e, which includes security negotiation, authorization, key derivation, handshake, and key transportation. While these building blocks are well designed, we point out some unwelcome features for these building blocks. We also give out suggestions to diminish the proposed problems.
基金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.
