Using Coloured Petri Nets to Simulate DoS-resistant Protocols
Suratose Tritilanunt, Colin Boyd, Ernest Foo, Juan González Nieto · QUT ePrints (Queensland University of Technology) · 2006
Abstract. 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 refining the definition 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 different strategies of DoS attack. 1