Checking Integrity via CoPS and Banana: the E-Commerce Case Study

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