Avispa User Manual
User Manual:
Open the PDF directly: View PDF
Page Count: 88
- Introduction
- User Section
- Specifying Protocols: HLPSL
- HLPSL Syntax
- a. Lexical entities.
- b. Structure of a HLPSL specification.
- c. Definition of roles.
- d. Definition of a role.
- e. Declarations in roles.
- f. Declaration of local variables.
- g. Declaration of owned variables.
- h. Declaration of constants.
- i. Initialisation of local variables.
- j. Declaration of the acceptance state.
- k. Declaration of intruder knowledge.
- l. Transitions in basic roles.
- m. Actions and reactions.
- n. Composition of roles.
- o. Instantiation of a role.
- p. Declaration of goals.
- q. Declaration of types of variables.
- r. Declaration of types of constants.
- s. Types and compound types.
- t. Stutter and non-stutter formulas.
- u. Stutter and non stutter expressions.
- v. Predefined equational theories.
- HLPSL Guidelines
- Example
- HLPSL Syntax
- Analyzing a HLPSL Specification
- Specifying Protocols: HLPSL
- Advanced User Section
- Generating an IF Specification
- Automatic Translation from HLPSL to IF
- The IF Specification Language
- a. Lexical entities.
- b. Prelude and IF files.
- c. Section for type symbols.
- d. Section for signature.
- e. Section for variables and constants declaration.
- f. Section for equations.
- g. Section for initialisation.
- h. Section for transition rules.
- i. Section for properties.
- j. Section for attack states.
- k. Section for intruder behaviour.
- IF Prelude File
- Example
- Analysing a IF Specification
- The Standard Output Format
- Generating an IF Specification
- Contributions
- HLPSL Semantics
- IF Semantics
- References