Is it secure to derive an AES key from a MAC?
It looks like, given your adversary model, things should be secure. HMAC as a randomness extractor has been shown to be good, especially when we can assume the hash function is collision resistant. That paper also has some results which tell how you could guard against the collision resistance being broken (basically use a hash function with larger output size). If SHA-256 is broken any time soon, however, we are all in a lot of trouble, so I wouldn't be too worried about that attack.