英语论文网

Abstract
Several information ow security de nitions, prop osed in the literature, aregeneralized and adapted to the mo del of lab elled transition systems.代写留学生论文 This verygeneral mo del has b een widely used as a semantic domain for many pro cess al-gebras, e.g. CCS. As a by-pro duct, we provide a pro cess algebra similar to CCSwith a set of security notions, hence relating these two areas of concurrencyresearch. A classi cation of these generalized security de nitions is presented,taking into account also the additional prop erty of input totality, which canin uence this taxonomy. We also show that some of these security prop ertiesare comp osable w.r.t. the op erators of parallelism and action restriction.

Introduction
In the literature, several possibilistic information ow security prop ertieshave b een prop osed 10, 17, 21, 25, 31, 32], in order to sp ecify what prop ertiesa multilevel system should satisfy to b e called secure. Unfortunately, mostof them are based on rather dissimilar abstract machines and following alsodi erent intuitions, hence making di cult a formal comparison.One feature, common to some of these prop erties, is the synchrony as-sumption 3, 32, 25]: a system is comp osed of several comp onents which haveto pro ceed together at every time instant. This assumption is incompatible with the idea of describing distributed systems, where the geographical dis-tance among the various comp onents prevents the existence of a commonglobal clo ck for the system. Hence, our rst aim is to extend these de -nitions to mo dels where the execution is asynchronous. Another commonfeature of some security mo dels, at least in their original formulation, is theassumption of determinism 3, 10]: outputs are univo cally determined bythe history of the past inputs. Again, this assumption is unrealistic whenmo deling concurrent applications, where the actual b ehaviour dep ends onthe relative sp eed of the various sequential subsystems. Indeed, most pro-gramming languages provide mechanism for controlling/sp ecifying alterna-tive choices in the ow of the computation, which can also b e intrinsicallynondeterministic. Hence, our second aim is to extend these de nitions tomo dels where nondeterminism can b e expressed.

References
1] P. G. Allen. \A Comparison of Non-Interference and Non-Deducibility usingCSP". In Proceedings of the Fourth Workshop on the Foundations of ComputerSecurity, pages 43{54, Franconia, New Hampshire, June 1991.
2] J. C. M. Baeten and W.P. Weijland. Process Algebra. Cambrige UniversityPress, 1985. Cambrige Tracts in Theoretical Computer Science 18.
3] P. Bieb er and F. Cupp ens. \A Logical View of Secure Dep endencies". Journalof Computer Security, 1(1):99{129, 1992.
4] G. Boudol, I. Castellani, M. Hennessy, and A. Kiehn. \A Theory of Pro cesseswith Lo calities". In Proceedings Concur 92, pages 108{122. Springer-VerlagLNCS 630, 1992.
5] R. Cleaveland, J. Parrow, and B. Ste en. \The Concurrency Workb ench:a https://www.51lunwen.org/liuxuelunwendx/Semantics Based To ol for the Veri cation of Concurrent Systems". ACMTransactions on Programming Languages and Systems, Vol. 15 No. 1:36{72,January 1993.
6] P. Darondeau and P. Degano. \Causal trees: interleaving + causality". InProceedings LITP Spring School on Semantics of Systems of Concurrent Pro-cesses, pages 239{255. Lecture Notes in Computer Science, Vol. 469. Spri本论文由英语论文网提供整理，提供论文代写，英语论文代写，代写论文，代写英语论文，代写留学生论文，代写英文论文，留学生论文代写相关核心关键词搜索。