diff --git a/thys/Automated_Stateful_Protocol_Verification/document/root.tex b/thys/Automated_Stateful_Protocol_Verification/document/root.tex --- a/thys/Automated_Stateful_Protocol_Verification/document/root.tex +++ b/thys/Automated_Stateful_Protocol_Verification/document/root.tex @@ -1,166 +1,166 @@ \documentclass[10pt,DIV16,a4paper,abstract=true,twoside=semi,openright] {scrreprt} -\usepackage[USenglish]{babel} +\usepackage[english]{babel} \usepackage[numbers, sort&compress]{natbib} \usepackage{isabelle,isabellesym} \usepackage{booktabs} \usepackage{paralist} \usepackage{graphicx} \usepackage{amssymb} \usepackage{xspace} \usepackage{xcolor} \usepackage{hyperref} \pagestyle{headings} \isabellestyle{default} \setcounter{tocdepth}{1} \newcommand{\ie}{i.\,e.\xspace} \newcommand{\eg}{e.\,g.\xspace} \newcommand{\thy}{\isabellecontext} \renewcommand{\isamarkupsection}[1]{% \begingroup% \def\isacharunderscore{\textunderscore}% \section{#1 (\thy)}% \def\isacharunderscore{-}% \expandafter\label{sec:\isabellecontext}% \endgroup% } \title{Automated Stateful Protocol Verification} \author{% \begin{minipage}{.8\textwidth} \centering \href{https://www.dtu.dk/english/service/phonebook/person?id=64207}{Andreas~V.~Hess}\footnotemark[1] \qquad\qquad \href{https://people.compute.dtu.dk/samo/}{Sebastian~M{\"o}dersheim}\footnotemark[1] \\ \href{http://www.brucker.ch/}{Achim~D.~Brucker}\footnotemark[2] \qquad\qquad \href{https://people.compute.dtu.dk/andschl}{Anders~Schlichtkrull} \end{minipage} } \publishers{% \footnotemark[1]~DTU Compute, Technical University of Denmark, Lyngby, Denmark\texorpdfstring{\\}{, } \texttt{\{avhe, samo, andschl\}@dtu.dk}\\[2em] % \footnotemark[2]~ Department of Computer Science, University of Exeter, Exeter, UK\texorpdfstring{\\}{, } \texttt{a.brucker@exeter.ac.uk} % } \begin{document} \maketitle \begin{abstract} \begin{quote} In protocol verification we observe a wide spectrum from fully automated methods to interactive theorem proving with proof assistants like Isabelle/HOL. In this AFP entry, we present a fully-automated approach for verifying stateful security protocols, i.e., protocols with mutable state that may span several sessions. The approach supports reachability goals like secrecy and authentication. We also include a simple user-friendly transaction-based protocol specification language that is embedded into Isabelle. \bigskip \noindent{\textbf{Keywords:}} Fully automated verification, stateful security protocols \end{quote} \end{abstract} \tableofcontents \cleardoublepage \chapter{Introduction} In protocol verification we observe a wide spectrum from fully automated methods to interactive theorem proving with proof assistants like Isabelle/HOL. The latter provide overwhelmingly high assurance of the correctness, which automated methods often cannot: due to their complexity, bugs in such automated verification tools are likely and thus the risk of erroneously verifying a flawed protocol is non-negligible. There are a few works that try to combine advantages from both ends of the spectrum: a high degree of automation and assurance. Inspired by~\cite{brucker.ea:integrating:2009}, we present here a first step towards achieving this for a more challenging class of protocols, namely those that work with a mutable long-term state. To our knowledge this is the first approach that achieves fully automated verification of stateful protocols in an LCF-style theorem prover. The approach also includes a simple user-friendly transaction-based protocol specification language embedded into Isabelle, and can also leverage a number of existing results such as soundness of a typed model (see, e.g.,~\cite{hess:typing:2018,hess.ea:formalizing:2017,hess.ea:typing:2018}) and compositionality (see, e.g.,~\cite{hess:typing:2018,hess.ea:stateful:2018}). The Isabelle formalization extends the AFP entry on stateful protocol composition and typing~\cite{hess.ea:stateful:2020}. \begin{figure} \centering \includegraphics[height=\textheight]{session_graph} \caption{The Dependency Graph of the Isabelle Theories.\label{fig:session-graph}} \end{figure} The rest of this document is automatically generated from the formalization in Isabelle/HOL, i.e., all content is checked by Isabelle. Overall, the structure of this document follows the theory dependencies (see \autoref{fig:session-graph}): We start with the formal framework for verifying stateful security protocols (\autoref{cha:verification}). We continue with the setup for supporting the high-level protocol specifications language for security protocols (the Trac format) and the implementation of the fully automated proof tactics (\autoref{cha:trac}). Finally, we present examples (\autoref{cha:examples}). \paragraph{Acknowledgments} This work was supported by the Sapere-Aude project ``Composec: Secure Composition of Distributed Systems'', grant 4184-00334B of the Danish Council for Independent Research. \clearpage \chapter{Stateful Protocol Verification} \label{cha:verification} \input{Transactions.tex} \input{Term_Abstraction.tex} \input{Stateful_Protocol_Model.tex} \input{Term_Variants.tex} \input{Term_Implication.tex} \input{Stateful_Protocol_Verification.tex} \chapter{Trac Support and Automation} \label{cha:trac} \input{Eisbach_Protocol_Verification.tex} \input{ml_yacc_lib.tex} \input{trac_term.tex} \input{trac_fp_parser.tex} \input{trac_protocol_parser.tex} \input{trac.tex} \chapter{Examples} \label{cha:examples} \input{Keyserver.tex} \input{Keyserver2.tex} \input{Keyserver_Composition.tex} \input{PKCS_Model03.tex} \input{PKCS_Model07.tex} \input{PKCS_Model09.tex} % \input{session} {\small \bibliographystyle{abbrvnat} \bibliography{root} } \end{document} \endinput %%% Local Variables: %%% mode: latex %%% TeX-master: t %%% End: diff --git a/thys/Core_DOM/document/root.tex b/thys/Core_DOM/document/root.tex --- a/thys/Core_DOM/document/root.tex +++ b/thys/Core_DOM/document/root.tex @@ -1,266 +1,266 @@ \documentclass[10pt,DIV16,a4paper,abstract=true,twoside=semi,openright] {scrreprt} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%% Overrides the (rightfully issued) warnings 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[USenglish]{babel} +\usepackage[english]{babel} \usepackage[numbers, sort&compress]{natbib} \usepackage{isabelle,isabellesym} \usepackage{booktabs} \usepackage{paralist} \usepackage{graphicx} \usepackage{amssymb} \usepackage{xspace} \usepackage{xcolor} \usepackage{listings} \lstloadlanguages{HTML} \usepackage[]{mathtools} \usepackage[pdfpagelabels, pageanchor=false, plainpages=false]{hyperref} \lstdefinestyle{html}{language=XML, basicstyle=\ttfamily, commentstyle=\itshape, keywordstyle=\color{blue}, ndkeywordstyle=\color{blue}, } \lstdefinestyle{displayhtml}{style=html, floatplacement={tbp}, captionpos=b, framexleftmargin=0pt, basicstyle=\ttfamily\scriptsize, backgroundcolor=\color{black!2}, frame=lines, } \lstnewenvironment{html}[1][]{\lstset{style=displayhtml, #1}}{} \def\inlinehtml{\lstinline[style=html, columns=fullflexible]} \pagestyle{headings} \isabellestyle{default} \setcounter{tocdepth}{1} \newcommand{\ie}{i.\,e.\xspace} \newcommand{\eg}{e.\,g.\xspace} \newcommand{\thy}{\isabellecontext} \renewcommand{\isamarkupsection}[1]{% \begingroup% \def\isacharunderscore{\textunderscore}% \section{#1 (\thy)}% \def\isacharunderscore{-}% \expandafter\label{sec:\isabellecontext}% \endgroup% } \title{Core DOM\\\medskip \Large A Formal Model of the Document Object Model}% \author{Achim~D.~Brucker \and Michael~Herzberg}% \publishers{ Department of Computer Science\\ The University of Sheffield\\ Sheffield, UK\\ \texttt{\{\href{mailto:a.brucker@sheffield.ac.uk}{a.brucker}, \href{mailto:msherzberg1@sheffield.ac.uk}{msherzberg1}\}@sheffield.ac.uk} } \begin{document} \maketitle \begin{abstract} \begin{quote} In this AFP entry, we formalize the core of the Document Object Model (DOM). At its core, the DOM defines a tree-like data structure for representing documents in general and HTML documents in particular. It is the heart of any modern web browser. Formalizing the key concepts of the DOM is a prerequisite for the formal reasoning over client-side JavaScript programs and for the analysis of security concepts in modern web browsers. We present a formalization of the core DOM, with focus on the \emph{node-tree} and the operations defined on node-trees, in Isabelle/HOL\@. We use the formalization to verify the functional correctness of the most important functions defined in the DOM standard. Moreover, our formalization is \begin{inparaenum} \item \emph{extensible}, i.e., can be extended without the need of re-proving already proven properties and \item \emph{executable}, i.e., we can generate executable code from our specification. \end{inparaenum} \bigskip \noindent{\textbf{Keywords:}} Document Object Model, DOM, Formal Semantics, Isabelle/HOL \end{quote} \end{abstract} \tableofcontents \cleardoublepage \chapter{Introduction} In a world in which more and more applications are offered as services on the internet, web browsers start to take on a similarly central role in our daily IT infrastructure as operating systems. Thus, web browsers should be developed as rigidly and formally as operating systems. While formal methods are a well-established technique in the development of operating systems (see, \eg,~\citet{klein:operating:2009} for an overview of formal verification of operating systems), there are few proposals for improving the development of web browsers using formal approaches~\cite{gardner.ea:dom:2008,raad.ea:dom:2016,jang.ea:establishing:2012,bohannon.ea:featherweight:2010}. As a first step towards a verified client-side web application stack, we model and formally verify the Document Object Model (DOM) in Isabelle/HOL\@. The DOM~\cite{whatwg:dom:2017,w3c:dom:2015} is \emph{the} central data structure of all modern web browsers. At its core, the Document Object Model (DOM), defines a tree-like data structure for representing documents in general and HTML documents in particular. Thus, the correctness of a DOM implementation is crucial for ensuring that a web browser displays web pages correctly. Moreover, the DOM is the core data structure underlying client-side JavaScript programs, \ie, client-side JavaScript programs are mostly programs that read, write, and update the DOM. In more detail, we formalize the core DOM as a shallow embedding~\cite{joyce.ea:higher:1994} in Isabelle/HOL\@. Our formalization is based on a typed data model for the \emph{node-tree}, \ie, a data structure for representing XML-like documents in a tree structure. Furthermore, we formalize a typed heap for storing (partial) node-trees together with the necessary consistency constraints. Finally, we formalize the operations (as described in the DOM standard~\cite{whatwg:dom:2017}) on this heap that allow manipulating node-trees. Our machine-checked formalization of the DOM node tree~\cite{whatwg:dom:2017} has the following desirable properties: \begin{itemize} \item It provides a \emph{consistency guarantee.} Since all definitions in our formal semantics are conservative and all rules are derived, the logical consistency of the DOM node-tree is reduced to the consistency of HOL. \item It serves as a \emph{technical basis for a proof system.} Based on the derived rules and specific setup of proof tactics over node-trees, our formalization provides a generic proof environment for the verification of programs manipulating node-trees. \item It is \emph{executable}, which allows to validate its compliance to the standard by evaluating the compliance test suite on the formal model and \item It is \emph{extensible} in the sense of~\cite{brucker.ea:extensible:2008-b,brucker:interactive:2007}, \ie, properties proven over the core DOM do not need to be re-proven for object-oriented extensions such as the HTML document model. \end{itemize} The rest of this document is automatically generated from the formalization in Isabelle/HOL, i.e., all content is checked by Isabelle.\footnote{For a brief overview of the work, we refer the reader to~\cite{brucker.ea:core-dom:2018}.} The structure follows the theory dependencies (see \autoref{fig:session-graph}): we start with introducing the technical preliminaries of our formalization (\autoref{cha:perliminaries}). Next, we introduce the concepts of pointers (\autoref{cha:pointers}) and classes (\autoref{cha:classes}), i.e., the core object-oriented datatypes of the DOM. On top of this data model, we define the functional behavior of the DOM classes, i.e., their methods (\autoref{cha:monads}). In \autoref{cha:dom}, we introduce the formalization of the functionality of the core DOM, i.e., the \emph{main entry point for users} that want to use this AFP entry. Finally, we formalize the relevant compliance test cases in \autoref{cha:tests}. \begin{figure} \centering \includegraphics[width=.8\textwidth]{session_graph} \caption{The Dependency Graph of the Isabelle Theories.\label{fig:session-graph}} \end{figure} \clearpage \chapter{Preliminaries} \label{cha:perliminaries} In this chapter, we introduce the technical preliminaries of our formalization of the core DOM, namely a mechanism for hiding type variables and the heap error monad. \input{Hiding_Type_Variables} \input{Heap_Error_Monad} \chapter{References and Pointers} \label{cha:pointers} In this chapter, we introduce a generic type for object-oriented references and typed pointers for each class type defined in the DOM standard. \input{Ref} \input{ObjectPointer} \input{NodePointer} \input{ElementPointer} \input{CharacterDataPointer} \input{DocumentPointer} \input{ShadowRootPointer} \chapter{Classes} \label{cha:classes} In this chapter, we introduce the classes of our DOM model. The definition of the class types follows closely the one of the pointer types. Instead of datatypes, we use records for our classes. a generic type for object-oriented references and typed pointers for each class type defined in the DOM standard. \input{BaseClass} \input{ObjectClass} \input{NodeClass} \input{ElementClass} \input{CharacterDataClass} \input{DocumentClass} \chapter{Monadic Object Constructors and Accessors} \label{cha:monads} In this chapter, we introduce the moandic method definitions for the classes of our DOM formalization. Again the overall structure follows the same structure as for the class types and the pointer types. \input{BaseMonad} \input{ObjectMonad} \input{NodeMonad} \input{ElementMonad} \input{CharacterDataMonad} \input{DocumentMonad} \chapter{The Core DOM} \label{cha:dom} In this chapter, we introduce the formalization of the core DOM, i.e., the most important algorithms for querying or modifying the DOM, as defined in the standard. For more details, we refer the reader to \cite{brucker.ea:core-dom:2018}. \input{Core_DOM_Basic_Datatypes} \input{Core_DOM_Functions} \input{Core_DOM_Heap_WF} \input{Core_DOM} \chapter{Test Suite} \label{cha:tests} In this chapter, we present the formalized compliance test cases for the core DOM. As our formalization is executable, we can (symbolically) execute the test cases on top of our model. Executing these test cases successfully shows that our model is compliant to the official DOM standard. As future work, we plan to generate test cases from our formal model (e.g., using~\cite{brucker.ea:interactive:2005,brucker.ea:theorem-prover:2012}) to improve the quality of the official compliance test suite. For more details on the relation of test and proof in the context of web standards, we refer the reader to \cite{brucker.ea:standard-compliance-testing:2018}. \input{Core_DOM_BaseTest} \input{Document_adoptNode} \input{Document_getElementById} \input{Node_insertBefore} \input{Node_removeChild} \input{Core_DOM_Tests} {\small \bibliographystyle{abbrvnat} \bibliography{root} } \end{document} %%% Local Variables: %%% mode: latex %%% TeX-master: t %%% End: diff --git a/thys/Extended_Finite_State_Machine_Inference/document/root.tex b/thys/Extended_Finite_State_Machine_Inference/document/root.tex --- a/thys/Extended_Finite_State_Machine_Inference/document/root.tex +++ b/thys/Extended_Finite_State_Machine_Inference/document/root.tex @@ -1,108 +1,108 @@ \documentclass[10pt,DIV16,a4paper,abstract=true,twoside=semi,openright]{scrreprt} -\usepackage[USenglish]{babel} +\usepackage[english]{babel} \usepackage[numbers, sort&compress]{natbib} \usepackage{isabelle,isabellesym} \usepackage{booktabs} \usepackage{paralist} \usepackage{graphicx} \usepackage{amssymb} \usepackage{xspace} \usepackage{xcolor} \usepackage{hyperref} \usepackage{rotating} \pagestyle{headings} \isabellestyle{default} \setcounter{tocdepth}{1} \newcommand{\ie}{i.\,e.\xspace} \newcommand{\eg}{e.\,g.\xspace} \newcommand{\thy}{\isabellecontext} \renewcommand{\isamarkupsection}[1]{% \begingroup% \def\isacharunderscore{\textunderscore}% \section{#1 (\thy)}% \def\isacharunderscore{-}% \expandafter\label{sec:\isabellecontext}% \endgroup% } \newcommand{\orcidID}[1]{} % temp. hack \newcommand{\repeatisanl}[1] {\ifnum#1=0\else\isanewline\repeatisanl{\numexpr#1-1}\fi} \newcommand{\snip}[4]{\repeatisanl#2#4\repeatisanl#3} \title{Inference of Extended Finite State Machines}% \author{% \begin{minipage}{.8\textwidth} \centering Michael~Foster\footnotemark[1]\orcidID{0000-0001-8233-9873}% \qquad\qquad% Achim~D.~Brucker\footnotemark[2]\orcidID{0000-0002-6355-1200}% \\% Ramsay~G.~Taylor\footnotemark[1]\orcidID{0000-0002-4036-7590}% \qquad\qquad% John~Derrick\footnotemark[1]\orcidID{0000-0002-6631-8914}% \end{minipage} } \publishers{% \footnotemark[1]~Department of Computer Science, The University of Sheffield, Sheffield, UK\texorpdfstring{\\}{, }% \texttt{\{% \href{mailto:jmafoster1@sheffield.ac.uk}{jmafoster1},% \href{mailto:r.g.taylor@sheffield.ac.uk}{r.g.taylor},% \href{mailto:j.derrick@sheffield.ac.uk}{j.derrick}% \}@sheffield.ac.uk}\\[2em]% \footnotemark[2]~% Department of Computer Science, University of Exeter, Exeter, UK\texorpdfstring{\\}{, }% \href{mailto:a.brucker@exeter.ac.uk}{\texttt{a.brucker@exeter.ac.uk}}% } \begin{document} \maketitle \begin{abstract} In this AFP entry, we provide a formal implementation of a state-merging technique to infer extended finite state machines (EFSMs), complete with output and update functions, from black-box traces. In particular, we define the \emph{subsumption in context} relation as a means of determining whether one transition is able to account for the behaviour of another. Building on this, we define the \emph{direct subsumption} relation, which lifts the \emph{subsumption in context} relation to EFSM level such that we can use it to determine whether it is safe to merge a given pair of transitions. Key proofs include the conditions necessary for subsumption to occur and the that subsumption and direct subsumption are preorder relations. We also provide a number of different \emph{heuristics} which can be used to abstract away concrete values into \emph{registers} so that more states and transitions can be merged and provide proofs of the various conditions which must hold for these abstractions to subsume their ungeneralised counterparts. A Code Generator setup to create executable Scala code is also defined. \begin{quote} \bigskip \noindent{\textbf{Keywords:} EFSMs, Model inference, Reverse engineering } \end{quote} \end{abstract} \tableofcontents \cleardoublepage \chapter{Introduction}\label{chap:intro} This AFP entry provides a formal implementation of a state-merging technique to infer EFSMs from black-box traces and is an accompaniment to work published in \cite{foster2018} and \cite{foster2019}. The inference technique builds off classical FSM inference techniques which work by first building a Prefix Tree Acceptor from traces of the underlying system, and then iteratively merging states which share behaviour to form a smaller model. Most notably, we formalise the definitions of \emph{subsumption in context} and \emph{direct subsumption.} When merging EFSM transitions, one must \emph{account for} the behaviour of the other. The \emph{subsumption in context} relation from \cite{foster2018} formalises the intuition that, in certain contexts, a transition $t_2$ reproduces the behaviour of, and updates the data state in a manner consistent with, another transition $t_1$, meaning that $t_2$ can be used in place of $t_1$ with no observable difference in behaviour. This relation requires us to supply a context in which to test subsumption, but there is a problem when we try to apply this to inference: Which context should we use? The \emph{directly subsumes} relation presented in \cite{foster2019} incorporates subsumption into a relation which can be used to determine if it is safe to merge a pair of transitions in an EFSM. It is this which allows us to take the subsumption relation from \cite{foster2018} and use it in the inference process. The rest of this document is automatically generated from the formalization in Isabelle/HOL, i.e., all content is checked by Isabelle. Overall, the structure of this document follows the theory dependencies (see \autoref{fig:session-graph}). \begin{sidewaysfigure} \centering \resizebox{\textheight}{!}{\includegraphics[height=\textheight]{session_graph}} \caption{The Dependency Graph of the Isabelle Theories.\label{fig:session-graph}} \end{sidewaysfigure} \nocite{foster.ea:efsm:2018} \clearpage \input{session} {\small \bibliographystyle{abbrvnat} \bibliography{root} } \end{document} \endinput %%% Local Variables: %%% mode: latex %%% TeX-master: t %%% End: diff --git a/thys/Extended_Finite_State_Machines/document/root.tex b/thys/Extended_Finite_State_Machines/document/root.tex --- a/thys/Extended_Finite_State_Machines/document/root.tex +++ b/thys/Extended_Finite_State_Machines/document/root.tex @@ -1,148 +1,148 @@ \documentclass[10pt,DIV16,a4paper,abstract=true,twoside=semi,openright]{scrreprt} -\usepackage[USenglish]{babel} +\usepackage[english]{babel} \usepackage[numbers, sort&compress]{natbib} \usepackage{isabelle,isabellesym} \usepackage{booktabs} \usepackage{paralist} \usepackage{graphicx} \usepackage{amssymb} \usepackage{xspace} \usepackage{xcolor} \usepackage{hyperref} \usepackage{enumitem} % Mess about with itemize, enumerate, description styles \newcommand\mydescriptionlabel[1]{\hspace{\leftmargini}\textbf{#1}} \newenvironment{where}{% \let\descriptionlabel\mydescriptionlabel \description[itemsep=0em, font=\normalfont] }{% \enddescription } \pagestyle{headings} \isabellestyle{default} \setcounter{tocdepth}{1} \newcommand{\ie}{i.\,e.\xspace} \newcommand{\eg}{e.\,g.\xspace} \newcommand{\thy}{\isabellecontext} \renewcommand{\isamarkupsection}[1]{% \begingroup% \def\isacharunderscore{\textunderscore}% \section{#1 (\thy)}% \def\isacharunderscore{-}% \expandafter\label{sec:\isabellecontext}% \endgroup% } \newcommand{\orcidID}[1]{} % temp. hack \newcommand{\repeatisanl}[1] {\ifnum#1=0\else\isanewline\repeatisanl{\numexpr#1-1}\fi} \newcommand{\snip}[4]{\repeatisanl#2#4\repeatisanl#3} \newcommand{\DefineSnippet}[2]{% \expandafter\newcommand\csname snippet--#1\endcsname{% \begin{quote} \begin{isabelle} #2 \end{isabelle} \end{quote}}} \newcommand{\Snippet}[1]{% \ifcsname snippet--#1\endcsname{\csname snippet--#1\endcsname}% \else+++++++ERROR: Snippet ``#1 not defined''+++++++ \fi} \title{A Formal Model of Extended Finite State Machines}% \author{% \begin{minipage}{.8\textwidth} \centering Michael~Foster\footnotemark[1]\orcidID{0000-0001-8233-9873}% \qquad\qquad% Achim~D.~Brucker\footnotemark[2]\orcidID{0000-0002-6355-1200}% \\% Ramsay~G.~Taylor\footnotemark[1]\orcidID{0000-0002-4036-7590}% \qquad\qquad% John~Derrick\footnotemark[1]\orcidID{0000-0002-6631-8914}% \end{minipage} } \publishers{% \footnotemark[1]~Department of Computer Science, The University of Sheffield, Sheffield, UK\texorpdfstring{\\}{, }% \texttt{\{% \href{mailto:jmafoster1@sheffield.ac.uk}{jmafoster1},% \href{mailto:r.g.taylor@sheffield.ac.uk}{r.g.taylor},% \href{mailto:j.derrick@sheffield.ac.uk}{j.derrick}% \}@sheffield.ac.uk}\\[2em]% \footnotemark[2]~% Department of Computer Science, University of Exeter, Exeter, UK\texorpdfstring{\\}{, }% \href{mailto:a.brucker@exeter.ac.uk}{\texttt{a.brucker@exeter.ac.uk}}% } \begin{document} \maketitle \begin{abstract} In this AFP entry, we provide a formalisation of extended finite state machines (EFSMs) where models are represented as finite sets of transitions between states. EFSMs execute traces to produce observable outputs. We also define various simulation and equality metrics for EFSMs in terms of traces and prove their strengths in relation to each other. Another key contribution is a framework of function definitions such that LTL properties can be phrased over EFSMs. Finally, we provide a simple example case study in the form of a drinks machine. \begin{quote} \bigskip \noindent{\textbf{Keywords:} Extended Finite State Machines, Automata, Linear Temporal Logic} \end{quote} \end{abstract} \tableofcontents \cleardoublepage \chapter{Introduction} This AFP entry formalises extended finite state machines (EFSMs) as defined in \cite{foster2018}. Here, models maintain both a \emph{control flow state} and a \emph{data state}, which takes the form of a set of \emph{registers} to which values may be assigned. Transitions may take additional input parameters, and may impose guard conditions on the values of both inputs and registers. Additionally, transitions may produce observable outputs and update the data state by evaluating arithmetic functions over inputs and registers. As defined in \cite{foster2018}, an EFSM is a tuple, $(S, s_0, T)$ where \begin{where} \item [$S$] is a finite non-empty set of states. \item [$s_0 \in S$]is the initial state. \item [$T$] is the transition matrix $T:(S \times S) \to \mathcal{P}(L \times \mathbb{N} \times G \times F \times U)$ with rows representing origin states and columns representing destination states. \end{where} In $T$ \begin{where} \item [$L$] is a finite set of transition labels \item [$\mathbb{N}$] gives the transition \emph{arity} (the number of input parameters), which may be zero. \item [$G$] is a finite set of Boolean guard functions $G:(I \times R) \to \mathbb{B}$. \item [$F$] is a finite set of \emph{output functions} $F:(I \times R) \to O$. \item [$U$] is a finite set of \emph{update functions} $U:(I \times R) \to R$. \end{where} In $G$, $F$, and $U$ \begin{where} \item [$I$] is a list $[i_0, i_1, \ldots, i_{m-1}]$ of values representing the inputs of a transition, which is empty if the arity is zero. \item [$R$] is a mapping from variables $[r_0, r_1, \ldots]$, representing each register of the machine, to their values. \item [$O$] is a list $[o_0, o_1, \ldots, o_{n-1}]$ of values, which may be empty, representing the outputs of a transition. \end{where} EFSM transitions have five components: label, arity, guards, outputs, and updates. Transition labels are strings, and the arities natural numbers. Guards have a defined type of \emph{guard expression} (\texttt{gexp}) and the outputs and updates are defined using \emph{arithmetic expressions} (\texttt{aexp}). Outputs are simply a list of expressions to be evaluated. Updates are a list of pairs with the first element being the index of the register to be updated, and the second element being an arithmetic expression to be evaluated. \begin{figure} \centering \includegraphics[height=\textheight]{session_graph} \caption{The Dependency Graph of the Isabelle Theories.\label{fig:session-graph}} \end{figure} The rest of this document is automatically generated from the formalization in Isabelle/HOL, i.e., all content is checked by Isabelle. Overall, the structure of this document follows the theory dependencies (see \autoref{fig:session-graph}): \nocite{foster.ea:efsm:2018} \clearpage % \chapter{Theories} \input{session} {\small \bibliographystyle{abbrvnat} \bibliography{root} } \end{document} \endinput %%% Local Variables: %%% mode: latex %%% TeX-master: t %%% End: diff --git a/thys/Stateful_Protocol_Composition_and_Typing/document/root.tex b/thys/Stateful_Protocol_Composition_and_Typing/document/root.tex --- a/thys/Stateful_Protocol_Composition_and_Typing/document/root.tex +++ b/thys/Stateful_Protocol_Composition_and_Typing/document/root.tex @@ -1,151 +1,151 @@ \documentclass[10pt,DIV16,a4paper,abstract=true,twoside=semi,openright] {scrreprt} -\usepackage[USenglish]{babel} +\usepackage[english]{babel} \usepackage[numbers, sort&compress]{natbib} \usepackage{isabelle,isabellesym} \usepackage{booktabs} \usepackage{paralist} \usepackage{graphicx} \usepackage{amssymb} \usepackage{xspace} \usepackage{xcolor} \usepackage{hyperref} \sloppy \pagestyle{headings} \isabellestyle{default} \setcounter{tocdepth}{1} \newcommand{\ie}{i.\,e.\xspace} \newcommand{\eg}{e.\,g.\xspace} \newcommand{\thy}{\isabellecontext} \renewcommand{\isamarkupsection}[1]{% \begingroup% \def\isacharunderscore{\textunderscore}% \section{#1 (\thy)}% \def\isacharunderscore{-}% \expandafter\label{sec:\isabellecontext}% \endgroup% } \title{Stateful Protocol Composition and Typing} \author{% \href{https://www.dtu.dk/english/service/phonebook/person?id=64207}{Andreas~V.~Hess}\footnotemark[1] \and \href{https://people.compute.dtu.dk/samo/}{Sebastian~M{\"o}dersheim}\footnotemark[1] \and \href{http://www.brucker.ch/}{Achim~D.~Brucker}\footnotemark[2] } \publishers{% \footnotemark[1]~DTU Compute, Technical University of Denmark, Lyngby, Denmark\texorpdfstring{\\}{, } \texttt{\{avhe, samo\}@dtu.dk}\\[2em] % \footnotemark[2]~ Department of Computer Science, University of Exeter, Exeter, UK\texorpdfstring{\\}{, } \texttt{a.brucker@exeter.ac.uk} % } \begin{document} \maketitle \begin{abstract} \begin{quote} We provide in this AFP entry several relative soundness results for security protocols. In particular, we prove typing and compositionality results for stateful protocols (i.e., protocols with mutable state that may span several sessions), and that focuses on reachability properties. Such results are useful to simplify protocol verification by reducing it to a simpler problem: Typing results give conditions under which it is safe to verify a protocol in a typed model where only ``well-typed'' attacks can occur whereas compositionality results allow us to verify a composed protocol by only verifying the component protocols in isolation. The conditions on the protocols under which the results hold are furthermore syntactic in nature allowing for full automation. The foundation presented here is used in another entry to provide fully automated and formalized security proofs of stateful protocols. \bigskip \noindent{\textbf{Keywords:}} Security protocols, stateful protocols, relative soundness results, proof assistants, Isabelle/HOL, compositionality \end{quote} \end{abstract} \tableofcontents \cleardoublepage \chapter{Introduction} The rest of this document is automatically generated from the formalization in Isabelle/HOL, i.e., all content is checked by Isabelle. The formalization presented in this entry is described in more detail in several publications: \begin{itemize} \item The typing result (\autoref{sec:Typing{-}Result} ``Typing\_Result'') for stateless protocols, the TLS formalization (\autoref{sec:Example{-}TLS} ``Example\_TLS''), and the theories depending on those (see \autoref{fig:session-graph}) are described in~\cite{hess.ea:formalizing:2017} and~\cite[chapter 3]{hess:typing:2018}. \item The typing result for stateful protocols (\autoref{sec:Stateful{-}Typing} ``Stateful\_Typing'') and the keyserver example (\autoref{sec:Example{-}Keyserver} ``Example\_Keyserver'') are described in~\cite{hess.ea:typing:2018} and~\cite[chapter 4]{hess:typing:2018}. \item The results on parallel composition for stateless protocols (\autoref{sec:Parallel{-}Compositionality} ``Parallel\_Compositionality'') and stateful protocols (\autoref{sec:Stateful{-}Compositionality} ``Stateful\_Compositionality'') are described in~\cite{hess.ea:stateful:2018} and~\cite[chapter 5]{hess:typing:2018}. \end{itemize} Overall, the structure of this document follows the theory dependencies (see \autoref{fig:session-graph}): we start with introducing the technical preliminaries of our formalization (\autoref{cha:preliminaries}). Next, we introduce the typing results in \autoref{cha:typing} and \autoref{cha:stateful-typing}. We introduce our compositionality results in \autoref{cha:composition} and \autoref{cha:stateful-composition}. Finally, we present two example protocols \autoref{cha:examples}. \paragraph{Acknowledgments} This work was supported by the Sapere-Aude project ``Composec: Secure Composition of Distributed Systems'', grant 4184-00334B of the Danish Council for Independent Research. \clearpage \begin{figure} \centering \includegraphics[height=\textheight]{session_graph} \caption{The Dependency Graph of the Isabelle Theories.\label{fig:session-graph}} \end{figure} \clearpage % \input{session} \chapter{Preliminaries and Intruder Model} \label{cha:preliminaries} In this chapter, we introduce the formal preliminaries, including the intruder model and related lemmata. \input{Miscellaneous.tex} \input{Messages.tex} \input{More_Unification.tex} \input{Intruder_Deduction.tex} \chapter{The Typing Result for Non-Stateful Protocols} \label{cha:typing} In this chapter, we formalize and prove a typing result for ``stateless'' security protocols. This work is described in more detail in~\cite{hess.ea:formalizing:2017} and~\cite[chapter 3]{hess:typing:2018}. \input{Strands_and_Constraints.tex} \input{Lazy_Intruder.tex} \input{Typed_Model.tex} \input{Typing_Result.tex} \chapter{The Typing Result for Stateful Protocols} \label{cha:stateful-typing} In this chapter, we lift the typing result to stateful protocols. For more details, we refer the reader to~\cite{hess.ea:typing:2018} and~\cite[chapter 4]{hess:typing:2018}. \input{Stateful_Strands.tex} \input{Stateful_Typing.tex} \chapter{The Parallel Composition Result for Non-Stateful Protocols} \label{cha:composition} In this chapter, we formalize and prove a compositionality result for security protocols. This work is an extension of the work described in~\cite{hess.ea:stateful:2018} and~\cite[chapter 5]{hess:typing:2018}. \input{Labeled_Strands.tex} \input{Parallel_Compositionality.tex} \chapter{The Stateful Protocol Composition Result} \label{cha:stateful-composition} In this chapter, we extend the compositionality result to stateful security protocols. This work is an extension of the work described in~\cite{hess.ea:stateful:2018} and~\cite[chapter 5]{hess:typing:2018}. \input{Labeled_Stateful_Strands.tex} \input{Stateful_Compositionality.tex} \chapter{Examples} \label{cha:examples} In this chapter, we present two examples illustrating our results: In \autoref{sec:Example{-}TLS} we show that the TLS example from~\cite{hess.ea:formalizing:2017} is type-flaw resistant. In \autoref{sec:Example{-}Keyserver} we show that the keyserver examples from~\cite{hess.ea:typing:2018,hess.ea:stateful:2018} are also type-flaw resistant and that the steps of the composed keyserver protocol from~\cite{hess.ea:stateful:2018} satisfy our conditions for protocol composition. \input{Example_TLS.tex} \input{Example_Keyserver.tex} {\small \bibliographystyle{abbrvnat} \bibliography{root} } \end{document} %%% Local Variables: %%% mode: latex %%% TeX-master: t %%% End: diff --git a/thys/UPF_Firewall/document/root.tex b/thys/UPF_Firewall/document/root.tex --- a/thys/UPF_Firewall/document/root.tex +++ b/thys/UPF_Firewall/document/root.tex @@ -1,186 +1,186 @@ \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[USenglish]{babel} +\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}\\[1em] % \normalsize\footnotemark[2]Information Security, ETH Zurich, 8092 Zurich, Switzerland \texorpdfstring{\\}{} \normalsize\href{mailto:"Lukas Bruegger" }{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} } \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} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % % \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} % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \bibliographystyle{abbrvnat} \bibliography{root} \end{document} %%% Local Variables: %%% mode: latex %%% TeX-master: t %%% End: