{"id":{"repo_id":"ku","oai_identifier":"oai:kuscholarworks.ku.edu:1808/37265"},"canonical_url":"https://search.dev.ndltd.org/etd/ku/oai:kuscholarworks.ku.edu:1808/37265","repository":{"repo_id":"ku","name":"University of Kansas","base_url":"https://kuscholarworks.ku.edu/server/oai/request"},"display":{"title":"Remote Attestation Protocol Verification with a Privacy Emphasis","abstract":"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.","abstract_html":"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.","abstract_has_math":false,"creators":["KLINE, PAUL I"],"institution":"University of Kansas","degree_name":null,"degree_level":null,"degree_discipline":null,"degree_department":null,"school":null,"contributors":[],"advisors":["Alexander, Perry"],"committee_chairs":[],"committee_members":[],"year":2018,"date_issued":"2018-01-01","date_published":"2018-01-01","updated_at":"2026-07-24T02:47:27Z","subjects":["Computer science","Coq","privacy","protocol","remote attestation","tpm","Verification"],"languages":["en"],"rights":["Copyright held by the author."],"rights_urls":[],"identifier_entries":[{"key":"dc:identifier.other","label":"Dc Identifier Other","values":["http://dissertations.umi.com/ku:16144"],"render_values":[{"text":"http://dissertations.umi.com/ku:16144","href":"http://dissertations.umi.com/ku:16144","code":true}]}]},"links":{"outbound_url":"https://hdl.handle.net/1808/37265","outbound_label":"Handle","outbound_source":"dc:identifier.uri"},"metadata_groups":[{"id":"people","label":"People","entries":[{"key":"dc:contributor.advisor","label":"Advisor","values":["Alexander, Perry"]},{"key":"dc:creator","label":"Author","values":["KLINE, PAUL I"]}]},{"id":"academic_context","label":"Academic Context","entries":[{"key":"dc:date.accessioned","label":"Dc Date Accessioned","values":["2026-04-14T19:01:00Z"]},{"key":"dc:date.available","label":"Dc Date Available","values":["2026-04-14T19:01:00Z"]},{"key":"dc:date.issued","label":"Date","values":["2018-01-01"]},{"key":"dc:publisher","label":"Institution","values":["University of Kansas"]},{"key":"dc:type","label":"Dc Type","values":["Thesis"]}]},{"id":"subjects_keywords","label":"Subjects and Keywords","entries":[{"key":"dc:subject","label":"Dc Subject","values":["Computer science","Coq","privacy","protocol","remote attestation","tpm","Verification"]}]},{"id":"language_rights","label":"Language and Rights","entries":[{"key":"dc:language.iso","label":"Language (ISO)","values":["en"]},{"key":"dc:rights","label":"Dc Rights","values":["Copyright held by the author."]}]},{"id":"identifiers","label":"Identifiers","entries":[{"key":"dc:identifier.other","label":"Dc Identifier Other","values":["http://dissertations.umi.com/ku:16144"]},{"key":"dc:identifier.uri","label":"Identifier URI","values":["https://hdl.handle.net/1808/37265"]}]},{"id":"additional","label":"Additional Metadata","entries":[{"key":"dc:description.abstract","label":"Abstract","values":["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."]},{"key":"dc:title","label":"Title","values":["Remote Attestation Protocol Verification with a Privacy Emphasis"]}]}],"canonical_facts":{"dc:contributor.advisor":["Alexander, Perry"],"dc:creator":["KLINE, PAUL I"],"dc:date.accessioned":["2026-04-14T19:01:00Z"],"dc:date.available":["2026-04-14T19:01:00Z"],"dc:date.issued":["2018-01-01"],"dc:description.abstract":["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."],"dc:identifier.other":["http://dissertations.umi.com/ku:16144"],"dc:identifier.uri":["https://hdl.handle.net/1808/37265"],"dc:language.iso":["en"],"dc:publisher":["University of Kansas"],"dc:rights":["Copyright held by the author."],"dc:subject":["Computer science","Coq","privacy","protocol","remote attestation","tpm","Verification"],"dc:title":["Remote Attestation Protocol Verification with a Privacy Emphasis"],"dc:type":["Thesis"]},"updated_at":"2026-07-24T02:47:27Z"}