[isabelle-dev] isatest ssh

Tjark Weber webertj at in.tum.de
Sun Nov 25 17:06:55 CET 2012

On Sun, 2012-11-25 at 00:00 +0000, Gerwin Klein wrote:
> On 20/11/2012, at 11:23 PM, Makarius <makarius at sketis.net> wrote:
> >  StrictHostKeyChecking no
> >  UserKnownHostsFile=/dev/null
> >
> > Maybe it helps in other situations, too.  Or maybe there is an ssh expert saying that this is really really bad.
> ssh does check these keys for a reason, it is now easy for another host
> to pretend to be one of the servers isatest wants to access. On the
> other hand, it's unclear what an attacker would gain from having
> isatest run a large isabelle session. There are easier ways to do that
> ;-)

If isatest used password-based authentication, the attacker could
obtain the password to log in to the original server, where he could do
anything isatest could do. With public-key authentication, the attacker
can merely generate unexpected responses to isatest's commands.

I don't know much about isatest or why these host keys keep changing.
A more principled approach (if possible) would be for these hosts to
somehow make their keys known to isatest via an authenticated channel.

Best regards,

More information about the isabelle-dev mailing list