Regarding the general concept of pushing state out to clients and using cryptography to protect it, I agree, and further think the DOS vector you're considering isn't very attractive.
Regarding this particular implementation: it's not documented well enough to tell, is it? It does use an HMAC. It does use AES. In the few minutes I gave myself to go through the code, I can't even figure out what mode they're running AES in, though, or what order the operations are applied in. How are keys generated? What keys are shared between client and server, and what keys are held serverside?
The latter questions are irrelevant to the academic project of proving the Trickles concept, so I'm not criticizing the team. I'm just saying, there's a lot of detail you'd want to have before saying they've got things covered.
The prototype did not use AES to encrypt continuations. As you said, the details are tricky. For instance, CTR mode may well be insecure. In a stateless environment, it's quite likely that the client could trick the server into encrypting multiple plaintexts with the same counter value.
The prototype did use AES to compute and check nonces -- AES is faster than HMAC for such small input sizes.
Since the server is effectively sending encrypted data and MACs to itself, there is no need for key distribution. Only the server holds keys; the client treats the encrypted data and MACs as opaque data.
Regarding this particular implementation: it's not documented well enough to tell, is it? It does use an HMAC. It does use AES. In the few minutes I gave myself to go through the code, I can't even figure out what mode they're running AES in, though, or what order the operations are applied in. How are keys generated? What keys are shared between client and server, and what keys are held serverside?
The latter questions are irrelevant to the academic project of proving the Trickles concept, so I'm not criticizing the team. I'm just saying, there's a lot of detail you'd want to have before saying they've got things covered.