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?
