CRÈME: AN AUTOMATIC INVARIANT PROVER OF BEHAVIORAL SPECIFICATIONS
Masahiro Nakano, Kazuhiro Ogata, MASAKI NAKAMURA, Kokichi Futatsugi · International Journal of Software Engineering and Knowledge Engineering · 2007
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. The proposed method has some notable features. Among them are as follow: (1) the method finds and uses as lemmas state predicates whose invariant proofs may (even mutually) depend on other state predicates whose invariant proofs may not be completed, and (2) the method finds a counterexample showing that an abstract machine does not satisfy an invariant property if any, which does not need to make the (reachable) state space of the abstract machine finite. Crème is a tool based on the proposed method. We also report on two case studies in which (1) Crème proves fully automatically that the NSLPK authentication protocol satisfies the secrecy property and (2) Crème finds a counterexample showing that the NSPK authentication protocol does not satisfy the secrecy property.