main.tex

\documentclass{article}

\usepackage{amssymb,amsmath,amsthm}
\usepackage{cmll}
\usepackage{txfonts}
\usepackage{graphicx}
\usepackage{stmaryrd}
\usepackage{todonotes}
\usepackage{mathtools}
\usepackage{amsmath}
\usepackage{mathpartir}
\usepackage{hyperref}
\usepackage{mdframed}
\usepackage[barr]{xy}
\usepackage{comment}
\usepackage{graphicx}
\usepackage[inline]{enumitem}

\setlist{noitemsep}
\newtheorem{theorem}{Theorem}
\newtheorem{lemma}[theorem]{Lemma}
\newtheorem{corollary}[theorem]{Corollary}
\newtheorem{definition}[theorem]{Definition}
\newtheorem{proposition}[theorem]{Proposition}
\newtheorem{example}[theorem]{Example}

\newcommand{\todoBA}[1]{\todo[linecolor=purple,backgroundcolor=blue!40!white,bordercolor=purple]{BA: #1}}
\newcommand{\todoHE}[1]{\todo[linecolor=black,backgroundcolor=black!40!white,bordercolor=black]{HE: #1}}

\title{Notes on Petri Nets and Attack Trees}

\author{Aubrey Bryant and Harley Eades III}

\begin{document}
\maketitle 

\begin{abstract}
  Cybersecurity professionals often use attack trees to visualize the various possible paths of attack on a resource. Such visualizations provide important tools for communication and threat analysis. However, they can quickly become complex and unwieldy, and must rely on humans for error-checking and the tracing of possible paths. We are working to translate attack trees into Petri nets, mathematical graphical models that can be analyzed and verified much more quickly and accurately. In their original form, Petri nets are constructed of places and transitions between places, with a flow relation indicating how resources can flow through the net, or what sequence of steps is needed to get from one point to another in the net. We have begun development of a chainable Petri net, which facilitates the construction of complex nets using simple logical operations already found in attack trees. Once constructed, these nets can be analyzed using the powerful tools native to the Petri net model. This will enable cybersecurity professionals to check two nets for equivalence or hierarchy, incorporate one net into another, compute possibilities under given circumstances, and complete many other tasks with greater speed and accuracy than is possible under the current model.
\end{abstract}
\section{Introduction}
\input{introduction}
\input{NotesAttackTreesPetriNets}
\section{Equational Representation of Petri Nets}
\input{PDL_for_Petri}
\section{Quantitative Analysis of Petri Nets}
\input{Quantify_Petri}
\section{Related Work}
\input{related_work}
\nocite{*}
\bibliographystyle{plain}
\bibliography{references}

\end{document}