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

new entry: Noninterference_Sequential_Composition

parent 4071e04d3366
This diff is collapsed.
chapter AFP
session "Noninterference_Sequential_Composition" (AFP) = "HOL" +
theories [document = false]
"../Noninterference_Ipurge_Unwinding/DeterministicProcesses"
theories
Propaedeutics
SequentialComposition
Counterexamples
document_files
"root.bib"
"root.tex"
# -*- shell-script -*-
# Get email when automated build fails. May be empty.
# values: "email1 email2 .. emailn"
NOTIFY="pasquale.noce@arjosystems.com"
# Participate in frequent (nightly) build (only for small submissions)
# values: "yes" "no"
FREQUENT="yes"
@article{
R1,
author={Pasquale Noce},
title={A General Method for the Proof of Theorems on Tail-recursive Functions},
journal={Archive of Formal Proofs},
month=dec,
year=2013,
note={\url{http://afp.sf.net/entries/Tail_Recursive_Functions.shtml}, Formal proof development},
ISSN={2150-914x}
}
@article{
R2,
author={Pasquale Noce},
title={Noninterference Security in Communicating Sequential Processes},
journal={Archive of Formal Proofs},
month=may,
year=2014,
note={\url{http://afp.sf.net/entries/Noninterference_CSP.shtml}, Formal proof development},
ISSN={2150-914x}
}
@article{
R3,
author={Pasquale Noce},
title={The Ipurge Unwinding Theorem for CSP Noninterference Security},
journal={Archive of Formal Proofs},
month=jun,
year=2015,
note={\url{http://afp.sf.net/entries/Noninterference_Ipurge_Unwinding.shtml}, Formal proof development},
ISSN={2150-914x}
}
@book{
R4,
author={C. A. R. Hoare},
title={Communicating Sequential Processes},
publisher={Prentice-Hall, Inc.},
year=1985
}
@book{
R5,
author={Tobias Nipkow and Gerwin Klein},
title={Concrete Semantics with Isabelle/HOL},
publisher={Springer},
year=2014,
note={\url{http://www.concrete-semantics.org/concrete-semantics.pdf}}
}
@manual{
R6,
author={Tobias Nipkow and Lawrence Paulson and Markus Wenzel},
title={Isabelle/HOL --- A Proof Assistant for Higher-Order Logic},
month=feb,
year=2016,
note={\url{http://isabelle.in.tum.de/website-Isabelle2016/dist/Isabelle2016/doc/tutorial.pdf}}
}
@manual{
R7,
author={Tobias Nipkow},
title={Programming and Proving in Isabelle/HOL},
month=feb,
year=2016,
note={\url{http://isabelle.in.tum.de/website-Isabelle2016/dist/Isabelle2016/doc/prog-prove.pdf}}
}
@manual{
R8,
author={Tobias Nipkow},
title={A Tutorial Introduction to Structured Isar Proofs},
note={\url{http://isabelle.in.tum.de/website-Isabelle2011/dist/Isabelle2011/doc/isar-overview.pdf}}
}
@manual{
R9,
author={Alexander Krauss},
title={Defining Recursive Functions in Isabelle/HOL},
note={\url{http://isabelle.in.tum.de/website-Isabelle2016/dist/Isabelle2016/doc/functions.pdf}}
}
\documentclass[11pt,a4paper]{article}
\usepackage{isabelle,isabellesym}
\renewcommand{\isastyletxt}{\isastyletext}
% further packages required for unusual symbols (see also
% isabellesym.sty), use only when needed
%\usepackage{amssymb}
%for \<leadsto>, \<box>, \<diamond>, \<sqsupset>, \<mho>, \<Join>,
%\<lhd>, \<lesssim>, \<greatersim>, \<lessapprox>, \<greaterapprox>,
%\<triangleq>, \<yen>, \<lozenge>
%\usepackage{eurosym}
%for \<euro>
%\usepackage[only,bigsqcap]{stmaryrd}
%for \<Sqinter>
%\usepackage{eufrak}
%for \<AA> ... \<ZZ>, \<aa> ... \<zz> (also included in amssymb)
%\usepackage{textcomp}
%for \<onequarter>, \<onehalf>, \<threequarters>, \<degree>, \<cent>,
%\<currency>
% this should be the last package used
\usepackage{pdfsetup}
% urls in roman style, theory text in math-similar italics
\urlstyle{rm}
\isabellestyle{it}
% for uniform font size
%\renewcommand{\isastyle}{\isastyleminor}
\begin{document}
\title{Conservation of CSP Noninterference Security\\under Sequential Composition}
\author{Pasquale Noce\\Security Certification Specialist at Arjo Systems, Italy\\pasquale dot noce dot lavoro at gmail dot com\\pasquale dot noce at arjosystems dot com}
\maketitle
\begin{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.
\end{abstract}
\tableofcontents
% sane default for proof documents
\parindent 0pt\parskip 0.5ex
% generated text of all theories
\input{session}
% bibliography
\bibliographystyle{abbrv}
\bibliography{root}
\end{document}
......@@ -164,6 +164,7 @@ Noninterference_CSP
Noninterference_Inductive_Unwinding
Noninterference_Ipurge_Unwinding
Noninterference_Generic_Unwinding
Noninterference_Sequential_Composition
NormByEval
Open_Induction
Ordinal
......
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