[moca] The Picasso tool

[Benjamin Aziz <baziz@xxxxxxxxxxxxxx>]

Dear all,
Recently, I have completed an evaluation prototype of Picasso, a
"Pi-Calculus Analyzer for Secrecy and Security Objectives" using the
language of Ocaml.  The tool can be downloaded from the following url:
http://www.compapp.dcu.ie/~baziz/research.html

Picasso is a non uniform static analysis tool that can be employed in
analyzing a range of security properties for closed and open mobile
systems specified using the language of the pi-calculus.  A novelty
about this tool is that it is entirely based on the denotational
semantics approach where Stark's concrete domains for the pi-calculus
are safely abstracted to arrive at finite domains.  The result of
analyzing a specification is an environment that associates with each
name a set of names that can substitute that name during run time.
The current version supports two security functions, process-level leaks
and insecure communications.  However, other properties, like the
perfect firewall equation and bound communications are also easily
implementable on top of Picasso.

Regards,
--
Benjamin Aziz
School of Computer Applications,
Dublin City University,
Dublin 9,
Ireland
Telephone(Office): (00353).(1).7005618
Electronic Mail: baziz@xxxxxxxxxxxxxx
```````````````````````````````````````


  
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
The "models for mobility" mailing list     mailto:moca@xxxxxxxxxxxxxxx
 http://www-sop.inria.fr/mimosa/personnel/Davide.Sangiorgi/moca.html