System-Level Design Group

KU Institute for Information Sciences

Copland Paper Submitted

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.