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.

Networks cities and ecological habitats

As the world’s rural populations continue to migrate from farmland to sprawling cities, transport networks form an impenetrable maze within which monocultures of urban form erupt from the spaces in‐between. These urban monocultures are as problematic to human activity in cities as cropping monocultures are to ecosystems in regional landscapes. In China, the speed of urbanisation is exacerbating the production of mono‐functional private and public spaces. Edges are tightly controlled. Barriers and management practices at these boundaries are discouraging the formation of new synergistic relationships, critical in the long‐term stability of ecosystems that host urban habitats. Some urban planners, engineers, urban designers, architects and landscape architects have recognised these shortcomings in contemporary Chinese cities. The ideology of sustainability, while critically debated, is bringing together thinking people in these and other professions under the umbrella of an ecological ethic. This essay aims to apply landscape ecology theory, a conceptual framework used by many professionals involved in land development processes, to a concept being developed by BAU International called Networks Cities: a city with its various land uses arranged in nets of continuity, adjacency, and superposition. It will consider six lesser‐known concepts in relation to creating enhanced human activity along (un)structured edges between proposed nets and suggest new frontiers that might be challenged in an eco‐city. Ecological theory suggests that sustaining biodiversity in regions and landscapes depends on habitat distribution patterns. Flora and fauna biologists have long studied edge habitats and have been confounded by the paradox that maximising the breadth of edges is detrimental to specialist species but favourable to generalist species. Generalist species of plants and animals tolerate frequent change in the landscape, frequenting two or more habitats for their survival. Specialist species are less tolerant of change, having specific habitat requirements during their life cycle. Protecting species richness then may be at odds with increasing mixed habitats or mixed‐use zones that are dynamic places where diverse activities occur. Forman (1995) in his book Land Mosaics however argues that these two objectives of land use management are entirely compatible. He postulates that an edge may be comprised of many small patches, corridors or convoluting boundaries of large patches. Many ecocentrists now consider humans to be just another species inhabiting the ecological environments of our cities. Hence habitat distribution theory may be useful in planning and designing better human habitats in a rapidly urbanising context like China. In less‐constructed environments, boundaries and edges provide important opportunities for the movement of multi‐habitat species into, along and from adjacent land use areas. For instance, invasive plants may escape into a national park from domestic gardens while wildlife may forage on garden plants in adjoining residential areas. It is at these interfaces that human interactions too flow backward and forward between land types. Spray applications of substances by farmers on cropland may disturb neighbouring homeowners while suburban residents may help themselves to farm produce on neighbouring orchards. Edge environments are some of the most dynamic and contested spaces in the landscape. Since most of us require access to at least two or three habitats diurnally, weekly, monthly or seasonally, their proximity to each other becomes critical in our attempts to improve the sustainability of our cities.

Soundness of workflow nets with reset arcs

Petri nets are often used to model and analyze workflows. Many workflow languages have been mapped onto Petri nets in order to provide formal semantics or to verify correctness properties. Typically, the so-called Workflow nets are used to model and analyze workflows and variants of the classical soundness property are used as a correctness notion. Since many workflow languages have cancelation features, a mapping to workflow nets is not always possible. Therefore, it is interesting to consider workflow nets with reset arcs. Unfortunately, soundness is undecidable for workflow nets with reset arcs. In this paper, we provide a proof and insights into the theoretical limits of workflow verification.

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.

The biconnected verification of workflow nets

Formal representations of business processes are used for analysis of the process behavior. Workflow nets are a widely used formalism for describing the behavior of business processes. Structure theory of processes investigates the relation between the structure of a model and its behavior. In this paper, we propose to employ the connectivity property of workflow nets as an angle to their structural analysis. In particular, we show how soundness verification can be organized using biconnected components of a workflow net. This allows for efficient identification and localization of flaws in the behavior of workflow nets and for supporting process analysts with diagnostic information

newYAWL : Towards Workflow 2.0

The field of workflow technology has burgeoned in recent years providing a variety of means of automating business processes. It is a great source of opportunity for organisations seeking to streamline and optimise their operations. Despite these advantages however, the current generation of workflow technologies are subject to a variety of criticisms, in terms of their restricted view of what comprises a business process, their imprecise definition and their general inflexibility. As a remedy to these potential difficulties, in this paper we propose a series of development goals for the next generation of workflow technology. We also present newYAWL, a formally defined, multi-perspective reference language for workflow systems.

Privacy compliance verification in cryptographic protocols

To provide privacy protection, cryptographic primitives are frequently applied to communication protocols in an open environment (e.g. the Internet). We call these protocols privacy enhancing protocols (PEPs) which constitute a class of cryptographic protocols. Proof of the security properties, in terms of the privacy compliance, of PEPs is desirable before they can be deployed. However, the traditional provable security approach, though well-established for proving the security of cryptographic primitives, is not applicable to PEPs. We apply the formal language of Coloured Petri Nets (CPNs) to construct an executable specification of a representative PEP, namely the Private Information Escrow Bound to Multiple Conditions Protocol (PIEMCP). Formal semantics of the CPN specification allow us to reason about various privacy properties of PIEMCP using state space analysis techniques. This investigation provides insights into the modelling and analysis of PEPs in general, and demonstrates the benefit of applying a CPN-based formal approach to the privacy compliance verification of PEPs.

Conformance checking of service behavior

