Pasture Node State Specification

Pasture [5] is a secure messaging and logging library that enables secure off-line data access on untrusted user devices by leveraging commodity trusted hardware. Pasture does not trust the application, OS, or hypervisor and even admits hardware snooping attacks, while providing two important safety properties: access-undeniability (a user cannot deny any off-line data access obtained by his device without failing an audit) and verifiable-revocation (a user who generates a verifiable proof of revocation of unaccessed data can never access that data in the future). Each node running Pasture uses its Trusted Platform Module to protect and log access to encryption keys that shield the data. Permanently forfeiting the ability to access an unused decryption key is the basis of revocation. This report presents a formal specification, written in TLA+ [7], for the actions of a Pasture node, along with the results of checking the specification using the TLC model checker. We also present a formal proof of the Pasture safety properties, which has been mechanically checked using the TLA+ proof system [2]. These results have been presented at a TLA Workshop [11]. This report also presents a formal specification and correctness proof of an optimized version of Pasture, in which the functions of two of Pasture’s Program Configuration Registers (PCRs) have been combined into one PCR. In spite of the slight change in the specification, the formal proof of correctness of optimized Pasture is almost identical to the original proof.