期刊名称：International Journal of Hybrid Information Technology
印刷版ISSN：1738-9968
出版年度：2015
卷号：8
期号：7
页码：243-252
DOI：10.14257/ijhit.2015.8.7.23
出版社：SERSC
摘要：The goal of high assurance systems development by formal verification motivates the investigation of techniques whereby a systems design or implementation can be formally shown to satisfy a formal definition of security. The security of unwinding relations provides a proof method that has been applied to establish that a system satisfies noninterference properties, but it requires significant human ingenuity to define an unwinding relation that forms the basis for the proof, and typically also has involved manual driving (proof rule selection) of the theorem proving tool within which the proof is conducted. The property of purge-based definition proposed by Goguen and Meseguer, intransitive purge-based definition proposed by Haigh and Young, and some more definitions TA-secure, TO-secure, ITO-secure proposed by van der Meyden are considered in this paper. The property can be used in the proof of noninterference property without unwinding relations.
关键词：Intransitive Noninterference; Information Security; Noninterference ; Property
