Steve Kremer: Are ideal functionalities really ideal?

Are ideal functionalities really ideal?

Myrto Arapinis, Véronique Cortier, Hubert de Groote, Charlie Jacomme, and Steve Kremer. Are ideal functionalities really ideal?. In Proceedings of the 39th IEEE Computer Security Foundations Symposium (CSF'26), IEEE Computer Society Press, Lisbon, Portugal, July 2026.

Download

[PDF] [PDF (long version)]

Abstract

Ideal functionalities are used to study increasingly complex protocols within the Universal Composability framework. However, such functionalities are often complex themselves, making it difficult to assess whether they truly fulfill their promises. In this paper, we present four attacks on functionalities from various applications (e-voting, SMPC, anonymous lotteries, and smart metering), demonstrating that they do not capture the intuitively expected properties.
We argue that ideal functionalities should not merely be justified secure at a high level but rigorously proven to be so. To this end, we propose a methodology that combines game-based proofs and computer-aided verification: ideal functionalities can in fact be treated as protocols, and one can use traditional game-based proofs to study them, where any game-based security property proven on the functionality does transfer to any protocol that realizes it. We also propose fixed versions of the ideal functionalities we studied, and formally define the security properties they should satisfy through a game. Finally, using SQUIRREL, a proof assistant for protocol security, we formally prove that the fixed functionalities verify the specified game-based security properties.

BibTeX

@inproceedings{ACdGJK-csf26,
  abstract =	 {Ideal functionalities are used to study increasingly complex protocols within the Universal Composability framework. However, such functionalities are often complex themselves, making it difficult to assess whether they truly fulfill their promises. In this paper, we present four attacks on functionalities from various applications (e-voting, SMPC, anonymous lotteries, and smart metering), demonstrating that they do not capture the intuitively expected properties.
  \par
  We argue that ideal functionalities should not merely be justified secure at a high level but rigorously proven to be so. To this end, we propose a methodology that combines game-based proofs and computer-aided verification: ideal functionalities can in fact be treated as protocols, and one can use traditional game-based proofs to study them, where any game-based security property proven on the functionality does transfer to any protocol that realizes it. We also propose fixed versions of the ideal functionalities we studied, and formally define the security properties they should satisfy through a game. Finally, using SQUIRREL, a proof assistant for protocol security, we formally prove that the fixed functionalities verify the specified game-based security properties.},
  address =	 {Lisbon, Portugal},
  author =	 {Arapinis, Myrto and Cortier, V{\'e}ronique and de Groote, Hubert and Jacomme, Charlie and Kremer, Steve},
  booktitle =	 {{P}roceedings of the 39th IEEE Computer Security
                  Foundations Symposium (CSF'26)},
  OPTdoi = {},
  month =	 jul,
  OPTpages = {},
  publisher =	 {{IEEE} Computer Society Press},
  title =	 {Are ideal functionalities really ideal?},
  year =	 {2026},
  acronym =	 {{CSF}'26},
  nmonth =	 7,
  url =          {https://inria.hal.science/hal-05422941},
}