This paper explains some basic concepts of the AVISPA system by re-using
some examples.

Technical
This is a serviceable introduction to AVISPA.  Of course it would
have been nicer to apply AVISPA to analyze something new.  You could
consider applying it to one of the protocols presented in the seminar
by others, or some of the recent standards, like the ones listed under
Jani Suomalainen's topic in the "Seminar material" section of the Seminar
web page.  Although it is not feasible to do this in the time remaining,
I would encourage you to try it out.


Editorial
- the reader gets the impression that the paper was written in a hurry
- lots of typos and some latex errors