Você pode fazer isso desta maneira:
Host machine1 machine2 machine3
User user
ProxyCommand ssh server nc %h %p 2>/dev/null
Você só precisa listar os hosts na linha Host , separados por espaço em branco, e pode omitir HostName se não for diferente do nome que você deu na linha Host . Consulte Várias entradas semelhantes em ssh config · U & L .
Para simplificar ainda mais, existem os curingas * e ? disponíveis com o seu significado habitual, por isso, Host machine? seria igualmente possível para o seu exemplo.