Annotations

The STP process is passed its user identifier self as a process parameter and receives as input an array of identity certificates, self_cert. These certificates are indexed according to user identifier. A certificate is used as a parameter to the SelfKey function, which computes the key that the process uses to sign messages for the transaction. Messages may be signed with the Sign function.

Processes exchange certificates during the transaction initiation phase. A process that receives a certificate will use the Id and Key functions to extract the user identifier and the verification key from the certificate. The verification key is then used as a parameter to the Verify function, which validates the signature computed by the sender.

Transaction state is kept in arrays indexed according to transaction identifier. The tid datum is a process parameter that is reset each time the guarded command set is evaluated, and so will either be a random number or will be equal to the TID field of a received message. If the former, its uniqueness can be determined with the Unique function, which implicitly registers TIDs and so prevents their reuse.

The transaction state will be initialized after the transaction has been accepted, and then is updated during the subsequent exchange and termination phases. We assume that data storage is persistent and durable.

For each transaction of which the process is a member, it will maintain the following information:

t_state

the current state (initially null)

t_other

the identity of the other process

t_key

the verification key

t_data

the data sent or received

t_seq

the current message number

t_context

the current context

The context is recomputed each time data is sent or received, using the Hash function. This function computes a cryptographic message digest of the concatenation of its arguments.

The sections below annotate the code for each action in the process. Note that the temporary boolean variable valid is computed for each received message, and is true if the signature is verified and if the transaction state allows this message. Invalid messages are always dropped with no other effect.

Note as well that the signature always includes the message type, so the message body can't be used to forge a different type of message, and that the signature does not cover certificates, since these have independent integrity checks.

Action 0

In this section, a process attempts to begin a new transaction. If tid is unique and the local state for this transaction is null, the process will non-deterministically decide either to skip or to initiate the transaction.

If it decides to initiate the transaction, it selects a process (at random) along with an identity certificate corresponding to the UID of that process. It then sends a T-start message to the other process with the identity certificate.

Action 1

A process that receives a valid T-start message can decide to accept or reject the transaction. Rejected transactions are simply dropped - the transaction will also remain in the null state for the other process.

To accept the transaction, the process selects the identity certificate corresponding to the UID of the initiating process, and sends a T-accept message to the other process with that certificate. It then initializes the transaction variables and sets the state for the transaction to receiving.

Action 2

When the transaction initiator gets a valid T-accept message, it verifies that it was sent by the process to whom it sent the T-start message. If so, it also initializes the variables for that transactions, but sets its state to sending.

Action 3

A process with a transaction in the sending state will non-deterministically either send data, pass the token, commit the transaction or abort the transaction.

In order to send data, a process sends a T-data message. The current context is included with each data message to establish causality. After sending the message, the data is stored, the sequence number is updated for the next message send or receive, and the context will be updated with the new data to reflect the current state of the transaction.

When a process decides to pass the token to the other process, it sends a T-token message and sets the state of the transaction to receiving.

When a process decides to commit the transaction, it sends a T-commit and sets the state of the transaction to ready.

When a process decides to abort the transaction, it sends a T-abort message and sets the state of the transaction to aborted.

Action 4

When a process receives a valid T-data message, it discards the data if the received context is incorrect; otherwise, it stores the data and updates the sequence number for the next message send or receive.

Action 5

When a process receives a valid T-token message, it will abort the transaction if the received context is incorrect; otherwise it sets its state to sending.

Action 6

When a process receives a valid T-commit message, it will process the message according to the state of the transaction.

If the transaction is already aborted or committed, the process's original T-abort or T-commit message was probably lost. and so the process resends the appropriate message.

If the transaction is in the ready state, then the message is in response to the process's earlier commit request, and the process sets the transaction state to committed.

If the transaction is in the receiving state, then the process non-deterministically either aborts or commits the transaction, and sets the transaction state accordingly. It will only commit the transaction if the received context matches its own, but note that it does not have to do so. If it does choose to accept the commit request, it returns a T-commit message that has a null data context field. Note that by accepting the commit, it implicitly asserts that its transaction context is equal to the received context, and so there is no reason to return its own value for context.

Action 7

When a process receives a valid T-abort message for a transaction, it sets the state of that transaction to aborted.

Action 8

When a process receives a T-fault message for a transaction, it processes it according to the state of that transaction. If the transaction is active (sending or receiving), the transaction is aborted. If the transaction is in the ready state, it is waiting for a response to its commit request, and so the process resends it. Otherwise the process does nothing.