We prove that the well-known (strong) fully-concurrent bisimilarity and the novel i-causal-net bisimilarity, which is a sligtlhy coarser variant of causal-net bisimilarity, are decidable for finite bounded Petri nets. The proofs are based on a generalization of the ordered marking proof technique that Vogler used to demonstrate that (strong) fully-concurrent bisimilarity (or, equivalently, history-preserving bisimilarity) is decidable on finite safe nets.

Place/Transition Petri nets with inhibitor arcs (PTI nets for short), which are a well-known Turing-complete, distributed model of computation, are equipped with a decidable, behavioral equivalence, called pti-place bisimilarity, that conservatively extends place bisimilarity defined over Place/Transition nets (without inhibitor arcs). We prove that pti-place bisimilarity is sensible, as it respects the causal semantics of PTI nets.

BPP nets, a subclass of finite Place/Transition Petri nets, are equipped with some causal behavioral semantics, which are variations of fully-concurrent bisimilarity [3], inspired by weak [28] or branching bisimulation [12] on labeled transition systems. Then, we introduce novel, efficiently decidable, distributed semantics, inspired by team bisimulation [17] and h-team bisimulation [19], and show how they relate to these variants of fully-concurrent bisimulation.

CCS(h,k) is the CCS subcalculus which can use at most h constants and k actions. We show that CCS(25,12) is Turing-complete by simulating Neary and Woods’ universal Turing machine with 15 states and 2 symbols.

A 2 CCS is a conservative extension of CCS, enriched with an operator of strong prefixing, enabling the modeling of atomic sequences and multi-party synchronization (realized as an atomic sequence of binary synchronizations); the classic dining philosophers problem is used to illustrate the approach. A step semantics for A 2 CCS is also presented directly as a labeled transition system. A safe Petri net semantics for this language is presented, following the approach of Degano, De Nicola, Montanari and Olderog. We prove that a process p and its associated net Net(p) are interleaving bisimilar (Theorem 5.1). Moreover, to support the claim that the intended concurrency is well-represented in the net, we also prove that a process p and its associated net Net(p) are step bisimilar (Theorem 5.2).

Several notions of non-interference have been proposed in the literature for studying the problem of confidentiality in concurrent systems. The common feature of these non-interference properties is that they are all defined as extensional properties based on some notion of behavioural equivalence on systems. Here, instead, we address the problem of defining non-interference by looking at the structure of the systems under investigation. We use a simple class of Petri nets, namely, contact-free elementary net systems, as the system model and define structural non-interference properties based on the absence of particular places in the net: such places show that a suitable causality or conflict relation is present between a high-level transition and a low-level one. We characterise one structural property, called PBNI+, which we show to be equivalent to the well-known behavioural property SBNDC. It essentially captures all the positive information flows (that is, a low-level user can deduce that some high-level action has occurred). We start by providing a characterisation of PBNI+ on contact-free elementary net systems, then extend the definition to cope with the richer class of trace nets.

Priority is a frequently used feature of many computational systems. In this paper we study the expressiveness of two process algebras enriched with different priority mechanisms. In particular, we consider a finite (that is, recursion-free) fragment of asynchronous CCS with global priority (FAP, for short) and Phillips' CPG (CCS with local priority), and contrast their expressive power with that of two non-prioritised calculi, namely the π-calculus and its broadcast-based version, called bπ. We prove, by means of leader-election-based separation results, that, under certain conditions, there exists no encoding of FAP in π-Calculus or CPG. Moreover, we single out another problem in distributed computing, which we call thelast man standingproblem (LMS for short), that better reveals the gap between the two prioritised calculi above and the two non-prioritised ones, by proving that there exists no parallel-preserving encoding of the prioritised calculi in the non-prioritised calculi retaining anysincere(complete but partially correct, that is, admitting divergence or premature termination) semantics.

The spreading of multicast technology enables the development of group communication and so dealing with digital streams becomes more and more common over the Internet. Given the flourishing of security threats, the distribution of streamed data must be equipped with sufficient security guarantees. To this aim, some architectures have been proposed, to supply the distribution of the stream with guarantees of, e.g. , authenticity, integrity, and confidentiality of the digital contents. This paper shows a formal capability of capturing some features of secure multicast protocols. In particular, both the modeling and the analysis of some case studies are shown, starting from basic schemes for signing digital streams, passing through protocols dealing with packet loss and time-synchronization requirements, concluding with a secure distribution of a secret key. A process-algebraic framework will be exploited, equipped with schemata for analysing security properties and compositional principles for evaluating if a property is satisfied over a system with more than two components.

