Commit cc8fa071 authored by Frits Vaandrager's avatar Frits Vaandrager
Browse files

Rewrote abstract and added ref to PC member Peled

parent 94bcb64d
......@@ -14,7 +14,7 @@ rather than cryptographic flaws. Such logical flaws have occurred in
implementations of other security protocols, notably TLS, with Apple's
'goto fail' bug and the FREAK attack \cite{Beurdouche:2017}. For this
we use model learning (a.k.a.\ active automata learning)
\cite{Angluin1987Learning,Vaa17} to infer state machines of three SSH
\cite{Angluin1987Learning,PeVaYa02,Vaa17} to infer state machines of three SSH
implementations, which we then analyze by model checking for
conformance to both functional and security properties.
......
......@@ -89,11 +89,12 @@ tabsize=2
\begin{abstract}
We apply model learning on three SSH implementations to infer state machine models, which
are then verified by a model checker for functional and security properties. Our analysis showed that
all tested SSH server models satisfy the security properties. Nevertheless, we uncovered several minor standard violations.
The state machines of the implementations differ significantly, allowing them to be
effectively fingerprinted.
We apply model learning on three SSH implementations to infer state machine models, and then use model checking
to verify that these models satisfy basic security properties and conform to the RFCs. Our analysis showed that
all tested SSH server models satisfy the stated security properties. However, our analysis uncovered several standard violations.
%Frits: I would say the fingerprinting is a detail, standard violations much more important.
%The state machines of the implementations differ significantly, allowing them to be
%effectively fingerprinted.
%Various shortcomings with regards to the RFCs were found. Opening multiple channels is not properly implemented on CiscoSSH and PowerShell. OpenSSH contains a bug which can result in connection closure after rekeying in some circumstances. Both Tectia and OpenSSH implement a liberal message acceptance policy in the first phase of the protocol. Such a liberal policy is unwise in this error-prone stage.
......
......@@ -574,3 +574,13 @@ machine learning algorithms},
}
@ARTICLE{PeVaYa02,
AUTHOR = "Peled, D. and Vardi, M.Y. and Yannakakis, M.",
TITLE = "{Black Box Checking}",
JOURNAL = "Journal of Automata, Languages, and Combinatorics",
YEAR = "2002",
VOLUME = "7",
NUMBER = "2",
PAGES = "225--246"
}
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