This article discusses the relationship between two frameworks: universal composability ( \(\mathsf{UC}\) ) and robust compilation ( RC ). In cryptography, \(\mathsf{UC}\) is a framework for the specification and analysis of cryptographic protocols with a strong compositionality guarantee: \(\mathsf{UC}\) protocols remain secure even when composed with other protocols. In programming language security, RC is a novel framework for determining secure compilation by proving whether compiled programs are as secure as their source-level counterparts no matter what target-level code they interact with. Presently, these disciplines are studied in isolation, though we argue that there is a deep connection between them and exploring this connection will benefit both research fields. This article formally proves the connection between \(\mathsf{UC}\) and RC and then it explores the benefits of this connection (focussing on perfect, rather than computational \(\mathsf{UC}\) ). For this, this article first identifies which conditions must programming languages fulfil in order to possibly attain \(\mathsf{UC}\) -like composition. Then, it proves \(\mathsf{UC}\) of both an existing and a new commitment protocol as a corollary of the related compilers attaining RC . Finally, it mechanises these proofs in DEEPSEC, obtaining symbolic guarantees that the protocol is indeed \(\mathsf{UC}\) . Our connection lays the groundwork towards a better and deeper understanding of both \(\mathsf{UC}\) and RC , and the benefits we showcase from this connection provide evidence of scalable mechanised proofs for \(\mathsf{UC}\) .

@article{paperbot2666,
  title = {Universal Composability Is Robust Compilation},
  author = {Marco Patrignani and Robert Künnemann and Riad S. Wahby and Ethan Cecchetti},
  journal = {ACM Transactions on Programming Languages and Systems},
  volume = {46},
  number = {4},
  year = {2024},
  doi = {10.1145/3698234}
}