Java is the most popular language for web programming. However it suffers from some well-known denial-of-service attacks (e.g., obscuring the screen) due to the execution of malicious code that uses resources in an improper way. In this paper we present a new approach to alleviate these problems by patching the Java Virtual Machine, in order to force the needed checks on resources usage bounds directly at the level of the source code.

We define several security properties for the analysis of probabilistic noninterference as a conservative extension of a classical, nondeterministic, process-algebraic approach to information flow theory. We show that probabilistic covert channels (that are not observable in the nondeterministic setting) may be revealed through our approach and that probabilistic information can be exploited to give an estimate of the amount of confidential information flowing to unauthorized users. Finally, we present a case study showing that the expressiveness of the calculus we adopt makes it possible to model and analyze real concurrent systems.

In previous work, we studied some noninterference properties for information flow analysis in computer systems on classic (possibilistic) labeled transition systems. In this paper, some of these properties, notably bisimulation-based nondeducibility on compositions (BNDC), are reformulated in a real-time setting. This is done by first enhancing the security process algebra proposed by two of the authors with some extra constructs to model real-time systems (in a discrete time setting), and then by studying the natural extension of these properties in this enriched setting. We prove essentially the same results known for the untimed case: ordering relation among properties, compositionality aspects, partial model checking techniques. Finally, we illustrate the approach through two case studies, where in both cases the untimed specification is secure, while the timed specification may show up interesting timing covert channels.

Due to the complex nature of bisimulation equivalences that express some form of history dependence, it turned out to be problematic to decide them over nontrivial classes of recursive systems. Moreover, to the best of our knowledge, the problem of axiomatizing them over such classes of systems has never been solved. In this article, we face this problem in the case of weak ST bisimulation, an equivalence that expresses the execution of an action as the combination of the two interdependent events of action start and action termination and that supports the operation of action refinement. We first consider a basic process algebra with CSP multiway synchronization and recursion and we show that a simple technique based on static names is sufficient to decide weak ST bisimulation over processes that are finite state according to the standard interleaving semantics. Then we introduce a different technique based on dynamic names and on the new idea of compositional level-wise renaming of actions (which produces semantic models via SOS such that weak ST bisimulation can be established through standard weak bisimulation) and we show that it can be applied to decide and axiomatize weak ST bisimulation over the same class of processes. Finally, we introduce a third technique based on pointers, updated according to a pseudo-stack discipline, which preserves the possibility of deciding and axiomatizing weak ST bisimulation also when an action refinement operator is considered.

Some of the non-interference properties studied in (Focardi, 1998; Focardi and Gorrieri, 1995) for information flow analysis in computer systems, notably BNDC, are reformulated in a real-time setting. This is done by enhancing the Security Process Algebra of (Focardi and Gorrieri, 1997; Focardi and Martinelli, 1999) with some extra constructs to model real-time systems (in a discrete time setting); and then by studying the natural extensions of those properties in this enriched setting. We prove essentially the same results known for the untimed case: ordering relation among properties, compositionality aspects, partial model checking techniques. Finally, we illustrate a case study of a system that presents no information flows when analyzed without considering timing constraints. When the specification is refined with time, some interesting information flows are detected.

The Security Process Algebra (SPA) is a CCS-like specification languag e where actions belong to two different levels of confidentiality. It has been used to define several noninterference-like security properties whose verification has been automated by the tool CoSeC. In recent years, a method for analyzing security protocols using SPA and CoSeC has been developed. Even if it has been useful in analyzing small security protocols, this method has shown to be error-prone, as it requires the protocol description and its environment to be written by hand. This problem has been solved by defining a protocol specification language more abstract than SPA, called VSP, and a compiler CVS that automatically generates the SPA specification for a given protocol described in VSP. The VSP/CVS technology is very powerful, and its usefulness is shown with some case studies: the Woo-Lam one-way authentication protocol, for which a new attack to authentication is found, and the Wide Mouthed Frog protocol, where different kinds of attack are detected and analyzed.

The Security Process Algebra (SPA) is a CCS-like specification language where actions belong to two different levels of confidentiality. It has been used to define several non-interference-like security properties whose verification has been automatized by means of the tool CoSeC. In recent years, a method for analyzing security protocols using SPA and CoSeC has been developed. Even if it has been useful in analyzing small security protocols, this method has shown to be error-prone as it requires the description by hand of the protocol and of the environment in which it will execute. This problem has been solved by defining a protocol specification language more abstract than SPA, called VSP and a compiler CVS that generates in an automatic way the SPA specification for a given protocol described in VSP. The VSP/CVS technology is very powerful and its usefulness is shown with the case-study of the Woo-Lam one-way authentication protocol, for which an attack undocumented in the literature is found.

Abstract. A case study is presented which concerns the design of an adaptive mechanism for packetised audio for use over the Internet. During the design process, the audio mechanism was modelled with the stochastically timed process algebra EMPA and analysed via simulation by the EMPA based software tool TwoTowers in order to predict the percentage of packets that are received in time for being played out. The predicted performance figures obtained from the algebraic model illustrated in advance the adequacy of the approach adopted in the design of the audio playout delay control mechanism. Based on these performance figures, it was possible to implement and develop the complete mechanism without incurring additional costs due to the late discovery of unexpected errors or inefficiency. Performance results obtained from experiments conducted on the field confirmed the predictive simulative results.

The Compositional Security Checker (CoSeC for short) is a semantic-based tool for the automatic verification of some compositional information flow properties. The specifications given as inputs to CoSeC are terms of the Security Process Algebra, a language suited for the specification of concurrent systems where actions belong to two different levels of confidentiality. The information flow security properties which can be verified by CoSeC are some of those classified in (Focardi and Gorrieri, 1994). They are derived from some classic notions, e.g., noninterference. The tool is based on the same architecture as the Concurrency Workbench, from which some modules have been imported unchanged. The usefulness of the tool is tested with the significant case-study of an access-monitor, presented in several versions in order to illustrate the relative merits of the various information flow properties that CoSeC can check. Finally, we present an application in the area of network security: we show that the theory (and the tool) can be reasonably applied also for singling out security flaws in a simple, yet paradigmatic, communication protocol.

The security checker (SC for short) is a semantic tool for the automatic verification of some information flow properties. The specifications given as inputs to SC are terms of the security process algebra (SPA for short), a language suited for the specification of systems where actions belong to two different levels of confidentiality. The information flow security properties which can be verified by SC are some of those classified in previous papers. They are derivations of some classic notions, e.g. non interference. The tool is based on the same architecture of the concurrency workbench, from which some modules have been integrally imported. The usefulness of the tool is tested with the significative case-study of an access monitor.

Extended Markovian Process Algebra (EMPA) is a stochastic process algebra equipped with an interleaving semantics, a Markovian semantics and a net semantics. The main drawback of its net semantics is that is usually associates huge nets with EMPA terms. Here we propose a new net semantics, based on contextual nets, in order to obtain more compact net representations for EMPA terms.

Several information flow security definitions, proposed in the literature, are generalized and adapted to the model of labelled transition systems. This very general model has been widely used as a semantic domain for many process algebras, e.g. CCS.

Several information flow security definitions, proposed in the literature, are generalized and adapted to the model of labelled transition systems. This very general model has been widely used as a semantic domain for process algebras, such as Milner's CCS. As a by-product, we provide CCS with a set of security notions, hence relating these two areas of concurrency research. A classification of these generalised security definitions is presented, taking into account also some additional properties, such as input totality, which can influence this taxonomy. We also show that some of these security properties are composable w.r.t. the operators of parallellism and action restriction.>

In [As87] a correspondence between the subset of Linear Logic [Gi86] involving the conjunctive tensor product only and Place/Transition Petri Nets [Rei85] is established. In this correspondence, formulae are regarded as distributed states and provable sequents are computations in the net. Developing this idea, Martì-Oliet and Meseguer [MaM89] have suggested that all the other computations of Linear Logic, which do not have an immediate correspondence with Petri Nets, should be regarded as “gedanken” or idealized processes, providing a richer language for the specification and the study of properties of distributed computations. In this paper we apply this program to the fundamental connective of linear implication. We prove that the introduction of linear implication allows us to observe the net at a lower, more decentralized level of atomicity, where the preemption of each resource needed for the firing of a transition is represented as a separate move. We give a conservative theorem relating computations at different levels of abstraction. The categorical semantics establishes a tight correspondence among Petri nets, monoidal closed categories and tensor theories, reminiscent of the well known relation among functional languages, Cartesian closed categories and intuitionistic logic [LS86]. The identification of computations in the categorical model naturally suggests the generalisation of the notion of process [DMM89] at the lower level of atomicity.