3.2 Leakage

The three requirements are those the general wrapper of Section 3.5 imposes, restated because leakage is not obtained from a core in the usual way. Line 1 is the existence half of \(\opl {Guard}\); the caller half is deliberately weaker, since \(\Adv \) must be able to leak from a functionality that does not admit it as a caller, so line 2 asks only that the adversary act for the party it is reading. Line 4 is the corruption gate. Without it an honest party’s state would be readable at will, which is what line 3 of the full interface refuses everywhere else. The silencer is line 5’s, so a leakage core that places calls claims its own identity like any other core.

For an ideal functionality, \(\opl {Leak}\) is part of the specification; the messages received so far and the contents of internal lists are typical. For real protocols it can be set to leak nothing, which models no leakage at all; ideal functionalities that say which parts of the state leak are the fix.

A protocol is leakage-well-formed if every machine body is pure between invocations, all sampled randomness is drawn through \(\Frand \) and all state persisting across invocations held in \(\Fstore \) rather than on a machine tape — each exposing it through its own \(\opl {Leak}\) — and inputs and outputs leak only where the protocol routes them through an input–output functionality \(\Fio \), which is not the default. Work tapes are then never leaked, purity between invocations leaving nothing on them. No result below assumes any of this; it is the condition a realization must meet for its \(\opl {Leak}\) to mean anything, and we record it rather than use it.

\(\Zenv \) cannot call this interface, so it need not be realized for indistinguishability. It must still be simulable, since the adversary can call it.