Download ASLan++ specification and tutorial

D2.3 (update): ASLan++ specification and tutorial
5/190
List of Figures
1
2
3
4
5
6
7
8
9
10
How the Model Checker simulates the Attacker. . . . . . . . . . . . . . . . .
The Sequence Chart for the NSPK Protocol. . . . . . . . . . . . . . . . . . .
The annotated Sequence Chart for the NSPK Protocol. . . . . . . . . . . . .
The Security Goals for the NSPK Protocol. . . . . . . . . . . . . . . . . . .
Nested Entities: Environment, its Sessions and their Actors. . . . . . . . . .
Two parallel sessions – Multiple Interference Facilities. . . . . . . . . . . . .
An AVANTSSAR Model Checker found a Vulnerability in the NSPK Protocol.
The Lowe Attack on the NSPK Protocol. . . . . . . . . . . . . . . . . . . . .
Lowe’s Fix for the Vulnerability in the NSPK Protocol. . . . . . . . . . . . .
The CA Hierarchy Setup. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
FP7-ICT-2007-1
Project No. 216471
11
11
12
15
17
18
28
29
30
31