Commit c5a24fc4 authored by Frits Vaandrager's avatar Frits Vaandrager

title page and figure 7

parent b34f19c0
......@@ -49,32 +49,33 @@ tabsize=2
\renewcommand{\shorttitle}{Inference and Verification of SSH Implementations}
\author{Joeri De Ruiter}
\affiliation{%
\institution{Radboud University Nijmegen}
}
\email{joeri@cs.ru.nl}
\author{Paul Fiter\u{a}u-Bro\c{s}tean}
\authornote{Supported by NWO project 612.001.216, Active Learning of Security Protocols (ALSEP).}
\author{Paul Fiterau-Brostean}
\affiliation{%
\institution{Radboud University Nijmegen}
}
\email{p.fiterau-brostean@science.ru.nl}
\author{Toon Laenarts}
\author{Toon Lenaerts}
\affiliation{%
\institution{Radboud University Nijmegen}
}
\email{toon.lenaerts@student.ru.nl}
\author{Erik Poll}
\affiliation{%
\institution{Radboud University Nijmegen}
}
\email{erikpoll@cs.ru.nl}
\author{Joeri de Ruiter}
\affiliation{%
\institution{Radboud University Nijmegen}
}
\email{joeri@cs.ru.nl}
\author{Frits Vaandrager}
\affiliation{%
\institution{Radboud University Nijmegen}
......@@ -87,73 +88,7 @@ tabsize=2
}
\email{patrick.verleg@student.ru.nl}
%\author{Ben Trovato}
%\authornote{Dr.~Trovato insisted his name be first.}
%\orcid{1234-5678-9012}
%\affiliation{%
% \institution{Institute for Clarity in Documentation}
% \streetaddress{P.O. Box 1212}
% \city{Dublin}
% \state{Ohio}
% \postcode{43017-6221}
%}
%\email{trovato@corporation.com}
%
%\author{G.K.M. Tobin}
%\authornote{The secretary disavows any knowledge of this author's actions.}
%\affiliation{%
% \institution{Institute for Clarity in Documentation}
% \streetaddress{P.O. Box 1212}
% \city{Dublin}
% \state{Ohio}
% \postcode{43017-6221}
%}
%\email{webmaster@marysville-ohio.com}
%
%\author{Lars Th{\o}rv{\"a}ld}
%\authornote{This author is the
% one who did all the really hard work.}
%\affiliation{%
% \institution{The Th{\o}rv{\"a}ld Group}
% \streetaddress{1 Th{\o}rv{\"a}ld Circle}
% \city{Hekla}
% \country{Iceland}}
%\email{larst@affiliation.org}
%
%\author{Lawrence P. Leipuner}
%\affiliation{
% \institution{Brookhaven Laboratories}
% \streetaddress{P.O. Box 5000}}
%\email{lleipuner@researchlabs.org}
%
%\author{Sean Fogarty}
%\affiliation{%
% \institution{NASA Ames Research Center}
% \city{Moffett Field}
% \state{California}
% \postcode{94035}}
%\email{fogartys@amesres.org}
%
%\author{Charles Palmer}
%\affiliation{%
% \institution{Palmer Research Laboratories}
% \streetaddress{8600 Datapoint Drive}
% \city{San Antonio}
% \state{Texas}
% \postcode{78229}}
%\email{cpalmer@prl.com}
%
%\author{John Smith}
%\affiliation{\institution{The Th{\o}rv{\"a}ld Group}}
%\email{jsmith@affiliation.org}
%
%\author{Julius P.~Kumquat}
%\affiliation{\institution{The Kumquat Consortium}}
%\email{jpkumquat@consortium.net}
%
%% The default list of authors is too long for headers}
\renewcommand{\shortauthors}{De Ruiter et al.}
\renewcommand{\shortauthors}{Fiter\u{a}u-Bro\c{s}tean et al.}
\begin{abstract}
We apply protocol state fuzzing on three SSH implementations to infer state machines, which
......
......@@ -48,20 +48,20 @@ This function updates the output and state variables for a given valuation of th
\begin{lstlisting}
MODULE main
VAR state : {q0, q1};
inp : {BEGIN, MSG};
out : {OK, NOK, ACK};
inp : {INIT, MSG};
ASSIGN
init(state) := q0;
next(state) := case
state = q0 & inp = INIT: q1;
state = q0 & inp = BEGIN: q1;
state = q0 & inp = MSG: q0;
state = q1 & inp = INIT: q1;
state = q1 & inp = BEGIN: q1;
state = q1 & inp = MSG: q1;
esac;
next(out) := case
state = q0 & inp = INIT: OK;
state = q0 & inp = MSG: ONOK;
state = q1 & inp = INIT: OK;
esac;
out := case
state = q0 & inp = BEGIN: OK;
state = q0 & inp = MSG: NOK;
state = q1 & inp = BEGIN: OK;
state = q1 & inp = MSG: ACK;
esac;
\end{lstlisting}
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment