v0.5.0

What's Changed

• Update for specification v0.8 by @soatok in #9

Full Changelog: v0.4.1...v0.5.0

v0.4.1

What's Changed

• Update proofs, Duvet snapshot by @soatok in #7

Full Changelog: v0.4.0...v0.4.1

v0.4.0

What's Changed

• Update proofs by @soatok in #6

Full Changelog: v0.3.0...v0.4.0

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

v0.2.1

What's Changed

• ProVerif: Cover more of the PKD protocols by @soatok in #3

Full Changelog: v0.2.0...v0.2.1

v0.2.0

Full Changelog: v0.1.0...v0.2.0

v0.1.0

This is the initial release of the ProVerif models and Duvet verification for these implementations:

• https://github.com/fedi-e2ee/pkd-crypto
• https://github.com/fedi-e2ee/pkd-server-php
• https://github.com/fedi-e2ee/pkd-client-php