1,721,124 research outputs found
Classification of Security Properties (Part II: Network Security)
No full textMany security properties of cryptographic protocols can be all formalized as specific instances of a general scheme, called Generalized Non Deducibility on Composition (GNDC). This scheme derives from the NDC property we proposed a few years ago for studying information flow in computer systems. The theory is formulated for CryptoSPA, a process algebra we introduced for the specification of cryptographic protocols. One of the advantages of our unifying GNDC-based theory is that that formal comparison among security properties become easier, being them all instances of a unique general property. Moreover, the full generality of the approach has helped us in finding a few undocumented attacks on cryptographic protocols.
This paper is based on the results of [20,22–25] and covers the second part of the course “Classification of Security Properties” given by Roberto Gorrieri and Riccardo Focardi at the FOSAD’00 and FOSAD’01 schools
Verification of finite-state machines: A distributed approach
No full textFinite-state machines, a simple class of finite Petri nets, are equipped with a truly concurrent, bisimulation-based, behavioral equivalence, called team equivalence, which conservatively extends classic bisimulation equivalence over labeled transition systems and which is checked in a distributed manner, without necessarily building a global model of the overall behavior. An associated distributed modal logic, called basic team modal logic(BTML, for short), is presented and shown to be coherent with team equivalence: two markings are team equivalent if and only if they satisfy the same BTML formulae
CCS(25,12) is Turing-complete
No full textCCS(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
Place Bisimilarity is Decidable, Indeed!
No full textPlace bisimilarity is a behavioral equivalence for finite Petri nets, proposed by Schnoebelen and co-workers in 1991. Differently from all the other behavioral relations proposed so far, a place bisimulation is not defined over the markings of a finite net, rather over its places, which are finitely many. However, place bisimilarity is not coinductive, as the union of place bisimulations may be not a place bisimulation. Place bisimilarity was claimed decidable in [1], even if the algorithm used to this aim [2] does not characterize this equivalence, rather the unique maximal place bisimulation which is also an equivalence relation; hence, its decidability was not proved. Here we show that it is possible to decide place bisimilarity with a simple, yet inefficient, algorithm, which essentially scans all the place relations (which are finitely many) to check whether they are place bisimulations. Moreover, we propose a slightly coarser variant, we call d-place bisimilarity, that we conjecture to be the coarsest equivalence, fully respecting causality and branching time, to be decidable on finite Petri nets
Team equivalences for finite-state machines with silent moves
Full text linkFinite-state machines, a simple class of finite Petri nets, were equipped in [16] with an efficiently decidable, truly-concurrent, bisimulation-based, behavioral equivalence, called team equivalence, which conservatively extends classic bisimulation equivalence on labeled transition systems and which is checked in a distributed manner. This paper addresses the problem of defining variants of this equivalence which are insensitive to silent moves. We define (rooted) weak team equivalence and (rooted) branching team equivalence as natural transposition to finite-state machines of Milner’s weak bisimilarity [25] and van Glabbeek and Weijland’s branching bisimilarity [12] on labeled transition systems. The process algebra CFM [15] is expressive enough to represent all and only the finite-state machines, up to net isomorphism. Here we first prove that the rooted versions of these equivalences are congruences for the operators of CFM, then we show some algebraic properties, and, finally, we provide finite, sound and complete, axiomatizations for the
Interleaving vs True Concurrency: Some Instructive Security Examples
No full textInformation flow security properties were defined some years ago in terms of suitable equivalence checking problems. These definitions were provided by using sequential models of computations (e.g., labeled transition systems [17, 26]), and interleaving behavioral equivalences (e.g., bisimulation equivalence [27]). More recently, the distributed model of Petri nets has been used to study non-interference in [1, 5, 6], but also in these papers an interleaving semantics was used. By exploiting a simple process algebra, called CFM [18] and equipped with a Petri net semantics, we provide some examples showing that team equivalence, a truly-concurrent behavioral equivalence proposed in [19, 20], is much more suitable to define information flow security properties. The distributed non-interference property we propose, called DNI, is very easily checkable on CFM processes, as it is compositional, so that it does not suffer from the state-space explosion problem. Moreover, DNI is characterized syntactically on CFM by means of a type system
A Study on Team Bisimulations for BPP nets
No full textBPP nets, a subclass of finite P/T nets, were equipped in [13] with an efficiently decidable, truly concurrent, behavioral equivalence, called team bisi-milarity. This equivalence is a very intuitive extension of classic bisimulation equivalence (over labeled transition systems) to BPP nets and it is checked in a distributed manner, without building a global model of the overall behavior of the marked BPP net. This paper has three goals. First, we provide BPP nets with various causality-based equivalences, notably a novel one, called causal-net bisimilarity, and (a version of) fully-concurrent bisimilarity [3]. Then, we define a variant equivalence, h-team bisimilarity, coarser than team bisimilarity. Then, we complete the study by comparing them with the causality-based semantics we have introduced: the main results are that team bisimilarity coincides with causal-net bisimilarity, while h-team bisimilarity with fully-concurrent bisimilarity
A Classification of Security Properties (Extended Abstract)
No full text) Riccardo Focardi Roberto Gorrieri Technical Report UBLCS-93-21 October 1993 Laboratory for Computer Science University of Bologna Piazza di Porta S. Donato, 5 40127 Bologna (Italy) The University of Bologna Laboratory for Computer Science Research Technical Reports are available via anonymous FTP from the area ftp.cs.unibo.it:/pub/TR/UBLCS in compressed PostScript format. Abstracts are available from the same host in the directory /pub/TR/UBLCS/ABSTRACTS in plain text format. All local authors can be reached via e-mail at the address [email protected]. UBLCS Technical Report Series 93-1 Consistent Global States of Distributed Systems: Fundamental Concepts and Mechanism, by O. Babao glu and K. Marzullo, January 1993. 93-2 Understanding Non-Blocking Atomic Commitment, by O. Babao glu and S. Toueg, January 1993. 93-3 Anchors and Paths in a Hypertext Publishing System, by C. Maioli and F. Vitali, February 1993. 93-4 A Formalization of Priority Inversion, by O. Babao glu, K. Marz..
Axiomatizing Team Equivalence for Finite-State Machines
No full textFinite-state machines, a simple class of finite Petri nets, were equipped in [11] with a truly concurrent, bisimulation-based, behavioral equivalence, called team equivalence, which conservatively extends bisimulation equivalence on labeled transition systems and which is checked in a distributed manner, without necessarily building a global model of the overall behavior. The process algebra CFM [10] is expressive enough to represent all and only the finite-state machines, up to net isomorphism. Here we first prove that this equivalence is a congruence for the operators of CFM, then we show some algebraic properties of team equivalence and, finally, we provide a finite, sound and complete, axiomatization for team equivalence over CFM
A Decidable Equivalence for a Turing-Complete, Distributed Model of Computation
Full text linkPlace/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
- …
