Checking Non-Interference Based on Unfolding Techniques of Petri Nets

Petri-net-based information flow analysis is an effective approach to check non-interference and analyze information security. However, Petri nets generally utilize the interleaving semantics, and easily suffer from the state space explosion problem. In this paper, we utilize unfolding techniques in checking non-interference. Specifically, we introduce some theorems to depict the structural behaviors of non-interference in the unfolding, and propose the finite interference-complete prefix (FICP) for checking non-interference. The theorems and FICP model benefit the checking of non-interference, which can alleviate the state space explosion problem.