I am working on a proof for a secure aggregation protocol in which the server aggregates values from several clients. A challenge in the proof is that the server may lie about which clients have dropped out, requiring the simulator to equivocate the encrypted values it has sent to end up with the correct output on the server side. However, in my protocol the simulator is not able to equivocate its inputs because the encryptions it sends are information-theoretically binding.
Therefore, I thought of an alternative proof based on rewinding. Instead, the simulator guesses the output that the server should arrive at before the adversary chooses what clients to drop. To check that the simulator made the correct guess, it compares its choice of output with a query to the ideal functionality that returns the sum of the honest clients' output, after the server has announced the dropped clients. The simulator only has to perform a constant number of guesses in my protocol because the input space is constant in the security parameter, and therefore the output space is bounded as well.
However, I can see one issue with this approach, but I do not have enough background in simulation-based proofs to see whether this is actually a problem. A difference in my proof strategy is that the simulator must make a query to the leakage oracle for each time it rewinds. This is different from the ideal world, in which only a single query is made to this oracle. Is this a problem, or does the rewinding allow the simulator to query the oracle multiple times?
Tldr: In a rewinding proof, are we limited to a single query to the ideal functionality or can we make one query for each rewind?
