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 environ

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.