v0.3.0
Additional ProVerif modeling for the threats captured in the threat model:
- pkd_composed_threats.pv verifies that Fireproof Actors cannot have their keys replaced, even with Richard, Yvonne, and Grace.
- pkd_concurrency.pv models concurrency scenarios (multiple initial AddKey -> first wins; BurnDown then AddKey racing is an open risk; if Fireproof beats BurnDown in a race, then the BurnDown is rejected)
- pkd_crypto_shredding.pv models that, after a key is wiped, the attribute is unrecoverable
- pkd_http_signatures.pv models HTTP Message Signature (RFC 9421) correctness, including attacks where the actor field in a Protocol Message disagrees with the HTTP Signature actor.
- pkd_message_uniqueness.pv models the requirement that the PKD protocol messages MUST be unique.
- pkd_totp_protocol.pv models our use of TOTP (Time-based One-Time Passwords).
- pkd_witness_consensus.pv models witness cosignatures.
Full Changelog: v0.2.1...v0.3.0