CoPS:

• is the unique tool that verify persistent bisimulation based security properties

• can also be used to test strong and weak bisimilarities

• has a user friendly editor with syntax color highlight, code auto-completion, and the possibility of adding comments

• allows to easily navigate (with a mouse click) from a warning or an error to another

• draws a treeview of the entire system under analysis which is useful to move on subsystems to verify/modify them

• provides a graphical rappresentation of the semantics of the analyzed system which can be saved in ps, jpg, gif, ...

          In particular:

• the systems are defined using the Security Process Algebra (SPA) which is a variation of CCS

• the user can choose the security property to be checked

• the user can also choose the underlying bisimulation algorithm, the dimension of an hash table (used to speed up the computation), the format of the generated graph, and other editor settings

• the tool is composed by a kernel module and graphical interface which are independent

• the kernel is written in standard C and can be used via command line

• the graphical interface is written in Java to be portable on every system

• the source code is available on request (or )