introduction.tex

\par  Attack trees are an important resource for cybersecurity researchers. However, as purely graphical models, they are laborious to build and analyze. To address this limitation, researchers have explored ways to represent them as Petri nets. Building and analyzing attack trees in the form of Petri nets remain complex tasks. To simplify the translation of attack trees into Petri nets and facilitate their analysis, we have developed a chainable Petri net, or CNET, which tracks both its initial and final places (the beginning and end points of the net) to make it easy to chain these nets together to build a large, complex net out of simple pieces. To join the simple nets together, we have developed connectives based on logical operators frequently found in attack tree models, such as sequential composition, disjunction, and conjunction. In addition, we have defined two new varieties of conjunction not currently used in attack trees: stepwise conjunction and synchronous conjunction. 
\par Attack trees provide a useful visual model with a number of advantages. Because they are fairly easy to understand, attack trees facilitate communication between professionals with different areas of expertise; such collaboration among specialists improves the quality of the security analysis. In addition, attack trees help defenders communicate with both detail and clarity, improving the quality of their end product. Attack tree models also encourage the people building them to decompose attacks into smaller steps; by helping to draw out lines of attack, these models lead to a more comprehensive view of both vulnerabilities and methods of defense. The attack tree method encourages defenders to take the attacker's view by drawing attention to the attacker's goals and the available means to achieve them, thus helping them to develop a more complete defense. Attack trees also provide good visual documentation of a team's collaborative efforts to discover and mitigate security vulnerabilities, facilitating their efforts to secure a system or resource. 
\par Given their many strengths, it is no surprise that attack trees have been a key tool for cybersecurity professionals since their development. However, as cybersecurity vulnerabilities and defenses become more complex, it becomes more difficult to use an attack tree to model them. One problem is that attack trees are generally built by hand; though there are tools to assist with the process, it remains labor-intensive, and the work required increases with the complexity of the system and its vulnerabilities. Beyond this, even in relatively simple scenarios, it is often possible to construct two attack trees that look very different, but in fact accurately capture the same vulnerabilities of the system. This problem of variation in equivalent attack trees also naturally increases as the complexity of the attack tree increases. As purely visual models, attack trees have very little formal structure to support them, and few resources to deal with the problems sketched above. However, work in the field has established a link between attack trees and Petri nets, which are both graphical and mathematical models.
\par Petri nets, first developed by Carl Adam Petri in 1962, are composed of places and transitions, with arcs connecting the two. The places model the state of the system under attack, and/or the progress of an attacker toward the goal. The transitions between the places represent actions that the attacker or the system can take to progress or impede the attack. The arcs link places to transitions, and transitions to places to show the paths through the net. Petri nets can be represented mathematically as well as graphically, allowing us to reason about them at a more abstract level while still maintaining an important common ground with attack trees. 
\par Researchers have applied category theory to Petri nets, allowing us to abstract even further, so that we can observe the most essential features of the objects under study. In stripping away the nonessential, category theory also helps us to notice important relationships between different objects that were not obvious before. By viewing Petri nets as a category, we can use abstraction and comparison to discover and prove important mathematical features that a purely graphical model like attack trees cannot reveal. In particular, we view Petri nets as monoids, a structure with objects and a binary operation that is associative and has an identity element. The places of a Petri net are a monoid with set union as the operator, and the transitions are a monoid with concatenation as the operator. Viewing Petri nets as monoids has allowed us to focus on the structure of each logical operator, so that we can build complex nets from simple parts.   
\\
In sum, our contributions include:
\begin{itemize}
  \item A chainable Petri net, or CNET, that tracks initial and final places, and start and end transitions, facilitating chaining multiple nets together.
  \item A definition of sequential composition for CNETs, with proof that it is associative but not symmetric, and keeps repetitions distinct.
  \item A definition of disjunction for CNETs, with proof that it is a coproduct. 
  \item A definition of simple conjunction for CNETs that allows for TRUE CONCURRENCY without added complexity due to the chainable feature of the CNET, with proof that it is a tensor product.
  \item A definition of synchronous conjunction for CNETs, a new type of connective that is not currently used in attack trees but would likely prove very useful in capturing steps that need to take place simultaneously, like denial-of-service attacks. Also, we include a proof that this is a product.
  \item A definition of stepwise conjunction for CNETs, where two nets must complete one at a time, in any order. This is also not currently used in attack trees, but may prove useful.
\end{itemize}
\par Ultimately, by joining in the effort to translate attack trees into mathematical/categorical models instead of simply visual models, we hope to give cybersecurity professionals a model that is just as useful as attack trees, but that additionally has properties provable with mathematical certainty, such as equivalence or hierarchy between two nets.