Symbolic partial model checking for security analysis

In this paper, we present a symbolic version of the Hennessy-Milner logic for expressing security properties. The models of the logic are CryptoCCS processes with their symbolic semantics. We study the model checking problem and partial model checking techniques for the logic.