%0 Journal Article
%T Petri net-based analysis and verification of information flow security properties<br>基于Petri网的信息流安全属性的分析与验证*
%A CHEN Song
%A ZHOU Cong-hua
%A JU Shi-guang
%A WANG Ji
%A <br>陈松
%A 周从华
%A 鞠时光
%A 王基
%J 计算机应用研究
%D 2010
%I 
%X The definition of information flow security properties are based on different semantic model, which is difficult to make comparison between them. This paper used Petri net as unified model to describe the security system, defined four security properties on Petri net and analyzed the logic relationship between them. The traditional algorithmic verification method for information flow was known as unwinding method, which was not sufficient and could be just used in deterministic system. The second work of this paper was giving a sufficient algorithmic verification method for the security properties had been defined and programming to implement the method. Finally, it shows the application of this method in covert channel.
%K Petri net
%K noninterference property
%K generalized noninterference property
%K generalized noninference property
%K separability property<br>Petri网
%K 无干扰属性
%K 广义无干扰属性
%K 广义非推断属性
%K 可分离属性
%U http://www.alljournals.cn/get_abstract_url.aspx?pcid=5B3AB970F71A803DEACDC0559115BFCF0A068CD97DD29835&cid=8240383F08CE46C8B05036380D75B607&jid=A9D9BE08CDC44144BE8B5685705D3AED&aid=34D565CF297179D337ACBE3450F0A6FD&yid=140ECF96957D60B2&vid=DB817633AA4F79B9&iid=59906B3B2830C2C5&sid=CBCEF6F4364C06A3&eid=3F5141272968AFF9&journal_id=1001-3695&journal_name=计算机应用研究&referenced_num=0&reference_num=12