Email Gateway (Aug 22 2022 at 10:55): Email Gateway (Aug 22 2022 at 10:55):From: Larry Paulson <lp15@cam.ac.uk>
I’m happy to announce a new entry in the AFP:
"The necessary and sufficient condition for CSP noninterference security stated by the Ipurge Unwinding Theorem, which is expressed in terms of a pair of event lists varying over the set of process traces. … 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…. Specific variants of this theorem
are additionally proven for deterministic processes and trace set processes.”
The entry is online at http://afp.sourceforge.net/entries/Noninterference_Inductive_Unwinding.shtml
Many thanks to Pasquale Noce for this contribution!
Larry Paulson
Last updated: Nov 21 2024 at 12:39 UTC