Among the five safety properties we have verified, we only present one of a particular interest. This property is necessary (but not sufficient) to the authentication of the TTP by the user and we will see later that the current protocol does not satisfy it.
Four special events are required to formalize this property. Two events are related
to the verdict given by the TTP and two other events to the verdict received
by the user. A critical point is reached when the TTP decides whether or not
the registration is successful. This decision depends on the correctness of
message 3. Before the TTP sends his positive or negative acknowledgement, he
generates a special event. The TTP_REG_SUCCEEDED event corresponds to
the positive acknowledgement and the TTP_REG_FAILED event corresponds to
the negative acknowledgement. When the user receives the TTP's response, he
also reaches a critical point. Thus, he generates a USER_REG_SUCCEEDED
event or a USER_REG_FAILED according to the response received.
Property P4 can be expressed by the graph shown on figure 5. It
shows the temporal orderings that we authorize among the
TTP_REG_SUCCEEDED, TTP_REG_FAILED, USER_REG_SUCCEEDED and
USER_REG_FAILED events. In particular, a USER_REG_SUCCEEDED must
always be preceded by one TTP_REG_SUCCEEDED because, when the user
learns that he has successfully registered, the TTP must have successfully
registered him. A USER_REG_FAILED must always be preceded by at least one
TTP_REG_FAILED and no TTP_REG_SUCCEEDED because, when the user
learns that his registration failed, the TTP must have refused to register him
at least once and the TTP must not have registered that user successfully. A
USER_REG_FAILED must never follow a TTP_REG_SUCCEEDED.
