Scyther.Typing

Contents

Data types
- Construction typings
- Pretty Printing

Description

Building typing invariants for security protocol in order to enable verification in an untyped model.

Synopsis

Data types

Constructors

AgentT
ConstT Id
NonceT Role Id
HashT Type
EncT Type Type
TupT Type Type
SymKT Type Type
AsymPKT Type
AsymSKT Type
KnownT RoleStep
SumT Type Type

Instances

Eq Type
Data Type
Ord Type
Show Type
Typeable Type
Isar Type

data Typing Source

A type assignment for variables of several roles.

Constructors

WeaklyAtomic
Typing (Map (Id, Role) Type)

Instances

Eq Typing
Data Typing
Ord Typing
Show Typing
Typeable Typing
Isar Typing

Construction typings

mscTyping :: Protocol -> Maybe Typing Source

Compute a typing from the message sequence chart of the protocol implicitly given by the corresponding labels.

FIXME: This is quite a hack and could be done much better: do it!

Pretty Printing

isaType :: IsarConf -> Maybe Role -> Type -> Doc Source

Pretty print a type in Isar syntax; paramatrized over the role of the variable that this type describes. This role is used for abbreviating role steps by the role_label constant symbols defined in Isabelle.

isaOptType :: IsarConf -> Maybe Role -> Maybe Type -> Doc Source

Pretty print a type that may be a weak atomicity type.

sptType :: Maybe Role -> Type -> Doc Source

Pretty print a type in security protocol theory format. If the role is given then the type describes a variable of this role. The steps of this role are abbreviated accordingly.

sptOptType :: Maybe Role -> Maybe Type -> Doc Source

Pretty print a type that may be a weak atomicity type in the security protocol theory format.

sptTyping :: Typing -> Doc Source