2013/08/06 by Sebastian Eggert, Eggert, Sebastian, Ron van der Meyden +5
Computer Science · Physics and Astronomy · #Cryptography and Security (cs.CR) #Distributed systems and fault tolerance #FOS: Computer and information sciences #Quantum Mechanics and Applications #Security and Verification in Computing
paper · pdf · doi:10.48550/arxiv.1308.1204
openalex publication_date 2013/08/06 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
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, as is checking ITO-security (van der Meyden). The most important ingredients in the proofs of the PTIME upper bounds are new characterizations of the respective security notions, which also lead to new unwinding proof techniques that are shown to be sound and complete for these notions of security, and enable the algorithms to return simple counter-examples demonstrating insecurity. Our results for IP-security improve a previous doubly exponential bound of Hadj-Alouane et al.