I've been advised that I should be using a key of 256 bits or more for HMAC-256.
For HMAC the key size is more or less identical to the key strength. Although you should be using 256 bits for the key to have 256 bit strength other sizes are certainly possible.
Is there any value in using sha256(key80bit) as the key for HMAC-SHA256, as it will not increase the entropy?
No. HMAC will already hash the (padded) key together with the data as part of the algorithm, see the HMAC algorithm for details. If the key is too large ten it will be pre-hashed as well, but that doesn't seem to be the case in your protocol. You could see this as SimpleKDF(OKKDF(secret)); removing the SimpleKDF, i.e. the hash doesn't make any difference.
Are other KDFs or key-stretching algorithms preferable?
Yes, it makes sense to use a password hash / PBKDF instead, as that will at least increase the workload for an adversary. Use the salt for the PBKDF otherwise rainbow table attacks may be possible. The 80 bit secret can be used as "pepper". The salt input parameter would then be e.g. 128 bit salt + 80 bit pepper.
Of course, if you have an 80 bit key from a source then you might question the source. Keys should be 128 bit minimum nowadays.
As it is so short, please find the HMAC algorithm below, copied from the RFC:
- append zeros to the end of K to create a B byte string
(e.g., if K is of length 20 bytes and B=64, then K will be
appended with 44 zero bytes 0x00)
- XOR (bitwise exclusive-OR) the B byte string computed in step
(1) with ipad
- append the stream of data 'text' to the B byte string resulting
from step (2)
- apply H to the stream generated in step (3)
- XOR (bitwise exclusive-OR) the B byte string computed in
step (1) with opad
- append the H result from step (4) to the B byte string
resulting from step (5)
- apply H to the stream generated in step (6) and output
the result
