In this proof, strategies we adopt are:
- Secure channels are modelled between Domain and CAs with rules from tamarin manual.
- Log on blockchain is modelled as a list of records, and it is append-only;
- CAs' identities are modelled as '1', '1'+'1', '1'+'1'+'1', ...; There can be unlimited number of CAs.
- The model support any combination of k CAs to issue certs, any combination of t CAs to revoke certs.
- BLMs are modelled as single trusted BLM, as we assume the blockchain is securely maintained with consensus algorithms.
To run the proof: tamarin-prover --prove BKI-proof.spthy -Dsecure1 -Dsecure2