A Formal Protocol Definition for MPCVD
The specification governs
This page explains the design of the Vultron Protocol. It is informative: the normative text is the Vultron Protocol Specification. Where this page and the specification differ, the specification governs.
This section defines the Multi-Party Coordinated Vulnerability Disclosure (MPCVD) process formally, as a Communicating Hierarchical State Machine. It is for implementers and researchers who already know the Report Management (RM), Embargo Management (EM), and Case State (CS) process models and need their exact combined definition.
Do Not Start Here
If this is your first time reading about the Vultron Protocol, we recommend that you start with Explanation. This section is heavy on formalism and is intended for readers who are already familiar with the Vultron Protocol concepts and design principles.
Pages in this section
The pages follow the order of the protocol definition, one element at a time:
- Protocol Definition — The formal definition of the Vultron protocol as a Brand-Zafiropulo communication protocol, its global state, and its number of processes.
- States — The set of states of each Participant and its start state.
- Messages — The message types that Participants exchange.
- Transitions — The transition function for sending and receiving each message type.
- Protocol Summary — A recap of the definition with summary diagrams of each process model.
Relationship to the specification
Where this section and the Vultron Protocol Specification disagree, the specification governs. The specification's state-machine sections give the normative states and transitions of each machine, starting with Report Management.
Reading path: You study how vulnerability disclosure works and want the models behind it
This page is part of Go to the formal definition.
Before this page: