Contents Index

AnBOnP

Description

This module defines some types for the parameters and options that the AnB translators use

Synopsis

data OutputType = Internal | Pretty | AST | IF | FP | FPI | Isa | HLPSL | Amphibian data Authlevel = Strong | Weak | HWeak data AnBOptsAndPars = AnBOnP { anbfilename :: String theory :: Maybe String anboutput :: Maybe String numSess :: Maybe Int outt :: OutputType typed :: Bool iterateFP :: Int authlevel :: Authlevel }

Documentation

data OutputType

The output type of the AnB translators Constructors Internal Do we use this? Pretty Do we use this? AST Just give the abstract syntax tree (for debugging) IF standard translation to AVISPA Intermediate Format FP output for fixedpoint computation FPI iterative version of FP (for debugging) Isa output for Isabelle HLPSL not implemented Amphibian do we use this? Instances Eq OutputType Show OutputType

data Authlevel

The version of authentication considered in fixedpoint computation Constructors Strong injective agreement: actually not supported for FP Weak standard non-injective agreement HWeak default; like Weak, but ignore if there are confusions between honest agents Instances Eq Authlevel Show Authlevel

data AnBOptsAndPars

The set of options and parameters that are passed to the AnB translators Constructors AnBOnP anbfilename :: String AnB file to translate theory :: Maybe String Algebraic theory file (not supported now) anboutput :: Maybe String Output filename numSess :: Maybe Int Number of sessions (for translation to IF) outt :: OutputType Output type typed :: Bool flag for typed protocol model iterateFP :: Int used? authlevel :: Authlevel authentication model level (for FP/Isa)

Produced by Haddock version 2.6.0