Remote Attestation Protocol Verification with a Privacy Emphasis

Remote attestation is innately challenging and wrought with auxiliary challenges. Even determining what information to request can be a challenge. In cases when a presumptuous request is denied, mutual trust can be built incrementally to achieve the same result. All the while, we must 1) Respect our own privacy policy not revealing more than necessary; 2) Respond to counter-attestation requests to build trust slowly; 3) Avoid Measurement Deadlock situations by handling cycles. In addition to these guidelines, there are basic properties of a remote attestation procedure that should be verified. One such property is ensuring parties send and receive messages harmoniously. Using the theorem prover Coq we explore designing, modeling, and verifying a mutual remote attestation procedure via an imperative protocol language that supports dynamically generating execution steps to perform a mutually agreeable attestation protocol from nothing other than a party’s initial privacy policy.

Grantor dc:publisher

University of Kansas

Year dc:date.issued

2018

Author dc:creator

• KLINE, PAUL I

Advisor dc:contributor.advisor

• Alexander, Perry

• Computer science
• Coq
• privacy
• protocol
• remote attestation
• tpm
• Verification

Statement dc:rights

• Copyright held by the author.

Language dc:language.iso

en

Dc Identifier Other

http://dissertations.umi.com/ku:16144

OAI identifier oai:identifier

oai:kuscholarworks.ku.edu:1808/37265