Sketch of unforgeability

Formally, these considerations are of little importance, because unforgeability (or at least an intuitively sufficient, slightly weaker version of it) seems to be a consequence of the other requirements. In this case, it is uimecessary as a separate requirement. A proof sketch follows in Section 5.4.4. 

However, if one considers signature-like schemes with accountable centres, one may forego unforgeability in favour of efficiency, see Section 5.2.3. 

A precondition is that the signer and the recipient are in the state CorrectJnit use at the beginning of this transaction. Furthermore, the recipient must be among the possible recipients according to both the input ids] gig and the corresponding initialization. 

The only exception is that authentication need not work if the message bound N has been reached. Expressing this condition in temporal. logic is probably not the most natural way, but it can be done with a flexible variable counter (i.e., counter may assume different values in different rounds — this is the opposite of a rigid variable), which is formally used to count executions of authentication. 

Effectiveness of initialization is a requirement of an interest group consisting of a signer ids d at least one recipient or court If they input consistent commands to start an initialization for ids (according to the predicate correct init start), the initialization should yield the result acc = TRUE for them all, provided they were in the state No init and are correcdy connected throughout the initialization. 

---