SSH paper and a possible transport layer extension [was: aside on formal methods]

[Heikki Nousiainen <htn%sumu.org@localhost>]

I found one paper on discussing the security of SSH, weakness with the 
CBC encryption modes and proofs of security in with CTR modes:
Bellare, M., Kohno, T. adn Namprempre, C.
"Authenticated Encryption in SSH: Provably Fixing the SSH Binary Packet 
Protocol"

The attack presented in the paper against CBC mode encryption in SSH is, 
in my understanding, thwarted with inclusion of SSH_MSG_IGNORE packets as 
described in 11.1.1. An attacker has no knowledge of IV of the packets in 
which he can insert data, if the chapter is followed.


The paper raises a question about the length of the sequence number used
in conjunction with MACs and the possibilty of using encrypt-then-mac to 
check the authenticity of the ciphertext. Now, as far as I see, both of 
these limitations could be lifted by defining the size and the use of 
sequence number and the order in which the MAC is applied as properties 
of the selected MAC algorithm (similiar of the mode of operation for the 
ciphers). Backward compatibility with the current implementations could 
be maintained by careful selection of the initial counter values even 
when a MAC algorithm is changed during re-keying.

I don't want to delay the drafts for this, but if there's an interest on 
this in the WG, maybe we can come up with an extension draft.

Thoughts, anyone?

 - Heikki Nousiainen


Examples:

hmac-sha1

Initial sequence number is  number-of-sent-packets modulo 2^32. Sequence 
number, 32 bit unsigned integer, is incremented for each packet and wraps 
around to zero after reaching 2^32-1. MAC is calculated as 
MAC = HMACsha1_K(sequence_number || unencrypted_packet)


hmac-sha2-64_bit_sequence-encrypt_then_authenticate

Initial sequence number is  number-of-sent-packets modulo 2^32. Sequence 
number, 64 bit unsigned integer, is incremented for each packet and wraps 
around to zero after reaching 2^64-1. MAC is caclulated as
MAC = HMACsha2_K(sequence_number || encrypted_packet)


On Thu, 15 May 2003, RJ Atkinson wrote:
> 
> 	Putting the practical questions of document editing aside
> for the moment, the length of the discussion on Security
> Considerations and the informal nature of that discussion
> are a bit troubling to me.  It makes one wonder whether the SSH
> spec really did get all the pieces right -- and, if it did,
> whether it did so by accident.
> 
> 	It would be pleasant and helpful if there some more formal
> analysis of the SSH protocol performed -- and published.  The
> first step would probably to try to come up with a formal
> specification of the protocol in some appropriate logic.
> 
> 	If there are any academic folks on this list, please consider
> whether such formal methods work might be a reasonable research topic
> to undertake.
> 
> IMHO,
> 
> Ran
> rja%extremenetworks.com@localhost