Proving security when using multiple modes in parallel should be doable with the models and CryptoVerif files prepared so far. However, I cannot spend time on it before May.
Reusing ikm elsewhere would be really inconvenient for proofs: at some point we have to assume that something is freshly random and not reused anywhere else, and I think drawing that line at the kind of root entry point, the KEM key pair, is good.
Polished alternative to #210.
Proving security when using multiple modes in parallel should be doable with the models and CryptoVerif files prepared so far. However, I cannot spend time on it before May.
Reusing
ikmelsewhere would be really inconvenient for proofs: at some point we have to assume that something is freshly random and not reused anywhere else, and I think drawing that line at the kind of root entry point, the KEM key pair, is good.Closes #210.