\documentclass[conference]{IEEEtran} \IEEEoverridecommandlockouts % The preceding line is only needed to identify funding in the first footnote. If that is unneeded, please comment it out. \usepackage{cite} \usepackage{amsmath,amssymb,amsfonts} \usepackage{algorithmic} \usepackage{graphicx} \usepackage{textcomp} \usepackage{xcolor} \usepackage{amsmath, amsthm} \usepackage{xspace} \usepackage{array} \usepackage{comment} \usepackage{xcolor,color,xspace,enumerate,centernot,multirow,float,graphicx, xcolor,caption,subcaption,textcomp,pgfplots,pgf-pie,tikz,listings, comment,adjustbox,mdframed,changepage,algorithm,algorithmic} \usepackage{hyperref} \usepackage{filecontents} % \PassOptionsToPackage{hyphens}{url}\usepackage[hidelinks]{hyperref} \usepackage{xurl} \usepackage{cryptocode} % crypto \usetikzlibrary{positioning, shapes.geometric, arrows} \usepackage{xurl} %\usepackage{csvsimple} \newtheorem{definition}{Definition} \newcommand{\cnr}[1]{\textcolor{blue}{Cristina says: {#1}}} \newcommand{\mvh}[1]{\textcolor{magenta}{Max says: {#1}}} \newcommand{\jg}[1]{\textcolor{purple}{Jake says: {#1}}} \newcommand{\spin}[0]{\textsc{Spin}\xspace} \newcommand{\korg}[0]{\textsc{PANDA}\xspace} \newcommand{\promela}[0]{\textsc{Promela}\xspace} \usepackage{listings} \definecolor{commentgreen}{rgb}{0,0.5,0} \lstset{ language=Promela, basicstyle=\ttfamily\small, keywordstyle=\color{blue}, commentstyle=\color{commentgreen}, stringstyle=\color{red}, showstringspaces=false, frame=single, captionpos=b, numberstyle=\tiny\color{gray}, breaklines=true, breakatwhitespace=true, tabsize=4, aboveskip=10pt, belowskip=10pt } \newcommand{\ba}{B\"uchi Automata\xspace} % theorem stuff: \theoremstyle{plain} \newtheorem{theorem}{Theorem} \def\BibTeX{{\rm B\kern-.05em{\sc i\kern-.025em b}\kern-.08em T\kern-.1667em\lower.7ex\hbox{E}\kern-.125emX}} \begin{document} \title{\korg: An Attack Synthesis Tool\\ for Distributed Protocols\\ } %\author{\IEEEauthorblockN{Jacob Ginesin} %\IEEEauthorblockA{\textit{Northeastern University}} %\and %\IEEEauthorblockN{Max von Hippel} %\IEEEauthorblockA{\textit{Northeastern University}} %\and %\IEEEauthorblockN{Cristina Nita-Rotaru} %\IEEEauthorblockA{\textit{Northeastern University}} %} \maketitle \begin{abstract} \input{sections/abstract} \end{abstract} \begin{IEEEkeywords} Protocols, Attack Synthesis, Denial of Service, Model Checking \end{IEEEkeywords} \section{Introduction} \label{sec:introduction} \input{sections/introduction} \section{\korg Architecture} \label{sec:design} \input{sections/design} %\section{Attacker Model Gadgets} %\label{sec:usage_attacker_models} %\input{sections/attacker_models} \section{Case Studies} \label{sec:case_studies} \input{sections/case_studies} \section{Conclusion} \label{sec:conclusion} \input{sections/conclusion} \bibliographystyle{IEEEtran} \bibliography{main} %\section{Appendix}% %\label{sec:Appendix} %\input{sections/appendix} \end{document}