Download HLPSL Tutorial - The AVISPA Project

CONTENTS
1
Contents
1 HLPSL Basics
3
1.1
Using the AVISPA Tool . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
3
1.2
Basic Roles . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
5
1.3
Transitions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
6
1.4
Composed Roles . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
7
2 HLPSL Examples
9
2.1
Example 1 - from Alice-Bob notation to HLPSL specification . . . . . . . . . . . .
9
2.2
Example 2 - common errors, untrusted agents, attack traces . . . . . . . . . . . .
14
2.2.1
Modelling Tips and Pitfalls . . . . . . . . . . . . . . . . . . . . . . . . . .
18
2.2.2
Discussion and Analysis Results . . . . . . . . . . . . . . . . . . . . . . . .
22
Example 3 - security goals . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
25
2.3.1
Discussion and Analysis Results . . . . . . . . . . . . . . . . . . . . . . . .
28
Example 4 - Algebraic Operators . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
2.3
2.4
3 HLPSL Tips
41
3.1
Priming Variables . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
41
3.2
Witness and Request . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
41
3.3
Secrecy . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
42
3.4
Constants and Variables . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
42
3.5
Concatenation (.) and Commas (,) . . . . . . . . . . . . . . . . . . . . . . . . . .
43
3.6
Exploring executability of your model . . . . . . . . . . . . . . . . . . . . . . . . .
43
3.7
Detecting Replay Attacks . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
44
3.8
Instantiating Sessions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
44
3.9
Function Results . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
47
3.10 Declaring Channels . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
47
4 Questions and answers about HLPSL
48
A Symbols and Keywords
49
AVISPA
HLPSL Tutorial