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

[Nicolas Williams <Nicolas.Williams%sun.com@localhost>]

It is bad to let sequence numbers wrap around while using the same key.
Rekeying takes care of this problem.

Nico

On Sat, May 17, 2003 at 01:48:30AM +0300, Heikki Nousiainen wrote:
> 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
> 
> 
>