F-certmail — Certified mail

F-certmail (Certified mail) is part of Channels, Agreement, Ledgers in the UC functionality encyclopedia. Status: an emerging formulation, still an active area of research.

Certified mail is the fair exchange of a message for a receipt: the recipient gets the message if and only if the sender gets a receipt. A rigorous definition exists, it is simulation-based, and it is the work of the people who invented the framework this encyclopedia’s own framework descends from. What it is not is a single ideal functionality, and the reason is structural rather than accidental — which is why this page records the absence instead of inventing a box.

The stub cited a 2000 IBM technical report as a .ps.gz. That report has a published successor, revised September 2004 and posted in 2006, and this entry cites the successor. The old link is superseded rather than dead.

Why there is no box

The definition is given as three ideal machines, not one, and which one applies depends on who is honest. Pfitzmann, Schunter and Waidner print \(\mathsf{th}_{s}\) for a correct sender only, \(\mathsf{th}_{r}\) for a correct recipient only, and \(\mathsf{th}_{sr}\) for both correct — Figures 1, 2 and 3. That is the structure convention of the reactive-simulatability model: an ideal system is a family of machines indexed by the honest set, and the security statement quantifies over the family. A UC functionality is one machine that handles every corruption pattern internally, through a corruption interface. Transcribing one of the three would be picking a corruption pattern and calling it the definition; transcribing all three would be three boxes on a page whose every sibling holds one.

And the two models are not far apart, which is what makes the mismatch worth recording rather than dismissing. The source says so itself: its approach “is nowadays better known as ‘universal composability’”. Reactive simulatability and UC are the same programme with different bookkeeping — this site has already recorded the same situation for F-SMT, whose page notes that Pfitzmann and Waidner’s secure message transmission is “an ideal system in the reactive-simulatability model, not a UC functionality”, and cites it as a parallel line of work rather than as a source. This page takes the same line, and the difference is that F-SMT had a UC box available from elsewhere and this slot does not.

A forward search found no UC functionality for certified mail. The nearest UC-framework relatives are optimistic fair exchange and the signature and certification functionalities — this site’s F-Sig and F-CERT, from Canetti’s certification paper — and none of them is certified mail, which needs the fairness the exchange is about and which a signature functionality does not provide.

What the closest printed thing is

The source’s ideal system, and it is a serious piece of work rather than a sketch: a definition covering optimistic protocols and many interleaved executions, which the paper says had no rigorous definition before it, together with a real protocol proved as secure as the ideal system, and — the reason it is worth a reader’s time even without a box here — a third-party dispute treatment, so that a receipt can be shown to a verifier who was not party to the exchange. The receipt-showing sub-protocol is its Figure 5.

What would resolve this

  1. A paper that prints a single UC functionality for certified mail, with a corruption interface rather than a family of machines indexed by the honest set. This is the ordinary route and there is no obstruction to it — the object is not resisting formulation the way F-MHF’s cost bound is; nobody appears to have done it.
  2. Decide the encyclopedia admits reactive-simulatability ideal systems, and transcribe all three machines with the indexing made explicit. That is an editorial decision about what the 104 slots hold, and it would apply to F-SMT’s neighbourhood too.

Formal artifacts

No machine-checked formalization yet, and none is possible before there is a definition to formalize.

References:

  • Pfitzmann, Schunter, and Waidner. Reactively simulatable certified mail. ePrint 2006/041, 2006 — a revision of September 2004 of a journal submission from December 2000. The closest printed thing: the ideal transaction machines \(\mathsf{th}_{s}\), \(\mathsf{th}_{r}\) and \(\mathsf{th}_{sr}\) are Figures 1–3, the sending sub-protocol Figure 4, receipt-showing Figure 5 and the sender machine Figure 6. Reactive simulatability is defined in its §5, and the paper notes that the approach “is nowadays better known as ‘universal composability’”. This supersedes the technical report this page previously cited — same authors, same work, published and fetchable.
  • Pfitzmann, Schunter, and Waidner. Provably secure certified mail. Technical Report RZ 3207 (#93253), IBM Research, Zurich, 2000. The page’s original citation, kept for the record. Superseded by the entry above.