pgpainless/misc/OpenPGPMessageFormat.md

Pushdown Automaton for the OpenPGP Message Format

See RFC4880 §11.3. OpenPGP Messages for the formal definition.

A simulation of the automaton can be found here.

RFC4880 defines the grammar of OpenPGP messages as follows:

   OpenPGP Message :- Encrypted Message | Signed Message |
                      Compressed Message | Literal Message.

   Compressed Message :- Compressed Data Packet.

   Literal Message :- Literal Data Packet.

   ESK :- Public-Key Encrypted Session Key Packet |
          Symmetric-Key Encrypted Session Key Packet.

   ESK Sequence :- ESK | ESK Sequence, ESK.

   Encrypted Data :- Symmetrically Encrypted Data Packet |
         Symmetrically Encrypted Integrity Protected Data Packet

   Encrypted Message :- Encrypted Data | ESK Sequence, Encrypted Data.

   One-Pass Signed Message :- One-Pass Signature Packet,
               OpenPGP Message, Corresponding Signature Packet.

   Signed Message :- Signature Packet, OpenPGP Message |
               One-Pass Signed Message.

   In addition, decrypting a Symmetrically Encrypted Data packet or a
   Symmetrically Encrypted Integrity Protected Data packet as well as
   decompressing a Compressed Data packet must yield a valid OpenPGP
   Message.

This grammar can be translated into a pushdown automaton with the following graphical representation:

Formally, the PDA is defined as M = (\mathcal{Q}, \Sigma, \Upgamma, \delta, q_0, Z, F), where

• \mathcal{Q} is a finite set of states
• \Sigma is a finite set which is called the input alphabet
• \Upgamma is a finite set which is called the stack alphabet
• \delta is a finite set of \mathcal{Q}\times(\Sigma\cup\textbraceleft\epsilon\textbraceright)\times\Upgamma\times\mathcal{Q}\times\Upgamma^*, the transition relation
• q_0\in\mathcal{Q} is the start state
• Z\in\Upgamma is the initial stack symbol
• F\subseteq\mathcal{Q} is the set of accepting states

In our diagram, the initial state is q_0 = \text{start}. The initial stack symbol is Z=\epsilon (TODO: Make it #?). The set of accepting states is F=\textbraceleft\text{valid}\textbraceright. \delta is defined by the transitions shown in the graph diagram.

The input alphabet \Sigma consists of the following OpenPGP packets:

• \text{Literal Data}: Literal Data Packet
• \text{Signature}: Signature Packet
• \text{OnePassSignature}: One-Pass-Signature Packet
• \text{Compressed Data}: Compressed Data Packet
• \text{SKESK}: Symmetric-Key Encrypted Session Key Packet
• \text{PKESK}: Public-Key Encrypted Session Key Packet
• \text{Sym. Enc. Data}: Symmetrically Encrypted Data Packet
• \text{Sym. Enc. Int. Prot. Data}: Symmetrically Encrypted Integrity Protected Data Packet

Additionally, \epsilon is used to transition without reading OpenPGP packets or popping the stack.

The following stack alphabet \Upgamma is used:

• m: OpenPGP Message
• o: One-Pass-Signature packet.
• k: Encrypted Session Key
• #: Terminal for valid OpenPGP messages

Note: The standards document states, that Marker Packets shall be ignored as well. For the sake of readability, those transitions are omitted here.

The dotted line indicates a nested transition. For example, the transition (\text{Compressed Message}, \epsilon, \epsilon, \text{OpenPGP Message}, m) indicates, that the content of the Compressed Data packet itself is an OpenPGP Message.