Database of Research Tools Developed Using CADP

LYS Knowledge Analysis Toolset for Epistemic Verification

Organisation: CWI (THE NETHERLANDS)
Eindhoven University of Technology (THE NETHERLANDS)

Functionality: Epistemic model checking

Tools used: CADP (Construction and Analysis of Distributed Processes)
μCRL toolset
Tcl/Tk
Graphviz

Period: 2007

Description: Dynamic epistemic logic provides a framework to model communication protocols involving sensitive personal information, such as electronic voting. In this framework, action models describe information updates and PDL (Propositional Dynamic Logic) formulas express anonymity properties.

The LYS toolset allows to create action models, visualize epistemic and action models, compute the product of an epistemic model with action models, reduce the models, and model check PDL or μ-calculus formulas. Model checking relies on the EVALUATOR tool of CADP and interfacing with LYS is done through the AUT format.

More details can also be found on the LYS web page at http://www.win.tue.nl/~sorzan/lys/

Conclusions: LYS and EVALUATOR have been successfully applied to the verification of the challenging anonymity property in several case studies, such as Chaum's dining cryptographers and Fujioka-Okamota-Ohta electronic voting scheme, presented in: http://cadp.inria.fr/case-studies/07-d-lys.html

Publications: [Eijck-Orzan-07] Jan van Eijck and Simona Orzan. "Epistemic Verification of Anonymity". In Proceedings of the 2nd International Workshop on Views on Designing Complex Architectures VODCA'06 (Bertinoro, Italy), ENTCS vol. 168, pp. 159-174, Elsevier, February 2007.
Available on-line from http://www.win.tue.nl/~sorzan/papers/lys.pdf
or from our FTP site in PDF or PostScript
Contact:
Jan van Eijck
CWI, P.O. Box 94079
1090 GB Amsterdam
Tel: + 31 20 592 4052
E-mail: jve@cwi.nl



Further remarks: This tool, amongst others, is described on the CADP Web site: http://cadp.inria.fr/software


Last modified: Fri Feb 19 09:13:01 2016.


Back to the CADP research tools page