非传递不干涉的复杂性与展开
密码学与安全
2013-08-07 v1
摘要
本文从验证有限状态系统是否安全的复杂性角度，考虑了非传递策略的信息流安全的几种定义。结果如下：检查 (i) P-安全 (Goguen 和 Meseguer)、(ii) IP-安全 (Haigh 和 Young) 以及 (iii) TA-安全 (van der Meyden) 均属于 PTIME，而检查 TO-安全 (van der Meyden) 和 ITO-安全 (van der Meyden) 则是不可判定的。PTIME 上界证明中最重要的要素是对各自安全概念的新刻画，这也导致了新的展开证明技术，这些技术被证明对这些安全概念是可靠且完备的，并使算法能够返回简单的反例以证明不安全。我们关于 IP-安全的结果改进了 Hadj-Alouane 等人此前提出的双指数界限。
引用
@article{arxiv.1308.1204,
title = {Complexity and Unwinding for Intransitive Noninterference},
author = {Sebastian Eggert and Ron van der Meyden and Henning Schnoor and Thomas Wilke},
journal= {arXiv preprint arXiv:1308.1204},
year = {2013}
}