Formal Verification of an Implementation of the Roughtime Server

Formal verification has been used in the past few decades to prove correctness of programs. This thesis provides a verification of a simpler implementation of Roughtime [1], a protocol that consists of securely querying the current time via a client-server interaction. The tool that was used is Bedr...

Full description

Bibliographic Details
Main Author: Altamirano, Christian
Other Authors: Chlipala, Adam
Format: Thesis
Published: Massachusetts Institute of Technology 2022
Online Access:https://hdl.handle.net/1721.1/139971