110 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
A comparison of three authentication properties
No full textAuthentication is a slippery security property that has been formally defined only recently; among the recent definitions, two rather interesting ones have been proposed for the spi-calculus by (Abadi and Gordon (in: Proc. CONCUR’97, Lecture Notes in Computer Science, Vol. 1243, Springer, Berlin, 1997, pp. 59–73; Inform. and Comput. 148(1) (1999) 1–70) and for CSP by Lowe (in: Proc. 10th Computer Security Foundation Workshop, IEEE Press, 1997, pp. 31–43). On the other hand, in a recent paper (in: Proc. World Congr. on Formal Methods (FM’99), Lecture Notes in Computer Science, Vol. 1708, Springer, Berlin, 1999, pp. 794–813), we have proved that many existing security properties can be seen uniformly as specific instances of a general scheme based on the idea of non-interference. The purpose of this paper is to show that, under reasonable assumptions, spi-authentication can be recast in this general framework as well, by showing that it is equivalent to the non-interference property called NDC of Focardi and Gorrieri (J. Comput. Security 3(1) (1994/1995) 5–33; IEEE Trans. Software Eng. 23(9) (199) 550–571). This allows for the comparison between such aproperty and the one based on CSP, which was already recast under the general scheme of Focardi and Martinelli (1999)
Performance Preorder and Competitive Equivalence
No full textS. All local authors can be reached via e-mail at the address [email protected]. Written requests and comments should be addressed to [email protected]. UBLCS Technical Report Series 93-20 An Information Flow Security Property for CCS, R. Focardi, R. Gorrieri, October 1993. 93-21 A Classification of Security Properties, R. Focardi, R. Gorrieri, October 1993. 93-22 Real Time Systems: A Tutorial, F. Panzieri, R. Davoli, October 1993. 93-23 A Scalable Architecture for Reliable Distributed Multimedia Applications, F. Panzieri, M. Roccetti, October 1993. 93-24 Wide-Area Distribution Issues in Hypertext Systems, C. Maioli, S. Sola, F. Vitali, October 1993. 93-25 On Relating Some Models for Concurrency, P. Degano, R. Gorrieri, S. Vigna, October 1993. 93-26 Axiomatising ST Bisimulation Equivalence, N. Busi, R. van Glabbeek, R. Gorrieri, December 1993. 93-27 A Theory of Processes with Durational Actions, R. Gorrieri, M. Roccetti, E. Stancampiano, December 1993. 94-1 Further Modificati..
Performance Preorder and Competitive Equivalence
No full textA preorder based on execution speed, called performance preorder, is introduced for a simple process algebra with durational actions. Two processes E and F are related -E (Square image of or equal to)p F-if they have the same functionality (in this case, we have chosen strong bisimulation equivalence) and E is at least as fast as F. Hence, this preorder supports the stepwise refinement "from specification to implementation" by increasing efficiency while retaining the same functionality. We show that the problem of finding faster implementations for a specification is connected to the problem of finding more distributed implementations of the same specification. Both performance preorder and the induced equivalence, called competitive equivalence, are provided with sound and complete axiomatizations for finite agents
Deciding and Axiomatizing ST Bisimulation for a Process Algebra with Recursion and Action Refinement
No full textS. All local authors can be reached via e-mail at the address [email protected]. Questions and comments should be addressed to [email protected]. Recent Titles from the UBLCS Technical Report Series 96-12 A Logic Coordination Language Based on the Chemical Metaphor, P. Ciancarini, D. Fogli, M. Gaspari, July 1996. 96-13 Towards Parallelization of Concurrent Systems, F. Corradini, R. Gorrieri, D. Marchignoli, August 1996 (Revised December 1996). 96-14 The Compositional Security Checker: A Tool for the Verification of Information Flow Security Properties, R. Focardi, R. Gorrieri, August 1996. 96-15 Jada: a Coordination Toolkit for Java, P. Ciancarini, D. Rossi, October 1996. 96-16 Fault Tolerance through View Synchrony in Partitionable Asynchronous Distributed Systems, A. Montresor, December 1996. 96-17 A Tutorial on EMPA: A Theory of Concurrent Processes with Nondeterminism, Priorities, Probabilities and Time, M. Bernardo, R. Gorrieri, December 1996 (Revised January 1997). 97-1 ..
A Theory of Processes with Durational Actions
No full texts 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-15 Data Algorithm: A Numerical Method to Extract Shape Information from Gray Scale Images, R. Davoli, F. Tamburini, June 1993. 93-16 Towards Performance Evaluation in Process Algebras, R. Gorrieri, M. Roccetti, July 1993. 93-17 Split and ST Bisimulation Semantics, R. Gorrieri, C. Laneve, July 1993. 93-18 Multilanguage Interoperability, G. Attardi, M. Gaspari, July 1993. 93-19 HERMES: an Expert System for the Prognosis of Hepatic Diseases, I. Bonf a, C. Maioli, F. Sarti, G.L. Milandri, P.R. Dal Monte, September 1993. 93-20 An Information Flow Security Property for CCS, R. Focardi, R. Gorrieri, October 1993. 93-21 A Classification of Security Properties, R. Focardi, R. Gorrieri, October 1993. 93-22 Real Time Systems: A Tutorial, F. Panzieri, R. Davoli, October 1993. 93-..
Syntax and Semantics of Petri Nets
No full textPetri nets are one of the most popular tools for modelling distributed systems. This book provides a modern look at the theory behind them, by studying three classes of nets that model (i) sequential systems, (ii) non-communicating parallel systems, and (iii) communicating parallel systems.
A suitable behavioural equivalence is presented for each class, followed by a modal logic characterization for each equivalence. The author then introduces a suitable process algebra for the corresponding class of nets and proves that the behavioral equivalence proposed for each class is a congruence for the operator of the corresponding process algebra. Finally, an axiomatization of the behavioral congruence is proposed.
The theory is introduced step-by-step, with ordinary-language explanations and examples provided throughout, to remain accessible to readers without specialized training in concurrency theory or formal logic. Exercises with solutions solidify the reader’s understanding, and the final chapter hints at possible extensions of the theory
SLC26A9 as a Potential Modifier and Therapeutic Target in Cystic Fibrosis Lung Disease
No full textSLC26A9 belongs to the solute carrier family 26 (SLC26), which comprises membrane proteins involved in ion transport mechanisms. On the basis of different preliminary findings, including the phenotype of SlC26A9-deficient mice and its possible role as a gene modifier of the human phenotype and treatment response, SLC26A9 has emerged as one of the most interesting alternative targets for the treatment of cystic fibrosis (CF). However, despite relevant clues, some open issues and controversies remain. The lack of specific pharmacological modulators, the elusive expression reported in the airways, and its complex relationships with CFTR and the CF phenotype prevent us from conclusively understanding the contribution of SLC26A9 in human lung physiology and its real potential as a therapeutic target in CF. In this review, we summarized the various studies dealing with SLC26A9 expression, molecular structure, and function as an anion channel or transporter; its interaction and functional relationships with CFTR; and its role as a gene modifier and tried to reconcile them in order to highlight the current understanding and the gap in knowledge regarding the contribution of SLC26A9 to human lung physiology and CF disease and treatment
- …
