Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] New in the AFP: The Inductive Unwinding Theorem


view this post on Zulip 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: Mar 28 2024 at 20:16 UTC