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.

Designing a workflow system using coloured petri nets

Traditional workflow systems focus on providing support for the control-flow perspective of a business process, with other aspects such as data management and work distribution receiving markedly less attention. A guide to desirable workflow characteristics is provided by the well-known workflow patterns which are derived from a comprehensive survey of contemporary tools and modelling formalisms. In this paper we describe the approach taken to designing the newYAWL workflow system, an offering that aims to provide comprehensive support for the control-flow, data and resource perspectives based on the workflow patterns. The semantics of the newYAWL workflow language are based on Coloured Petri Nets thus facilitating the direct enactment and analysis of processes described in terms of newYAWL language constructs. As part of this discussion, we explain how the operational semantics for each of the language elements are embodied in the newYAWL system and indicate the facilities required to support them in an operational environment. We also review the experiences associated with developing a complete operational design for an offering of this scale using formal techniques.

Analysis of Object-Specific Authorization Protocol (OSAP) using coloured petri nets - Version 1.0

Analyzing security protocols is an ongoing research in the last years. Different types of tools are developed to make the analysis process more precise, fast and easy. These tools consider security protocols as black boxes that can not easily be composed. It is difficult or impossible to do a low-level analysis or combine different tools with each other using these tools. This research uses Coloured Petri Nets (CPN) to analyze OSAP trusted computing protocol. The OSAP protocol is modeled in different levels and it is analyzed using state space method. The produced model can be combined with other trusted computing protocols in future works.

Analysis of Object-Specific Authorization Protocol (OSAP) using coloured Petri nets

The use of Trusted Platform Module (TPM) is be- coming increasingly popular in many security sys- tems. To access objects protected by TPM (such as cryptographic keys), several cryptographic proto- cols, such as the Object Specific Authorization Pro- tocol (OSAP), can be used. Given the sensitivity and the importance of those objects protected by TPM, the security of this protocol is vital. Formal meth- ods allow a precise and complete analysis of crypto- graphic protocols such that their security properties can be asserted with high assurance. Unfortunately, formal verification of these protocols are limited, de- spite the abundance of formal tools that one can use. In this paper, we demonstrate the use of Coloured Petri Nets (CPN) - a type of formal technique, to formally model the OSAP. Using this model, we then verify the authentication property of this protocol us- ing the state space analysis technique. The results of analysis demonstrates that as reported by Chen and Ryan the authentication property of OSAP can be violated.

On the invariants of coloured Petri Nets

In this paper, we develop a theorem that enables computation of the place invariants of the union of a finite collection of coloured Petri Nets when the individual nets satisfy certain conditions and their invariants are known. We consider the illustrative examples of the Readers-Writers problem, a resource sharing system, and a network of databases and show how this theorem is a valuable tool in the analysis of concurrent systems.

Coloured Petri net models for automated manufacturing systems

In this paper, we propose an approach, using Coloured Petri Nets (CPN) for modelling flexible manufacturing systems. We illustrate our methodology for a Flexible Manufacturing Cell (FMC) with three machines and three robots. We also consider the analysis of the FMC for deadlocks using the invariant analysis of CPNs.

Controlling traffic jams on urban roads modeled in Coloured Petri net using Genetic Algorithm

This paper presents an application to traffic lights control in congested urban traffic, in real time, taking as input the position and route of the vehicles in the involved areas. This data is obtained from the communication between vehicles and infrastructure (V2I). Due to the great complexity of the possible combination of traffic lights and the short time to get a response, Genetic Algorithm was used to optimize this control. According to test results, the application can reduce the number of vehicles in congested areas, even with the entry of vehicles that previously were not being considered in these roads, such as parked vehicles. © 2012 IEEE.

Bottlenecks detection of track allocation schemes at rail stations by Petri nets

Robustness of the track allocation problem is rarely addressed in literatures and the obtained track allocation schemes (TAS) embody some bottlenecks. Therefore, an approach to detect bottlenecks is needed to support local optimization. First a TAS is transformed to an executable model by Petri nets. Then disturbances analysis is performed using the model and the indicators of the total trains' departure delays are collected to detect bottlenecks when each train suffers a disturbance. Finally, the results of the tests based on a rail hub linking six lines and a TAS about thirty minutes show that the minimum buffer time is 21 seconds and there are two bottlenecks where the buffer times are 57 and 44 seconds respectively, and it indicates that the bottlenecks do not certainly locate at the area where there is minimum buffer time. The proposed approach can further support selection of multi schemes and robustness optimization.

Petri net modeling of spatial and temporal constraints in track allocation problem at railway stations

The track allocation problem (TAP) at a multi-track, multi-platform mainline railway station is defined by the station track layout and service timetable, which implies combinations of spatial and temporal conflicts. Feasible solutions are available from either traditional planning or advanced intelligent searching methods and their evaluations with respect to operational requirements are essential for the operators. To facilitate thorough analysis, a timed Coloured Petri Nets (CPN) model is presented here to encapsulate the inter-relationships of the spatial and temporal constraints in the TAP.

Modeling resource management in the building design process by information constraint Petri nets

The effect of resource management on the building design process directly influences the development cycle time and success of construction projects. This paper presents the information constraint net (ICN) to represent the complex information constraint relations among design activities involved in the building design process. An algorithm is developed to transform the information constraints throughout the ICN into a Petri net model. A resource management model is developed using the ICN to simulate and optimize resource allocation in the design process. An example is provided to justify the proposed model through a simulation analysis of the CPN Tools platform in the detailed structural design. The result demonstrates that the proposed approach can obtain the resource management and optimization needed for shortening the development cycle and optimal allocation of resources.

Analysis of two authorization protocols using Colored Petri Nets

To prevent unauthorized access to protected trusted platform module (TPM) objects, authorization protocols, such as the object-specific authorization protocol (OSAP), have been introduced by the trusted computing group (TCG). By using OSAP, processes trying to gain access to the protected TPM objects need to prove their knowledge of relevant authorization data before access to the objects can be granted. Chen and Ryan’s 2009 analysis has demonstrated OSAP’s authentication vulnerability in sessions with shared authorization data. They also proposed the Session Key Authorization Protocol (SKAP) with fewer stages as an alternative to OSAP. Chen and Ryan’s analysis of SKAP using ProVerif proves the authentication property. The purpose of this paper was to examine the usefulness of Colored Petri Nets (CPN) and CPN Tools for security analysis. Using OSAP and SKAP as case studies, we construct intruder and authentication property models in CPN. CPN Tools is used to verify the authentication property using a Dolev–Yao-based model. Verification of the authentication property in both models using the state space tool produces results consistent with those of Chen and Ryan.