Download now Free registration required
The DEGAS project aims at enriching standard UML-centred development environments in such a way that the developers of global applications can exploit automated formal analyses with minimal overhead. This paper presents For-LySa, an instantiation of the DEGAS approach for authentication analysis, which exploits an existing analysis tool developed for the process calculus LySa. The paper discusses what information is needed for the analysis, and how to build the UML model of an authentication protocol in such a way that the needed information can be extracted from the model. It then presents the prototype implementation and report on some promising results of its use.
- Format: PDF
- Size: 283.1 KB