Automating Open Bisimulation Checking for the Spi Calculus
We consider the problem of automating open bisimulation checking for the spi-calculus, an extension of the pi-calculus with cryptographic primitives. The notion of open bisimulation considered here is indexed by a (symbolic) environment, represented as bi-traces (i.e., pairs of symbolic traces), which encode the history of interaction between the intruder with the processes being checked for bisimilarity. A crucial part of the definition of this open bisimulation, that is, the notion of...[Show more]
|Collections||ANU Research Publications|
|Source:||Proceedings of IEEE Computer Security Foundations Symposium 2010|
|01_Tiu_Automating_Open_Bisimulation_2010.pdf||356.02 kB||Adobe PDF||Request a copy|
|02_Tiu_Automating_Open_Bisimulation_2010.pdf||407.58 kB||Adobe PDF||Request a copy|
Items in Open Research are protected by copyright, with all rights reserved, unless otherwise indicated.