Sciweavers

Share
AFP
2015
Springer

The Inductive Unwinding Theorem for CSP Noninterference Security

3 years 7 months ago
The Inductive Unwinding Theorem for CSP Noninterference Security
The necessary and sufficient condition for CSP noninterference security stated by the Ipurge Unwinding Theorem is expressed in terms of a pair of event lists varying over the set of process traces. This does not render it suitable for the subsequent application of rule induction in the case of a process defined inductively, since rule induction may rather be applied to a single variable ranging over an inductively defined set. Starting from the Ipurge Unwinding Theorem, this paper derives a necessary and sufficient condition for CSP noninterference security that involves a single event list varying over the set of process traces, and is thus suitable for rule induction; hence its name, Inductive Unwinding Theorem. Similarly to the Ipurge Unwinding Theorem, the new theorem only requires to consider individual accepted and refused events for each process trace, and applies to the general case of a possibly intransitive noninterference policy. Specific variants of this theorem are add...
Pasquale Noce
Added 13 Apr 2016
Updated 13 Apr 2016
Type Journal
Year 2015
Where AFP
Authors Pasquale Noce
Comments (0)
books