Appendix (proof of protocol security)
We consider the licenses for a single software product.
Definition 1:
A key CK has a valid license if the private part of the
key CK is unerased, and there is a card certificate signed by
PMK and issued to the public part of CK, and a
certificate chain:
license certificate signed by PMK to CK0,
a delegation certificate signed by CK0
to CK1,
a delegation certificate signed by CK1
to CK2,
···
a delegation certificate signed by CKk-1
to CKk
such that CKk = CK. []
This forms a valid license because the verifier checks for these
conditions before allowing the use of the software. It is possible
that k=0, i.e. there are no delegation certificates. We ignore the
check for the other card certificates (of CK0 ... CKk-1) and
for the production dates because they have effect only if some other
assumption is broken.
Assumption 1:
PMK only issues license and card certificates to authentic card keys.
An authentic card key only issues delegation certificates to
keys with a card certificate. []
Assumption 2:
For every authentic card key CK, exactly one of the following holds:
- CK has signed no delegation certificates.
- CK has signed exactly one delegation certificate and
the private key CK has been erased. []
The second assumption follows from the policy of erasing the private
key immediately after signing a delegation certificate.
Proposition 1:
The number of keys with valid licenses is at most equal to the number
license certificates signed by PMK. []
Proof:
The subjects of license certificates (CK0) are
always authentic card keys. An authentic card key only delegates to a
key with card certificate and such keys are authentic card keys
(Ass. 1). Consequently, all keys in the chains starting from license
certificates are authentic card keys. The authentic card keys delegate
to at most one other key and a key that has delegated is itself erased
(Ass. 2). Thus, the certificate chains starting from license
certificates do not branch and only the last key in a chain can be
unerased.
If there would be more keys with valid licenses than license
certificates, there should be some two valid licenses whose
corresponding certificate chains (Def. 1) begin with the same license
certificate but end in two different unerased keys. However, this is
not possible since the chains do not branch and only the
maximal-length chains end in unerased keys.