Subject: aside on formal methods

From: RJ Atkinson <[email-masked]>
Date: Thu, 15 May 2003 14:22:43 -0400

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
[email-masked]

---

From: Heikki Nousiainen <[email-masked]>
Date: Sat, 17 May 2003 01:48:30 +0300 (EEST)

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)

---

From: Nicolas Williams <[email-masked]>
Date: Sat, 17 May 2003 09:29:35 -0700

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

Nico

---

From: Heikki Nousiainen <[email-masked]>
Date: Sat, 17 May 2003 21:28:44 +0300 (EEST)

> Rekeying takes care of this problem.

Oh yes, the rekeying is required, but with a 64bit counter, a suitable MAC 
algorithm and a suitable cipher, we can bump up the re-keying requirement 
up to every 2^64 packets. Excessive? Maybe as for today, but modularising 
this aspect of the protocol paves way for future changes if so needed.

Here's some motivation behind the proposed change, something I should have 
included in the earlier post already:
 - modularising integrity protection of the protocol, making future 
    changes easy to incorporate
 - lifting the re-keying constraints on the MAC algorithm (e.g. 64bit 
    counter, cipher with blocksize of 256 bits => rekey after 2^64 
    packets)
 - authentication of either plaintext or ciphertext (or even both
    for that matter) at the selection of a MAC algorithm
 - complete backward compatibility with careful specification of the MAC 
    algorithms

Best regards,
 Heikki Nousiainen

> On Sat, May 17, 2003 at 01:48:30AM +0300, Heikki Nousiainen wrote:
[snip]
> > when a MAC algorithm is changed during re-keying.
[snip]

---

From: Nicolas Williams <[email-masked]>
Date: Sat, 17 May 2003 21:10:00 -0700

> this aspect of the protocol paves way for future changes if so needed.

I don't see anything stopping a future SSHv2 encr/mac alg set from
requiring larger sequence numbers.  I wouldn't mind sequence number
sizes being negotiable though (I take it this is what you mean by
"modularizing").

I think larger sequence numbers (e.g., 64 bits and up) are a must for
protocols that don't support rekeying; for those that do, unless
rekeying is onerous (and I don't think SSHv2 rekeking is), smaller
sequence numbers (e.g., 32 bits) are not such a bad thing.

Cheers,

Nico
--

---

From: Heikki Nousiainen <[email-masked]>
Date: Sun, 18 May 2003 08:32:49 +0300 (EEST)

> sizes being negotiable though (I take it this is what you mean by

The only thing stopping this is the section 4.4 of the transport layer 
spec. As it now stands, the spec dictates 32 bit counter and 
authenticating the plaintext. It's an artificial limitation, which, I 
think, could be lifted by defining these properties with the MAC 
algorithm [algorithm, as defined for use in secsh].

> sequence numbers (e.g., 32 bits) are not such a bad thing.

MAC is not the only part requiring rekey, but yes, with ciphers with 
bigger blocksizes, the rekeying is likely to be required for the MAC 
first.

Rekeying is not that much of a problem with the current algorithms, but it 
may be in the future. We need bigger DH groups and more expensive 
calculations for bigger keysizes. With data growing and transports 
getting faster we are likely to hit the limitation faster. Why not change 
the behaviour before it becomes a problem?

Regards,
 Heikki Nousiainen

Few corrections to my earlier post:
 - The underlying cipher doesn't know packets, so the rekeying requirement 
can't be expressed as 2^64 packets as I wrote. For 256bit block cipher, 
this should be every 2^64 blocks or with 64 bit sequence number, 2^64 packets, 
whichever comes first.
 - I mix use the term MAC algorithm with both the function and how MAC 
algorithm is specified in the spec; first occurence should be function, 
the latter two refer to how MAC is specified in the spec.

---

From: Nicolas Williams <[email-masked]>
Date: Sun, 18 May 2003 08:41:07 -0700

> authenticating the plaintext. It's an artificial limitation, which, I 

Sure, but I don't think that really stops a future SSHv2 mac/enc alg
spec from saying otherwise.

> the behaviour before it becomes a problem?

I'm not saying "don't."  I'm pointing out that I don't think the current
drafts need modifying to accomodate larger sequence numbers and so on -
unless one wishes to make those directly negotiable during initial keyex,
as opposed to indirectly by negotiation of enc/mac algs, but that would
be a an incompatible change unless it were associated with a new keyex
type, but that would mean introducing a new keyex type for GSS-API.

It will be easier to associate these features of the SSHv2 crypto system
with mac and enc alg types than to make them directly negotiable, so the
current drafts, IMO, need no changes then.

Cheers,

Nico
--