Experiments on Formal Verification of Mobile Agent Data Integrity Properties.
Paolo Maggi, Riccardo Sisto · 2002
This paper explores the possibility of applying existing verification techniques and tools to the cryptographic mechanisms specifically designed for the protection of mobile agents from their environment, with a particular emphasis on agent data integrity. In a previous paper we explored the use of the CSPbased tools FDR and Casper. Here, instead, we present our experience with a prototype of a new verification tool based on spicalculus. The symbolic techniques employed in this new tool make it efficient enough to analyze protocol configurations larger than the ones that could be analyzed with the CSP-based tools. This made it possible to formally find attacks that did not show up in the simplified configurations previously analyzed.