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:

graph LR
    start((start)) -- "ε,ε/m#" --> pgpmsg((OpenPGP Message))
    pgpmsg -- "Literal Data,m/ε" --> literal((Literal Message))
    literal -- "ε,#/ε" --> accept((Valid))
    literal -- "Signature,o/ε" --> sig4ops((Corresponding Signature))
    sig4ops -- "Signature,o/ε" --> sig4ops
    sig4ops -- "ε,#/ε" --> accept
    pgpmsg -- "OnePassSignature,m/o" --> ops((One-Pass-Signed Message))
    ops -- "ε,ε/m" --> pgpmsg
    pgpmsg -- "Signature,m/ε" --> signed((Signed Message))
    signed -- "ε,ε/m" --> pgpmsg
    pgpmsg -- "Compressed Data,m/ε" --> comp((Compressed Message))
    comp -. "ε,ε/m" .-> pgpmsg
    comp -- "ε,#/ε" --> accept
    comp -- "Signature,o/ε" --> sig4ops
    pgpmsg -- "SKESK|PKESK,m/k" --> esks((ESKs))
    pgpmsg -- "Sym. Enc. (Int. Prot.) Data,m/ε" --> enc
    esks -- "SKESK|PKESK,k/k" --> esks
    esks -- "Sym. Enc. (Int. Prot.) Data,k/ε" --> enc((Encrypted Message))
    enc -. "ε,ε/m" .-> pgpmsg
    enc -- "ε,#/ε" --> accept
    enc -- "Signature,o/ε" --> sig4ops
    accept -- "ε,ε/ε" --> accept

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.

9.9 KiB Raw Blame History

Pushdown Automaton for the OpenPGP Message Format

9.9 KiB

Raw Blame History