187 lines
6.1 KiB
TeX
187 lines
6.1 KiB
TeX
\documentclass[11pt,DIV10,a4paper,twoside=semi,openright,titlepage]{scrreprt}
|
|
\usepackage{fixltx2e}
|
|
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
|
%%% Overrides the (rightfully issued) warning by Koma Script that \rm
|
|
%%% etc. should not be used (they are deprecated since more than a
|
|
%%% decade)
|
|
\DeclareOldFontCommand{\rm}{\normalfont\rmfamily}{\mathrm}
|
|
\DeclareOldFontCommand{\sf}{\normalfont\sffamily}{\mathsf}
|
|
\DeclareOldFontCommand{\tt}{\normalfont\ttfamily}{\mathtt}
|
|
\DeclareOldFontCommand{\bf}{\normalfont\bfseries}{\mathbf}
|
|
\DeclareOldFontCommand{\it}{\normalfont\itshape}{\mathit}
|
|
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
|
|
|
\usepackage{isabelle,isabellesym}
|
|
\usepackage{stmaryrd}
|
|
\usepackage{paralist}
|
|
\usepackage{xspace}
|
|
\usepackage{amsmath}
|
|
\usepackage[english]{babel}
|
|
\newcommand{\testgen}{HOL-TestGen\xspace}
|
|
\newcommand{\testgenFW}{HOL-TestGen/FW\xspace}
|
|
\usepackage[numbers, sort&compress, sectionbib]{natbib}
|
|
\usepackage{graphicx}
|
|
\usepackage{color}
|
|
\sloppy
|
|
|
|
\usepackage{amssymb}
|
|
\newcommand{\isadefinition} {{\operatorname{definition}}}
|
|
\newcommand{\types} {{\operatorname{type\_synonym}}}
|
|
\newcommand{\datatype} {{\operatorname{datatype}}}
|
|
\newcommand{\ap}{\,}
|
|
|
|
|
|
\newcommand{\dom}{\mathrm{dom}}
|
|
\newcommand{\ran}{\mathrm{ran}}
|
|
\newcommand{\ofType}{\!::\!}
|
|
\newcommand{\HolBin}[0]{\ensuremath{\mathrm{bin}}}
|
|
\newcommand{\HolNum}[0]{\ensuremath{\mathrm{num}}}
|
|
\newcommand{\HolBoolean}[0]{\ensuremath{\mathrm{bool}}}
|
|
\newcommand{\HolString}[0]{\ensuremath{\mathrm{string}}}
|
|
\newcommand{\HolInteger}[0]{\ensuremath{\mathrm{int}}}
|
|
\newcommand{\HolNat}[0]{\ensuremath{\mathrm{nat}}}
|
|
\newcommand{\HolReal}[0]{\ensuremath{\mathrm{real}}}
|
|
\newcommand{\HolSet}[1]{#1\ap\ensuremath{\mathrm{set}}}
|
|
\newcommand{\HolList}[1]{#1\ap\ensuremath{\mathrm{list}}}
|
|
%\newcommand{\HolOrderedSet}[1]{#1~\ensuremath{\mathrm{orderedset}}}
|
|
\newcommand{\HolMultiset}[1]{#1\ap\ensuremath{\mathrm{multiset}}}
|
|
\newcommand{\classType}[2]{#1\ap\ensuremath{\mathrm{#2}}}
|
|
\newcommand{\bottom}{\bot}
|
|
\DeclareMathOperator{\HolSome}{Some}
|
|
\DeclareMathOperator{\HolNone}{None}
|
|
\DeclareMathOperator{\Poverride}{\oplus}
|
|
\DeclareMathOperator{\prodTwo}{\otimes_2}
|
|
|
|
\newcommand{\HolMkSet}[1]{\operatorname{set} #1}
|
|
\newcommand{\spot}{.\;}
|
|
\newcommand{\where} {{\operatorname{where}}}
|
|
\DeclareMathOperator{\HolIf}{if}
|
|
\DeclareMathOperator{\HolLet}{let}
|
|
\DeclareMathOperator{\HolIn}{in}
|
|
\DeclareMathOperator{\HolThen}{then}
|
|
\DeclareMathOperator{\HolElse}{else}
|
|
|
|
|
|
\newcommand{\isasymmodels}{\isamath{\models}}
|
|
\newcommand{\HOL}{HOL}
|
|
|
|
\newcommand{\ie}{i.\,e.}
|
|
\newcommand{\eg}{e.\,g.}
|
|
|
|
\usepackage{pdfsetup}
|
|
|
|
\urlstyle{rm}
|
|
\isabellestyle{it}
|
|
\renewcommand{\isastyle}{\isastyleminor}
|
|
|
|
\pagestyle{empty}
|
|
\begin{document}
|
|
\renewcommand{\subsubsectionautorefname}{Section}
|
|
\renewcommand{\subsectionautorefname}{Section}
|
|
\renewcommand{\sectionautorefname}{Section}
|
|
\renewcommand{\chapterautorefname}{Chapter}
|
|
\newcommand{\subtableautorefname}{\tableautorefname}
|
|
\newcommand{\subfigureautorefname}{\figureautorefname}
|
|
|
|
\title{Formal Network Models and Their Application to Firewall Policies\\ (UPF-Firewall)}
|
|
\author{Achim D. Brucker\footnotemark[1] \quad
|
|
Lukas Br\"ugger\footnotemark[2] \quad
|
|
Burkhart Wolff\footnotemark[3]\\[1.5em]
|
|
\normalsize
|
|
\normalsize\footnotemark[1]~Department of Computer Science, The University of Sheffield, Sheffield, UK
|
|
\texorpdfstring{\\}{}
|
|
\normalsize\href{mailto:"Achim D. Brucker"
|
|
<a.brucker@sheffield.ac.uk>}{a.brucker@sheffield.ac.uk}\\[1em]
|
|
%
|
|
\normalsize\footnotemark[2]Information Security, ETH Zurich, 8092 Zurich, Switzerland
|
|
\texorpdfstring{\\}{}
|
|
\normalsize\href{mailto:"Lukas Bruegger"
|
|
<lukas.a.bruegger@gmail.com>}{Lukas.A.Bruegger@gmail.com}\\[1em]
|
|
%
|
|
\normalsize\footnotemark[3]~Univ. Paris-Sud, Laboratoire LRI,
|
|
UMR8623, 91405 Orsay, France
|
|
France\texorpdfstring{\\}{}
|
|
\normalsize\href{mailto:"Burkhart Wolff" <burkhart.wolff@lri.fr>}{burkhart.wolff@lri.fr}
|
|
}
|
|
|
|
\pagestyle{empty}
|
|
\publishers{%
|
|
\normalfont\normalsize%
|
|
\centerline{\textsf{\textbf{\large Abstract}}}
|
|
\vspace{1ex}%
|
|
\parbox{0.8\linewidth}{%
|
|
We present a formal model of network protocols and their
|
|
application to modeling firewall policies. The formalization is
|
|
based on the \emph{Unified Policy Framework} (UPF). The
|
|
formalization was originally developed with for generating test
|
|
cases for testing the security configuration actual firewall and
|
|
router (middle-boxes) using HOL-TestGen. Our work focuses on
|
|
modeling application level protocols on top of tcp/ip.
|
|
}
|
|
}
|
|
|
|
\maketitle
|
|
\cleardoublepage
|
|
\pagestyle{plain}
|
|
\tableofcontents
|
|
\cleardoublepage
|
|
|
|
\chapter{Introduction}
|
|
\input{introduction}
|
|
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
|
% <session>
|
|
% \input{session}
|
|
\input{UPF-Firewall}
|
|
\input{NetworkModels}
|
|
\input{NetworkCore}
|
|
\input{DatatypeAddress}
|
|
\input{DatatypePort}
|
|
\input{IntegerAddress}
|
|
\input{IntegerPort}
|
|
\input{IntegerPort_TCPUDP}
|
|
\input{IPv4}
|
|
\input{IPv4_TCPUDP.tex}
|
|
\input{PacketFilter.tex}
|
|
\input{PolicyCore}
|
|
\input{PolicyCombinators}
|
|
\input{PortCombinators}
|
|
\input{ProtocolPortCombinators}
|
|
\input{Ports}
|
|
\input{NAT}
|
|
\input{FWNormalisation.tex}
|
|
\input{FWNormalisationCore.tex}
|
|
\input{NormalisationGenericProofs.tex}
|
|
\input{NormalisationIntegerPortProof.tex}
|
|
\input{NormalisationIPPProofs.tex}
|
|
\input{StatefulFW}
|
|
\input{StatefulCore}
|
|
\input{FTP}
|
|
\input{FTP_WithPolicy}
|
|
\input{VOIP}
|
|
\input{FTPVOIP}
|
|
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
|
\input{Examples.tex}
|
|
\input{DMZ.tex}
|
|
\input{DMZDatatype.tex}
|
|
\input{DMZInteger.tex}
|
|
\input{PersonalFirewall.tex}
|
|
\input{PersonalFirewallInt.tex}
|
|
\input{PersonalFirewallIpv4.tex}
|
|
\input{PersonalFirewallDatatype.tex}
|
|
\input{Transformation.tex}
|
|
\input{Transformation01.tex}
|
|
\input{Transformation02.tex}
|
|
\input{NAT-FW.tex}
|
|
\input{Voice_over_IP.tex}
|
|
% </session>
|
|
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
|
|
|
\bibliographystyle{abbrvnat}
|
|
\bibliography{root}
|
|
\end{document}
|
|
|
|
%%% Local Variables:
|
|
%%% mode: latex
|
|
%%% TeX-master: t
|
|
%%% End:
|