This paper proposes a preliminary framework in which protocols, expressed in a dialect of the spi-calculus, can be verified using model checking algorithms. In particular we define a formal semantics for a dialect of the spi-calculus based on labeled transition systems in such a way that the model checking environment developed by Clarke Marrero and Jha, can be re-used. Recently this environment has been extended with both a first order linear temporal logic, used to specify security properties, and partial order reduction techniques. These two new results make our approach interesting and effective for automatic verification.
|Number of pages||13|
|Publication status||Published - 2000|
|Event||CAV Workshop on Formal Methods and Computer Security, FMCS 2000 - Chicago, United States|
Duration: 1 Jul 2000 → 1 Jul 2000
|Other||CAV Workshop on Formal Methods and Computer Security, FMCS 2000|
|Period||1/07/00 → 1/07/00|