Checking Accountability with a Prover

Today on-line services are the cornerstone of on-line applications such as e-commerce, e-government and e-health applications. However, they raise several challenges about data privacy. Accountability, which is the property of an entity of being responsible for its acts, meets some of these challenges and hence increases user´s trustworthiness in on-line applications. In this work, we propose an approach to assist the design of accountable applications. In particular, we consider an application´s abstract component design and we introduce a logical approach allowing various static verifications. This approach offers effective means to early check the design and the behavior of an application and its offered/required services. We motivate our work with a realistic use case coming from the A4Cloud project and validate our proposal with experiments using a theorem prover.