Simulation in the proof of unforgeability

The attacker strategy attacks three correct entities the attack is based on a black-box simulation of the attacker strategy A. A succeeds if the resulting sequences of events at the shown interface do not fulfil the requirements (with significant probability). Grey arrows are taps on connections. 

After a forgery. A stops simulating A and starts a dispute about the forgery, i.e., it inputs all the correct commands at the access points of the interest group and provides the correct connections at the connection-control access point. (And it makes no further inputs.) Before that, it may have to wait until previous transactions at those access points end availability of service guarantees that this happens. 

Availability of service also guarantees that the dispute ends. If the court s output is neither TRUE nor not cooperated , the requirement of the recipient is not fulfilled, because recipient accepts idg, m, id ) had occurred. If it is TRUE or not cooperated , the requirement of the signer is not fulfilled, because signer signs idg, m) had not occurred until the forgery and A made no further inputs since. 

Together with modus ponens, this contradicts the original requirements. 

In Section 5.2.9, it was mentioned that effectiveness of initialization need not be required explicitly for fail-stop signature schemes with special risk bearers. It is now sketched that correctness of initialization indeed implies effectiveness of initialization in these schemes. 

---