Petri net-based analysis and verification of information flow security properties
基于Petri网的信息流安全属性的分析与验证*

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.