Unequivocal-signed-certificates
Invariant that
the certificates signed by a correct validator are unequivocal.
A correct validator signs a certificates
under conditions formalized in create-possiblep;
recall that create is the only kind of event
that generates a new certificate.
The conditions for certificate signing include the fact that
the signer does not already have a record for
a certificate with the same author and round:
in other words, in order for the new certificate to be created,
and thus be added to the set of certificates signed by the signer,
the signer must not have a record of the certificate's author and round.
But as proved in signer-records,
it is an invariant that each correct validator has
a record of all the certificates it has signed.
Therefore, a new certificate will be signed,
and added to the set of signed certificates,
only if it has a different author-round combination
from all the existing signed certificates,
thus preventing equivocation.
This non-equivocation property is limited to
the set of certificates signed by a single validator.
There is no quorum intersection argument needed for this:
the property comes from the internal consistency tests
performed by a correct validator when it signs certificates.
This invariant is then used to prove
the broader non-equivocation property,
which makes use of the quorum intersection argument.
Subtopics
- Not-signer-record-p-when-create-possiblep
- If create-possiblep holds,
then signer-record-p is false for its correct signers.
- Unequivocal-signed-certs-p-of-next
- Preservation of the invariant:
if the invariant holds in a system state,
it also holds in the next system state.
- Signer-record-p-when-author+round-in-signed-certs
- If a certificate with a certain author and round
can be obtained from the signed certificates of a validator,
then the validator has a record of that author and round.
- Unequivocal-signed-certs-p
- Definition of the invariant:
the set of certificates signed by each correct validator
is unequivocal.
- Unequivocal-signed-certs-p-when-init
- Establishment of the invariant:
the invariant holds in any initial system state.
- Unequivocal-signed-certs-p-of-events-next
- Preservation of the invariant by multiple transitions.
- Unequivocal-signed-certs-p-when-reachable
- The invariant holds in every reachable state.
