Re: [moca] PI analysis tools

[Pierpaolo Degano <degano@xxxxxxxxxxx>]

>     I use pi calculus to model and analyse workflow(business process).
> Do you know some analysis tools based pi calculus?
>
> Thanks
>
> CHEN Zhenyu
> Mathematics Department, NJU
> Business Value Research
> IBM China Research Lab
> Tel: (86-10) 6298 6677 x 559,
> Fax: (86-10) 82899634


You may wish to have a look at http://www.imm.dtu.dk/cs_LySa/ (Mikael 
Buchholtz <mib@xxxxxxxxxx> is th e"master").

The tool implements a static analyser for LySa, a calculus that 
extends the pi-calculus with crypto primitives (similarly to spi).
We used it to check symmetric and asymmetric key protocols such as
Needham-Schroeder symmetric key, Otway-Rees, Yahalom, Andrew Secure
RPC, Needham-Schroeder asymmetric key, and Beller-Chang-Yacobi MSR.
It proved sufficient to identify several authentication (and 
security) flaws and also to find a new one in the MSR.
(References are:
Bodei, C., Buchholtz, M., Degano, P., Nielson, F. and Riis Nielson, 
H. Automatic Validation of Protocol Narration, Proc. 16th IEEE CSFW, 
Asilomar, 2003, pp. 126-140
Bodei, C., Buchholtz, M., Degano, P., Nielson, F. and Riis Nielson, 
H.,, Control Flow Analysis Can Find New Flaws Too, Proc. WITS'04 (P. 
Ryan, Ed.), Barcelona)

Enjoy! Pierpaolo
--

+++++++++++++++++++++++++++++++++++++++++++++++++++++
Prof. Pierpaolo Degano

Dipartimento di Informatica
Universita' di Pisa
via Filippo Buonarroti, 2  --  I-56127 PISA, Italia
Tel: +39 050 2212757   Fax: +39 050 2212726
e_mail: degano@xxxxxxxxxxx
http://www.di.unipi.it/~degano
_____________________________________________________

Unless unavoidable, no Word or PowerPoint attachments, please. See
http://www.fsf.org/philosophy/no-word-attachments.html

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