Sciweavers

Share
AFP
2015
Springer

The Ipurge Unwinding Theorem for CSP Noninterference Security

3 years 7 months ago
The Ipurge Unwinding Theorem for CSP Noninterference Security
The definition of noninterference security for Communicating Sequential Processes requires to consider any possible future, i.e. any indefinitely long sequence of subsequent events and any indefinitely large set of refused events associated to that sequence, for each process trace. In order to render the verification of the security of a process more straightforward, there is a need of some sufficient condition for security such that just individual accepted and refused events, rather than unbounded sequences and sets of events, have to be considered. Of course, if such a sufficient condition were necessary as well, it would be even more valuable, since it would permit to prove not only that a process is secure by verifying that the condition holds, but also that a process is not secure by verifying that the condition fails to hold. This paper provides a necessary and sufficient condition for CSP noninterference security, which indeed requires to just consider individual accepted ...
Pasquale Noce
Added 13 Apr 2016
Updated 13 Apr 2016
Type Journal
Year 2015
Where AFP
Authors Pasquale Noce
Comments (0)
books