Using coloured petri nets to simulate DoS-resistant protocols

In this work, we examine unbalanced computation between an initiator and a responder that leads to resource exhaustion attacks in key exchange protocols. We construct models for two cryp-tographic protocols; one is the well-known Internet protocol named Secure Socket Layer (SSL) protocol, and the other one is the Host Identity Protocol (HIP) which has built-in DoS-resistant mechanisms. To examine such protocols, we develop a formal framework based on Timed Coloured Petri Nets (Timed CPNs) and use a simulation approach provided in CPN Tools to achieve a formal analysis. By adopting the key idea of Meadows' cost-based framework and re¯ning the de¯nition of operational costs during the protocol execution, our simulation provides an accurate cost estimate of protocol execution compar- ing among principals, as well as the percentage of successful connections from legitimate users, under four di®erent strategies of DoS attack.

An Efficient and Verifiable Solution to the Millionaire Problem

A new solution to the millionaire problem is designed on the base of two new techniques: zero test and batch equation. Zero test is a technique used to test whether one or more ciphertext contains a zero without revealing other information. Batch equation is a technique used to test equality of multiple integers. Combination of these two techniques produces the only known solution to the millionaire problem that is correct, private, publicly verifiable and efficient at the same time.

A Novel Range Test

In a range test, one party holds a ciphertext and needs to test whether the message encrypted in the ciphertext is within a certain interval range. In this paper, a range test protocol is proposed, where the party holding the ciphertext asks another party holding the private key of the encryption algorithm to help him. These two parties run the protocol to implement the test. The test returns TRUE if and only if the encrypted message is within the certain interval range. If the two parties do not conspire, no information about the encrypted message is revealed from the test except what can be deduced from the test result. Advantages of the new protocol over the existing related techniques are that it achieves correctness, soundness, °exibility, high e±ciency and privacy simultaneously.

Password Based Server Aided Key Exchange

We propose a new password-based 3-party protocol with a formal security proof in the standard model. Under reasonable assumptions we show that our new protocol is more efficient than the recent protocol of Abdalla and Pointcheval (FC 2005), proven in the random oracle model. We also observe some limitations in the model due to Abdalla, Fouque and Pointcheval (PKC 2005) for proving security of such protocols.

Modelling Denial of Service Attacks on JFK with Meadow's Cost-Based Framework

We present the first detailed application of Meadows’s cost-based modelling framework to the analysis of JFK, an Internet key agreement protocol. The analysis identifies two denial of service attacks against the protocol that are possible when an attacker is willing to reveal the source IP address. The first attack was identified through direct application of a cost-based modelling framework, while the second was only identified after considering coordinated attackers. Finally, we demonstrate how the inclusion of client puzzles in the protocol can improve denial of service resistance against both identified attacks.