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 the CADP Web site in PDF or PostScript
Contact:	Jan van Eijck CWI, P.O. Box 94079 1090 GB Amsterdam Tel: + 31 20 592 4052 E-mail: [email protected]
Further remarks:	This tool, amongst others, is described on the CADP Web site: http://cadp.inria.fr/software

Back to the CADP research tools page