Formal Specification and Verification of Mobile Agent Data Integrity Properties: A Case Study