[Avispa-users] arguments pour choisir AVISPA

[Ben Smyth]

Bonjour,

My french is no good, so I will try to write in basic English.

You need to use the best tool (program) for the job (task). I could not 
find anything about CASPER or EVA, do you have the web address?

Here is my argument for using ProVerif in favour of AVISPA and CAPSL. My 
goals are: prove that a state is unreachable (secrecy) and demonstrate 
privacy using observational equivalence. I need to be able to define 
equations. (this is taken straight from my dissertation, so probably 
isn't basic english. Its in LaTeX format)

CAPSL is unsuitable since it can only model authentication and 
key-exchange. Similarly AVISPA supports only authentication and secrecy. 
Although in theory it is possible to define one's own rules using 
AVISPA's Intermediate Format (IF) language~\cite{AVISPA03} - which would 
permit the modeling of further requirements - in reality such usage is 
unsupported\footnotemark. ProVerif permits the verification of privacy 
using observational equivalence. However, its ability is not complete 
and thus it is commonly necessary to complete a proof by hand. Although 
not perfect ProVerif is the only tool which meets the demands of the 
analysis.

\footnotetext{Sebastian M\"{o}dersheim has since made claims that 
AVISPA's \emph{On-the-Fly Model-Checker} (OFMC) back-end is now capable 
(February, 2006) of handling user defined algebraic expressions. At the 
time of analysis support was classified as beta and it was therefore 
decided to utilise a tool which is known to provide the necessary 
functionality.}


au revior,

Ben


chikh omar wrote:
> Bonjour,
>   
>   Quelles sont les arguments qui peut convaincre les validateurs de  choisir AVISPA comme outils de validation formelle et non pas un autre  outils comme CASPER ou EVA ...?
>   
>   y a t-il de documentation qui explique les arguments de choisir AVISPA. ?
>   
>   Cordialement
>   Omar
>   
> 		
> ---------------------------------
>  Nouveau : téléphonez moins cher avec Yahoo! Messenger ! Découvez les tarifs exceptionnels pour appeler la France et l'international.Téléchargez la version beta.
> 
> 
> ------------------------------------------------------------------------
> 
> _______________________________________________
> Avispa-users mailing list
> Avispa-users at avispa-project.org
> http://www.avispa-project.org/mailman/listinfo/avispa-users