The paper considers several definitions of information flow security for intransitive policies from the point of view of the complexity of verifying whether a finite-state system is secure. The results are as follows. Checking (i) P-security (Goguen and Meseguer), (ii) IP-security (Haigh and Young), and (iii) TA-security (van der Meyden) are all in PTIME, while checking TO-security (van der Meyden) is undecidable. The most important ingredients in the proofs of the PTIME upper bounds are new characterizations of the respective security notions, which also enable the algorithms to return simple counterexamples demonstrating insecurity. Our results for IP-security improve a previous doubly exponential bound of Hadj-Alouane et al.
展开▼
机译：本文从验证有限状态系统是否安全的复杂性的角度来看，对信息流安全的几个定义。结果如下。检查（i）P-Security（Goguen和Meseguer），（ii）IP-Security（Haigh And Young），（III）TA-Security（van der Meyden）都在PTime，同时检查到安全（van der梅登）是不可判定的。 PTIME上限的证据中最重要的成分是各个安全概念的新特征，这也使算法能够返回展示不安全感的简单的反例。我们的IP-Security的结果改进了Hadj-Alouane等人的先前双重指数绑定。
展开▼
