We consider two different approaches to security issues. In the first one bisimulation equivalences (dynamic verifications) are exploited to verify non-interference security properties on a CCS-like process algebra calculus. In the second approach control flow analysis (static analysis) is applied to verify security properties in Mobile Ambient calculus. We analyze how a simple electronic commerce case study can be modeled and its integrity verified using the two techniques. The tools CoPS and BANANA are used to perform the computations. © 2004 Elsevier B.V. All rights reserved.
Braghin, C., & Piazza, C. (2004). Checking integrity via CoPS and Banana: The E-commerce case study. Electronic Notes in Theoretical Computer Science, 99, 295–317. https://doi.org/10.1016/j.entcs.2004.02.013