Are ideal functionalities really ideal?

Are ideal functionalities really ideal?. Myrto Arapinis, Véronique Cortier, Hubert de Groote, Charlie Jacomme, and Steve Kremer. In CSF 2026 -- 39th IEEE Computer Security Foundations Symposium, Lisbonne, Portugal, 2026.

Download

[PDF]

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{ideal-fct-CSF26,
  TITLE = {{Are ideal functionalities really ideal?}},
  AUTHOR = {Arapinis, Myrto and Cortier, V{\'e}ronique and de Groote, Hubert and Jacomme, Charlie and Kremer, Steve},
  BOOKTITLE = {{CSF 2026 -- 39th IEEE Computer Security Foundations Symposium}},
  ADDRESS = {Lisbonne, Portugal},
  YEAR = {2026},
  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.},
}