Email Gateway (Aug 22 2022 at 13:12): Email Gateway (Aug 22 2022 at 13:12):From: Lawrence Paulson <lp15@cam.ac.uk>
I’m pleased to announce a new AFP entry, by Pasquale Noce, on the conservation of CSP noninterference security under sequential composition. Abstract and other details below. Thank you, Pasquale!
And please note that the AFP has a new URL: http://www.isa-afp.org/
The AFP has moved from SourceForge because of a lot of issues there.
Larry Paulson
Conservation of CSP Noninterference Security under Sequential Composition
Pasquale Noce
In his outstanding work on Communicating Sequential Processes, Hoare has defined two fundamental binary operations allowing to compose the input processes into another, typically more complex, process: sequential composition and concurrent composition. Particularly, the output of the former operation is a process that initially behaves like the first operand, and then like the second operand once the execution of the first one has terminated successfully, as long as it does. This paper formalizes Hoare's definition of sequential composition and proves, in the general case of a possibly intransitive policy, that CSP noninterference security is conserved under this operation, provided that successful termination cannot be affected by confidential events and cannot occur as an alternative to other events in the traces of the first operand. Both of these assumptions are shown, by means of counterexamples, to be necessary for the theorem to hold.
http://www.isa-afp.org/entries/Noninterference_Sequential_Composition.shtml
Email Gateway (Aug 22 2022 at 13:12):From: Makarius <makarius@sketis.net>
At last! With a delay of only 10 years after SourceForge issues started.
Makarius
Email Gateway (Aug 22 2022 at 13:12):From: Gerwin Klein <Gerwin.Klein@nicta.com.au>
Archives shouldn’t move too often, so we’ve been very careful and conservative with this, but I’m happy that we have finally moved ahead.
SF has had reliability issues for a long time, which Makarius is alluding to, and they’ve had malware issues more recently.
The new domain http://isa-afp.org is controlled by us and should be stable for the future. Currently the site is hosted at TU Munich, but even if the physical server moves in the future, the URLs etc will remain stable.
Existing links to SF in papers and other locations are redirected automatically to their counterparts on http://isa-afp.org, and we will keep maintaining a skeleton of the SF site to retain control and to make sure the redirects stay in place.
Cheers,
Gerwin
The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.
Last updated: Apr 26 2024 at 04:17 UTC