Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Access Hoare Logic

Arnold Beckmann, Anton Setzer

TL;DR

The paper tackles the limitation of standard Hoare logic in expressing access security properties by introducing access Hoare logic (aHl), which reasons from postconditions to preconditions using triples of the form $\langle P\rangle C \langle Q\rangle$. It develops a direct calculus for aHl, proves its soundness and completeness, and connects it to classical Hoare logic through the relationship between weakest and strongest preconditions. The authors illustrate the approach with three concrete examples—electronic keys, Bitcoin scripts, and a key-list access check—to show how aHl captures necessary conditions for secure access. The work lays groundwork for formal verification of access-control properties and suggests implications for tooling and future research, including intuitionistic considerations and potential applications to smart contracts and security-sensitive code.

Abstract

Following Hoare's seminal invention, later called Hoare logic, to reason about correctness of computer programs, we advocate a related but fundamentally different approach to reason about access security of computer programs such as access control. We define the formalism, which we denote access Hoare logic, and present examples which demonstrate its usefulness and fundamental difference to Hoare logic. We prove soundness and completeness of access Hoare logic, and provide a link between access Hoare logic and standard Hoare logic.

Access Hoare Logic

TL;DR

The paper tackles the limitation of standard Hoare logic in expressing access security properties by introducing access Hoare logic (aHl), which reasons from postconditions to preconditions using triples of the form . It develops a direct calculus for aHl, proves its soundness and completeness, and connects it to classical Hoare logic through the relationship between weakest and strongest preconditions. The authors illustrate the approach with three concrete examples—electronic keys, Bitcoin scripts, and a key-list access check—to show how aHl captures necessary conditions for secure access. The work lays groundwork for formal verification of access-control properties and suggests implications for tooling and future research, including intuitionistic considerations and potential applications to smart contracts and security-sensitive code.

Abstract

Following Hoare's seminal invention, later called Hoare logic, to reason about correctness of computer programs, we advocate a related but fundamentally different approach to reason about access security of computer programs such as access control. We define the formalism, which we denote access Hoare logic, and present examples which demonstrate its usefulness and fundamental difference to Hoare logic. We prove soundness and completeness of access Hoare logic, and provide a link between access Hoare logic and standard Hoare logic.

Paper Structure

This paper contains 16 sections, 8 theorems, 10 equations, 1 figure.

Table of Contents

  1. Introduction
  2. Examples
  3. Access Security for Electronic Keys
  4. Access Security for Bitcoin
  5. Access Security for While Loops
  6. Access Hoare Triples
  7. The Calculus
  8. Axiom for empty statement
  9. Axiom scheme of assignment
  10. Consequence rule
  11. Rule of composition
  12. Conditional rule
  13. While rule
  14. Weakest and Strongest Preconditions
  15. Soundness and Completeness
  16. ...and 1 more sections

Key Result

Theorem 3.1

$\langle P\rangle\,C\,\langle Q\rangle$ is equivalent to $\{\neg P\}\,C\,\{\neg Q\}$

Figures (1)

  • Figure 1: Executing the combined unlocking and locking script

Theorems & Definitions (12)

  • Theorem 3.1
  • Remark 3.2
  • Definition 5.1: Weakest precondition for Hoare triples
  • Definition 5.2: Strongest precondition for access Hoare triples
  • Lemma 5.3
  • Lemma 5.4
  • Corollary 5.5
  • Corollary 5.6
  • Remark 5.7
  • Theorem 6.1: Soundness of aHl
  • ...and 2 more