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.

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.

Business process management as the 'killer app' for Petri nets

Since their inception in 1962, Petri nets have been used in a wide variety of application domains. Although Petri nets are graphical and easy to understand, they have formal semantics and allow for analysis techniques ranging from model checking and structural analysis to process mining and performance analysis. Over time Petri nets emerged as a solid foundation for Business Process Management (BPM) research. The BPM discipline develops methods, techniques, and tools to support the design, enactment, management, and analysis of operational business processes. Mainstream business process modeling notations and workflow management systems are using token-based semantics borrowed from Petri nets. Moreover, state-of-the-art BPM analysis techniques are using Petri nets as an internal representation. Users of BPM methods and tools are often not aware of this. This paper aims to unveil the seminal role of Petri nets in BPM.

Performance modelling of a fault-tolerant real-time multiprocessor using stochastic Petri nets

The fault-tolerant multiprocessor (ftmp) is a bus-based multiprocessor architecture with real-time and fault- tolerance features and is used in critical aerospace applications. A preliminary performance evaluation is of crucial importance in the design of such systems. In this paper, we review stochastic Petri nets (spn) and developspn-based performance models forftmp. These performance models enable efficient computation of important performance measures such as processing power, bus contention, bus utilization, and waiting times.

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.

Graphical simulation of Petri Nets

An interactive graphics package for modeling with Petri Nets has been implemented. It uses the VT-11 graphics terminal supported on the PDP-11/35 computer to draw, execute, analyze, edit and redraw a Petri Net. Each of the above mentioned tasks can be performed by selecting appropriate items from a menu displayed on the screen. Petri Nets with a reasonably large number of nodes can be created and analyzed using this package. The number of nodes supported may be increased by making simple changes in the program. Being interactive, the program seeks information from the user after displaying appropriate messages on the terminal. After completing the Petri Net, it may be executed step by step and the changes in the number of tokens may be observed on the screen, at each place. Some properties of Petri Nets like safety, boundedness, conservation and redundancy can be checked using this package. This package can be used very effectively for modeling asynchronous (concurrent) systems with Petri Nets and simulating the model by “graphical execution.”

A Petri net model for evaluating packet buffering strategies in a network processor

Previous studies have shown that buffering packets in DRAM is a performance bottleneck. In order to understand the impediments in accessing the DRAM, we developed a detailed Petri net model of IP forwarding application on IXP2400 that models the different levels of the memory hierarchy. The cell based interface used to receive and transmit packets in a network processor leads to some small size DRAM accesses. Such narrow accesses to the DRAM expose the bank access latency, reducing the bandwidth that can be realized. With real traces up to 30% of the accesses are smaller than the cell size, resulting in 7.7% reduction in DRAM bandwidth. To overcome this problem, we propose buffering these small chunks of data in the on chip scratchpad memory. This scheme also exploits greater degree of parallelism between different levels of the memory hierarchy. Using real traces from the internet, we show that the transmit rate can be improved by an average of 21% over the base scheme without the use of additional hardware. Further, the impact of different traffic patterns on the network processor resources is studied. Under real traffic conditions, we show that the data bus which connects the off-chip packet buffer to the micro-engines, is the obstacle in achieving higher throughput.

Invariant-preserving Petri net reduction and conditions for invariant-existence

The use of invariants is an important tool for analysis of distributed and concurrent systems modeled by Petri nets. For a large practical system, the computation of desired invariants by the existing techniques is a time-consuming task. This paper proposes a theoretical foundation for simplified computation of desired invariants. We provide invariant-preserving Petri net reduction rules followed by the conditions for the existence of invariants in various well-structured nets. If an invariant exists, it can be found directly from the net structure using the formulas derived, or by applying the existing techniques on the reduced net.

Extended colored Petri net: An efficient tool for analyzing concurrent systems

This paper proposes a novel and simple definition of general colored Petri nets. This definition is coherent with that of (uncolored) Petri nets, preserves the reflexivity of the original net and is extended to represent inhibitors. Also suggested are systematic and formal merging rules to obtain a well-formed structure of the extended colored Petri net by folding a given uncolored net. Finally, we present a technique to compute colored invariants by selecting colored RP-subnets. On the average, the proposed technique performs better than the existing ones. The analysis procedure is explained through an illustrative example of a three-level interrupt-priority-handler scheme.

A new methodology for analyzing distributed systems modeled by petri nets

Distributed computing systems can be modeled adequately by Petri nets. The computation of invariants of Petri nets becomes necessary for proving the properties of modeled systems. This paper presents a two-phase, bottom-up approach for invariant computation and analysis of Petri nets. In the first phase, a newly defined subnet, called the RP-subnet, with an invariant is chosen. In the second phase, the selected RP-subnet is analyzed. Our methodology is illustrated with two examples viz., the dining philosophers' problem and the connection-disconnection phase of a transport protocol. We believe that this new method, which is computationally no worse than the existing techniques, would simplify the analysis of many practical distributed systems.

S-nets: A Petri net based model for performance evaluation of real-time scheduling algorithms

A new class of nets, called S-nets, is introduced for the performance analysis of scheduling algorithms used in real-time systems Deterministic timed Petri nets do not adequately model the scheduling of resources encountered in real-time systems, and need to be augmented with resource places and signal places, and a scheduler block, to facilitate the modeling of scheduling algorithms. The tokens are colored, and the transition firing rules are suitably modified. Further, the concept of transition folding is used, to get intuitively simple models of multiframe real-time systems. Two generic performance measures, called �load index� and �balance index,� which characterize the resource utilization and the uniformity of workload distribution, respectively, are defined. The utility of S-nets for evaluating heuristic-based scheduling schemes is illustrated by considering three heuristics for real-time scheduling. S-nets are useful in tuning the hardware configuration and the underlying scheduling policy, so that the system utilization is maximized, and the workload distribution among the computing resources is balanced.

Petri net-based modeling of a class of complex digital systems

We present through the use of Petri Nets, modeling techniques for digital systems realizable using FPGAs. These Petri Net models are used for logic validation at the logic design phase. The technique is illustrated by modeling practical circuits. Further, the utility of the technique with respect to timing analysis of the modeled digital systems is considered. Copyright (C) 1997 Elsevier Science Ltd