Capability-Passing Processes

AbstractCapability-passing processes model global applications in a way that decouples the global agreement aspects of protocols from the details of how the communications are actually made. It relies on a restricted API or programming language and on the exchange of digital certificates representing capabilities to ensure that participants are faithful to a protocol and that outsiders cannot interfere. At the specification level, protocols are reasoned about independently of the underlying communication, using a process calculus with an abstraction of logs to isolate the remote state required for such protocols. At the implementation level, protocol steps no longer perform global communication; instead capabilities are used to transmit evidence of remote state, which in turn are used to authorize local log changes (corresponding to protocol steps). In this way, an API for global agreement protocols is defined independently of the underlying communication system