State-transition diagram for initializations

Formal predicates. The first predicate models that the user with identity id tries to start initialization for the signer idg in the current round. It reflects that initializations for id cannot be attempted at signer access points other than idg. The parameters ids if and N are the set of possible recipients and the message bound that this user wants. 

The next predicate represents that an interest group is in the state No init at the beginning of the current round, i.e., no attempt at an initialization has been made prior to this round  

Vide interest group Vidspi ne Idsif i ii(Idi ) VNe MessageJbounds WEAK PREVIOUS 

ALWAYS IN THE PAST -i init attempt(id, idg, idsg inip AO- 

In rounds where it is clear that one initialization for idg has already taken place (and the following predicate will only be used in such contexts), the fact that a second initialization occurs among interest group can simply be expressed by 

---

Figure 5.7. State-transition diagram for initializations. Everything refers to one interest group and one identity of a signer.

---