PCP — Proof-Carrying Payloads

Proof-Carrying Payloads (PCP) is an end-to-end authorization overlay for Pub/Sub Messaging systems that moves both data protection and authorization from the broker to the clients. PCP is broker-agnostic and deploys as a wrapper around an existing pub/sub system, without modifying the broker. In PCP, each message is carried inside a cryptographic envelope that combine encryption with succinct authorization proofs. This proof is a succinct zero-knowledge proof that the publisher holds a valid write credential. Subscribers verify that a publisher was authorized to write to the target topic before attempting decryption, while read authorization is enforced cryptographically. PCP further introduces a two-tier authorization revocation mechanism: one tier revokes publishers, and the other revokes subscribers.

This repository is the supplementary material of the paper:

Proof-Carrying Payloads: End-to-End Authorization for Pub/Sub Messaging.

The paper presents the design of PCP together with a formal analysis of its security.

This repository contains:

• The Tamarin model and lemma used for the security analysis in the symbolic model (formal/);

How to replicate the results of the paper

The formal/ directory contains everything needed to reproduce the symbolic analysis of Section 6 of the paper.

See formal/README.md for detailed instructions, expected output, and troubleshooting.

Project structure

Directory	Contents
formal/	Tamarin model of PCP

License

This software is a research prototype. The Tamarin model is release under the MIT license.