Brzusk et al. introduced the state-separation proof technique to tame complexity in game-based security proofs. The framework allows for modular, easy to understand, and reusable proofs. It has been applied to real-world protocols, like in this paper on the security of the TLS 1.3 key schedule. Additionally, this formalism is used in Mike Rosulek's book "The Joy of Cryptography".

The framework (that I am currently learning) relies on packages as basic building blocks and defines them in a way that provides a sequential and parallel composition.

What I don't understand so far is: are the composition theorem in state-separable proofs of the same kind as in composable frameworks like UC (and variants) or Constructive cryptography.

In particular, I don't see how the framework prevents the following "bad" example. Consider the task of combining an IND-CPA secure scheme (which we can define in the framework as well) and a secure MAC to create a secure channel; clearly, we can't expect the subsystems of all variants of this composition to retain their security in an arbitrary environment.

In short: Do state-separable proofs fundamentally change the semantics of code-based game-playing to allow composability in the sense of a known composable framework? Or do they "simply" provide a better syntax for code-based games that is more modular, readable, and reusable?

  • $\begingroup$ Why can we "clearly" not expect encrypt-then-MAC to always provide a secure channel? In other words, I don't understand why your "bad" example is bad. $\endgroup$
    – Mikero
    Dec 7, 2022 at 14:37
  • $\begingroup$ @Mikero, "clearly" is a bit of a strong word. But the intent was to say, well, if we consider a generic composition of MAC, then encrypt, then we don't know what guarantees we get. On one hand, EtM is not generically secure. If we use CBC we have padding oracles but at the same time, there are secure instantiations of EtM with CBC... So to my understanding the definitions are not meant to give universal guarantees in arbitrary environments. Ohh and, nice book tbw ; ) $\endgroup$ Dec 7, 2022 at 14:44
  • $\begingroup$ But encrypt-then-MAC is generically secure. A padding oracle attack is usually on plain CBC mode without a MAC. A padding oracle attack against CBC within encrypt-then-MAC requires a Dec algorithm like "if invalid padding return error1; elsif invalid MAC return error2; else decrypt" -- and this is not the correct Dec for encrypt-then-MAC. $\endgroup$
    – Mikero
    Dec 7, 2022 at 15:37
  • $\begingroup$ arggg sorry, I goofed on the abbreviations before. I actually meant Mac-then-Encrypt... $\endgroup$ Dec 7, 2022 at 15:47
  • $\begingroup$ These bad ways of combining MAC and CPA encryption are secure or insecure, based on how you internally instantiate the MAC and encryption scheme. I don't see what it has to do with the external environment surrounding the combined scheme. $\endgroup$
    – Mikero
    Dec 7, 2022 at 18:43


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Browse other questions tagged or ask your own question.