our models are too complex for manual inspection but trivial for NuSMV

introduction.tex

@@ -21,9 +21,10 @@ conformance to both functional and security properties.
 The properties we verify for the inferred state machines are based on
 the RFCs that specify SSH \cite{rfc4251,rfc4252,rfc4253,rfc4254}.
 These properties are formalized in LTL and verified using
-NuSMV~\cite{NuSMV2}. Manually verifying these properties would be
-difficult, as the learned models are complex.  Moreover, formalizing
-properties means we can also better assess and overcome vagueness or
+NuSMV~\cite{NuSMV2}.  
+We use a model checker since the models are too complex for manual inspection (they are trivial for NuSMV).
+Moreover, by formalizing the
+properties we can better assess and overcome vagueness or
 under-specification in the RFC standards.
 
 Model learning obtains a state machine model of a black-box system by