Commit ac3eaef6 authored by Lawrence Paulson's avatar Lawrence Paulson
Browse files

Noninterference_Sequential_Composition website

parent 6c1913293a97
......@@ -3586,3 +3586,25 @@ abstract =
This entry can be used as a more advanced replacement for
HOL/Nominal in the Isabelle distribution.
</p>
[Noninterference_Sequential_Composition]
title = Conservation of CSP Noninterference Security under Sequential Composition
author = Pasquale Noce <mailto:pasquale.noce.lavoro@gmail.com>
date = 2016-04-26
topic = Computer Science/Security
abstract =
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.
<!DOCTYPE public "-//w3c//dtd html 4.01 transitional//en"
"http://www.w3.org/TR/html4/loose.dtd">
<html>
<head>
<title>Archive of Formal Proofs</title>
<link rel="stylesheet" type="text/css" href="../front.css">
<script src="../jquery.min.js"></script>
<script src="../script.js"></script>
<link rel="icon" href="../images/favicon.ico" type="image/icon">
<meta http-equiv="Content-Type" content="text/html; charset=utf-8">
</head>
<body>
<table width="100%">
<tbody>
<tr>
<td width="20%" align="center" valign="top">
<!-- navigation -->
<!--#include file="nav.html"-->
</td>
<td width="80%" valign="top">
<!-- content -->
<div align="center">
<p>&nbsp;</p>
<h1><font class="first">C</font>onservation
of
<font class="first">C</font>SP
<font class="first">N</font>oninterference
<font class="first">S</font>ecurity
under
<font class="first">S</font>equential
<font class="first">C</font>omposition
</h1>
<p></p>
<table width="80%" class="data">
<tbody>
<tr><td class="datahead" width="20%">Title:</td>
<td class="data" width="80%">Conservation of CSP Noninterference Security under Sequential Composition</td></tr>
<tr><td class="datahead">Author:</td>
<td class="data">Pasquale Noce (pasquale /dot/ noce /dot/ lavoro /at/ gmail /dot/ com)</td></tr>
<tr><td class="datahead">Submission date:</td>
<td class="data">2016-04-26</td></tr>
<tr><td class="datahead" valign="top">Abstract:</td>
<td class="abstract">
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.
</td></tr>
<tr><td class="datahead" valign="top">BibTeX:</td>
<td class="formatted">
<pre>@article{Noninterference_Sequential_Composition-AFP,
author = {Pasquale Noce},
title = {Conservation of CSP Noninterference Security under Sequential Composition},
journal = {Archive of Formal Proofs},
month = apr,
year = 2016,
note = {\url{http://isa-afp.org/entries/Noninterference_Sequential_Composition.shtml},
Formal proof development},
ISSN = {2150-914x},
}</pre>
</td></tr>
<tr><td class="datahead">License:</td>
<td class="data"><a href="http://isa-afp.org/LICENSE">BSD License</a></td></tr>
<tr><td class="datahead">Depends on:</td>
<td class="data"><a href="Noninterference_Ipurge_Unwinding.shtml">Noninterference_Ipurge_Unwinding</a></td></tr>
<!--#set var="status" value="-STATUS-" -->
<!--#set var="version" value="-VERSION-" -->
<!--#set var="afp-version" value="-AFPVERSION-" -->
<!---INCLUDE- file="devel-warning.shtml"-->
</tbody>
</table>
<p></p>
<!--#set var="name" value="Noninterference_Sequential_Composition" -->
<!--#set var="binfo" value="../browser_info/current/AFP/${name}" -->
<!--#set var="doc" value="${binfo}/document.pdf" -->
<!--#set var="outline" value="${binfo}/outline.pdf" -->
<!--#set var="browse" value="${binfo}/index.html" -->
<!--#set var="tar" value="../release/afp-${name}-current.tar.gz" -->
<table class="links">
<tbody>
<tr>
<td class="links">
<a href="<!--#echo var="outline" -->">Proof outline</a><br>
<a href="<!--#echo var="doc" -->">Proof document</a>
</td>
<!-- link to README.hmtl if no document exists -->
</tr>
<tr>
<td class="links">
<a href="<!--#echo var="browse" -->">Browse theories</a>
</td></tr>
<tr>
<td class="links">
<a href="<!--#echo var="tar" -->">Download this entry</a>
</td>
</tr>
<tr><td class="links">Older releases:
None </td></tr>
</tbody>
</table>
<!-- entry data end -->
</td> </tr> </table>
</body>
</html>
......@@ -49,6 +49,13 @@ A <a href="devel.shtml">development version</a> of the archive is available as w
<td class="head">2016</td>
</tr>
<tr><td class="entry">
2016-04-26:
<a href="entries/Noninterference_Sequential_Composition.shtml">Conservation of CSP Noninterference Security under Sequential Composition</a>
<br>Author:
Pasquale Noce
</td></tr>
<tr><td class="entry">
2016-04-12:
<a href="entries/KAD.shtml">Kleene Algebras with Domain</a>
......
......@@ -269,6 +269,7 @@
<a href="entries/Bounded_Deducibility_Security.shtml">Bounded_Deducibility_Security</a> &nbsp;
<a href="entries/Network_Security_Policy_Verification.shtml">Network_Security_Policy_Verification</a> &nbsp;
<a href="entries/Noninterference_Inductive_Unwinding.shtml">Noninterference_Inductive_Unwinding</a> &nbsp;
<a href="entries/Noninterference_Sequential_Composition.shtml">Noninterference_Sequential_Composition</a> &nbsp;
</div>
<h2>Logic</h2>
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment