Verification of Observational Determinism

Organisation:	INRIA Sophia-Antipolis (FRANCE) IIT Kharagpur (INDIA) Esterel Technologies (FRANCE)
Method:	LOTOS CTL
Tools used:	CADP (Construction and Analysis of Distributed Processes)
Domain:	Security Protocols.
Period:	2006
Size:	n/a
Description:	Privacy guarantees are essential to ensure the acceptance of global computing applications, such as electronic banking or health care information systems. Observational determinism is a notion of security ensuring that changes in private or secret data are not reflected in the public data. This case study describes the application of LOTOS and CADP so as to check if a program satisfies observational determinism. The considered programming language is a parallel while-language, providing assignments, if-then-else statements, sequential and parallel composition, while-loops, and the statement ``wait(b)'', which blocks execution until condition ``b'' becomes true. A simulator for this language has been written in LOTOS. To assess the privacy guarantees of a program by model checking, two different logical characterisations of observational determinism are compared. The first characterisation uses a CTL* formula, which is close to the formal definition of observational determinism. However, this first approach leads to large models, since it requires to use a memorising transition relation that, for each transition, keeps track of the source state. The second characterisation using the polyadic modal mu-calculus might seem less intuitive, but the generated models are smaller and simpler. For both characterisations, the formulas are translated into modal mu-calculus formulae and checked with EVALUATOR.
Conclusions:	A technique to precisely verify observational determinism of parallel while programs has been implemented using CADP. As regards the model checking of security properties, the authors of [Huisman-Worah-Sunesen-06] conclude that the mu-calculus is more promising than an approach using CTL*, since the latter generates significantly larger models. As regards the reasons for using LOTOS and CADP, the authors of [Huisman-Worah-Sunesen-06] mention the following: "We choose this tool set, because of the flexibility of its model specification language LOTOS, and because of its well-established reputation."
Publications:	[Huisman-Worah-Sunesen-06] Marieke Huisman, Pratik Worah, and Kim Sunesen. "A Temporal Logic Characterisation of Observational Determinism". In Proceedings of the 19th IEEE Computer Security Foundations Workshop CSFW '06 (Venice, Italy), IEEE Computer Society Press, July 2006. Available on-line at ftp://ftp-sop.inria.fr/everest/personnel/Marieke.Huisman/obsequiv_char.pdf or from the CADP Web site in PDF or PostScript
Contact:	Marieke Huisman INRIA Sophia Antipolis 2004, route des Lucioles BP 93 06902 Sophia Antipolis FRANCE Tel: +33 (0)4 92 38 79 45 Fax: +33 (0)4 92 38 50 29 Email: Marieke.Huisman@sophia.inria.fr
Further remarks:	This case study, amongst others, is described on the CADP Web site: http://cadp.inria.fr/case-studies

Back to the CADP case studies page