KU Institute for Information Sciences
With colleagues at NSA, MITRE, and JHUAPL we submitted the first paper on Copland to POST’19. The paper describes the semantics of attestation protocol terms and correctness properties. The paper is currently udner consideration, but the Coq proofs are available on the Copland site.