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.展开更多
Specification language is used to provide enough information for the model of the cryptographic protocol. This paper first extends strand space model to dynamic strand model, and then a formal specification language f...Specification language is used to provide enough information for the model of the cryptographic protocol. This paper first extends strand space model to dynamic strand model, and then a formal specification language for this model is defined by using BNF grammar. Compared with those in literatures, it is simpler because of only concerning the algebraic properties of cryptographic protocols.展开更多
In this paper, we show how to use the novel extended strand space method to verify Kerberos V. First, we formally model novel semantical features in Kerberos V such as timestamps and protocol mixture in this new frame...In this paper, we show how to use the novel extended strand space method to verify Kerberos V. First, we formally model novel semantical features in Kerberos V such as timestamps and protocol mixture in this new framework. Second, we apply unsolicited authentication test to prove its secrecy and authentication goals of Kerberos V. Our formalization and proof in this case study have been mechanized using Isabelle/HOL.展开更多
In this paper, we present two extensions of the strand space method to model Kerberos V. First, we include time and timestamps to model security protocols with timestamps: we relate a key to a crack time and combine i...In this paper, we present two extensions of the strand space method to model Kerberos V. First, we include time and timestamps to model security protocols with timestamps: we relate a key to a crack time and combine it with timestamps in order to define a notion of recency. Therefore, we can check replay attacks in this new framework. Second, we extend the classic strand space theory to model protocol mixture. The main idea is to introduce a new relation to model the causal relation between one primary protocol session and one of its following secondary protocol session. Accordingly, we also extend the definition of unsolicited authentication test.展开更多
基金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.
文摘Specification language is used to provide enough information for the model of the cryptographic protocol. This paper first extends strand space model to dynamic strand model, and then a formal specification language for this model is defined by using BNF grammar. Compared with those in literatures, it is simpler because of only concerning the algebraic properties of cryptographic protocols.
文摘In this paper, we show how to use the novel extended strand space method to verify Kerberos V. First, we formally model novel semantical features in Kerberos V such as timestamps and protocol mixture in this new framework. Second, we apply unsolicited authentication test to prove its secrecy and authentication goals of Kerberos V. Our formalization and proof in this case study have been mechanized using Isabelle/HOL.
文摘In this paper, we present two extensions of the strand space method to model Kerberos V. First, we include time and timestamps to model security protocols with timestamps: we relate a key to a crack time and combine it with timestamps in order to define a notion of recency. Therefore, we can check replay attacks in this new framework. Second, we extend the classic strand space theory to model protocol mixture. The main idea is to introduce a new relation to model the causal relation between one primary protocol session and one of its following secondary protocol session. Accordingly, we also extend the definition of unsolicited authentication test.
