Proof systems for partial incorrectness logic (partial reverse Hoare logic)

TL;DR

This paper introduces two sound and relatively complete proof systems for partial incorrectness logic, enabling formal verification of systems where final states guarantee initial states, with applications in security and authentication.

Contribution

It defines the first proof systems for partial incorrectness logic, including an ordinary and a cyclic system, and proves their relative completeness.

Findings

Both proof systems are sound and relatively complete.

The cyclic proof system can be transformed into an ordinary proof.

The systems facilitate verification of security-critical systems.

Abstract

Partial incorrectness logic (partial reverse Hoare logic) has recently been introduced as a new Hoare-style logic that over-approximates the weakest pre-conditions of a program and a post-condition. It is expected to verify systems where the final state must guarantee its initial state, such as authentication, secure communication tools and digital signatures. However, the logic has only been given semantics. This paper defines two proof systems for partial incorrectness logic (partial reverse Hoare logic): ordinary and cyclic proof systems. They are sound and relatively complete. The relative completeness of our ordinary proof system is proved by showing that the weakest pre-condition of a while loop and a post-condition is its loop invariant. The relative completeness of our cyclic proof system is also proved by providing a way to transform any cyclic proof into an ordinary proof.