update specification and proof-of-concept implementation

[cfm]

• After Formal Analysis of Protocol #33
• Blocked on summary comparison of encryption schemes #65

Update this repository so that lumaier/securedrop-formalanalysis → the specification → (optionally: revising or replacing) the proof-of-concept implementation (i.e., sans network I/O) are all current, correct, and consistent. This includes but is not limited to:

1. Adopting @lumaier's proposed construction based on authenticated HPKE, using libraries as high-level and vetted as possible
2. Aligning both code and documentation as closely as possible with Luca’s nomenclature and notation, documenting explicitly where deviate it from it