A service-oriented system is composed of independent software units, namely services, that interact with one another exclusively through message exchanges. The proper functioning of such system depends on whether or not each individual service behaves as the other services expect it to behave. Since services may be developed and operated independently, it is unrealistic to assume that this is always the case. This article addresses the problem of checking and quantifying how much the actual behavior of a service, as recorded in message logs, conforms to the expected behavior as specified in a process model.We consider the case where the expected behavior is defined using the BPEL industry standard (Business Process Execution Language for Web Services). BPEL process definitions are translated into Petri nets and Petri net-based conformance checking techniques are applied to derive two complementary indicators of conformance: fitness and appropriateness. The approach has been implemented in a toolset for business process analysis and mining, namely ProM, and has been tested in an environment comprising multiple Oracle BPEL servers.

Workflow patterns put into context

In his paper “Approaches to Modeling Business Processes. A Critical Analysis of BPMN, Workflow Patterns and YAWL”, Egon Börger criticizes the work of the Workflow Patterns Initiative in a rather provocative manner. Although the workflow patterns and YAWL are well established and frequently used, Börger seems to misunderstand the goals and contributions of the Workflow Patterns Initiative. Therefore, we put the workflow patterns and YAWL in their historic context. Moreover, we address some of the criticism of Börger by pointing out the real purpose of the workflow patterns and their relationship to formal languages (Petri nets) and real-life WFM/BPM systems.

The 4C spectrum of fundamental behavioral relations for concurrent systems

The design of concurrent software systems, in particular process-aware information systems, involves behavioral modeling at various stages. Recently, approaches to behavioral analysis of such systems have been based on declarative abstractions defined as sets of behavioral relations. However, these relations are typically defined in an ad-hoc manner. In this paper, we address the lack of a systematic exploration of the fundamental relations that can be used to capture the behavior of concurrent systems, i.e., co-occurrence, conflict, causality, and concurrency. Besides the definition of the spectrum of behavioral relations, which we refer to as the 4C spectrum, we also show that our relations give rise to implication lattices. We further provide operationalizations of the proposed relations, starting by proposing techniques for computing relations in unlabeled systems, which are then lifted to become applicable in the context of labeled systems, i.e., systems in which state transitions have semantic annotations. Finally, we report on experimental results on efficiency of the proposed computations.

Task constraints

Newell (1985, 1986) identified the importance of interacting constraints on the emergent behaviours of learners or performers in sport as they assemble functional states of movement organisation in achieving task goals. Constraints, related to the person, task and environment, were defined as ‘boundaries or features that limit motion of the entity under consideration at any moment in time’ (Newell, 1986, p.347). Personal (or organismic) constraints include factors such as individual anthropometrics (height, weight, and limb lengths), fitness (e.g., strength, speed, aerobic capacity, and flexibility), mental skills (e.g. concentration, confidence, emotional control and motivation), perceptual and decisionmaking skills (e.g., recognising patterns of play, anticipation by reading the movements of opponents) and personality factors (e.g., risk taking or conservative behaviours). Newell (1986, p.350) distinguished between general environmental constraints, such as gravity, ambient temperature, natural light and altitude and task constraints, which are task specific and concerned with the goals of a specific activity. More recently, socio-cultural constraints (e.g., family support, cultural expectations and access to facilities) have also been considered as environmental constraints. Application of the constraints framework to the study of sport performance has led to task constraints being defined to include factors such as rules of games, equipment used, boundary playing areas and markings, nets and goals, the number of...

Interrupting malaria transmission: quantifying the impact of interventions in regions of low to moderate transmission

Malaria has been eliminated from over 40 countries with an additional 39 currently planning for, or committed to, elimination. Information on the likely impact of available interventions, and the required time, is urgently needed to help plan resource allocation. Mathematical modelling has been used to investigate the impact of various interventions; the strength of the conclusions is boosted when several models with differing formulation produce similar data. Here we predict by using an individual-based stochastic simulation model of seasonal Plasmodium falciparum transmission that transmission can be interrupted and parasite reintroductions controlled in villages of 1,000 individuals where the entomological inoculation rate is <7 infectious bites per person per year using chemotherapy and bed net strategies. Above this transmission intensity bed nets and symptomatic treatment alone were not sufficient to interrupt transmission and control the importation of malaria for at least 150 days. Our model results suggest that 1) stochastic events impact the likelihood of successfully interrupting transmission with large variability in the times required, 2) the relative reduction in morbidity caused by the interventions were age-group specific, changing over time, and 3) the post-intervention changes in morbidity were larger than the corresponding impact on transmission. These results generally agree with the conclusions from previously published models. However the model also predicted changes in parasite population structure as a result of improved treatment of symptomatic individuals; the survival probability of introduced parasites reduced leading to an increase in the prevalence of sub-patent infections in semi-immune individuals. This novel finding requires further investigation in the field because, if confirmed, such a change would have a negative impact on attempts to eliminate the disease from areas of moderate transmission.

Soundness of workflow nets: classification, decidability, and analysis

Workflow nets, a particular class of Petri nets, have become one of the standard ways to model and analyze workflows. Typically, they are used as an abstraction of the workflow that is used to check the so-called soundness property. This property guarantees the absence of livelocks, deadlocks, and other anomalies that can be detected without domain knowledge. Several authors have proposed alternative notions of soundness and have suggested to use more expressive languages, e.g., models with cancellations or priorities. This paper provides an overview of the different notions of soundness and investigates these in the presence of different extensions of workflow nets.We will show that the eight soundness notions described in the literature are decidable for workflow nets. However, most extensions will make all of these notions undecidable. These new results show the theoretical limits of workflow verification. Moreover, we discuss some of the analysis approaches described in the literature.