Nondeterministic Admissible Interference

dc.creatorMullins,John
dc.date2000
dc.date.accessioned2024-02-06T12:50:50Z
dc.date.available2024-02-06T12:50:50Z
dc.descriptionIn this article we address the issue of confidentiality of information in the context of downgrading systems i.e. systems admitting information flow between secrecy levels only through a downgrader. Inspired by the intuition underlying the usual definition of admissible information flow, we propose an analogue based on trace equivalence as developed in the context of concurrency theory and on a modification of the usual definition of purge function. We also provide unwinding conditions to guarantee a consistent and complete proof method in terms of communicating transition systems. We take advantage of this framework to investigate its compositionality issues w.r.t. the main operators over communicating transition systems. We conclude the article with a short presentation of this work s most promising aspects in the perspective of future developments.
dc.formattext/html
dc.identifierhttps://doi.org/10.3217/jucs-006-11-1054
dc.identifierhttps://lib.jucs.org/article/27728/
dc.identifier.urihttps://openrepository.mephi.ru/handle/123456789/7848
dc.languageen
dc.publisherJournal of Universal Computer Science
dc.relationinfo:eu-repo/semantics/altIdentifier/eissn/0948-6968
dc.relationinfo:eu-repo/semantics/altIdentifier/pissn/0948-695X
dc.rightsinfo:eu-repo/semantics/openAccess
dc.rightsJ.UCS License
dc.sourceJUCS - Journal of Universal Computer Science 6(11): 1054-1070
dc.subjectspecification techniques
dc.subjectprogram verification
dc.subjectsecurity models
dc.subjectinformation flow properties
dc.subjectconfidentiality
dc.subjectnoninterference
dc.subjectintransitive noninterference
dc.titleNondeterministic Admissible Interference
dc.typeResearch Article
Файлы