Abstract
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.
Original language | English |
---|---|
Number of pages | 13 |
Publication status | Published - 2000 |
Externally published | Yes |
Event | CAV Workshop on Formal Methods and Computer Security, FMCS 2000 - Chicago, United States Duration: 1 Jul 2000 → 1 Jul 2000 |
Other
Other | CAV Workshop on Formal Methods and Computer Security, FMCS 2000 |
---|---|
Abbreviated title | FMCS |
Country/Territory | United States |
City | Chicago |
Period | 1/07/00 → 1/07/00 |