Describir: A Correctness Proof of a Mesh Security Architecture