Automating Invariant Verification of Behavioral Specifications

We describe a method of automating invariant verification of behavioral specifications, which are algebraic specifications of abstract machines. The proposed method is based on fixed-point computation, which is one of the standard techniques for automatic (invariant) verification. One notable feature of the proposed method is to find and use as lemmas state predicates whose invariant proofs may (even mutually) depend on other state predicates whose invariant proofs may not be completed. Creme is a tool based on the proposed method. We also report on a case study in which Creme proves fully automatically that the NSLPK authentication protocol satisfies the secrecy property