Building typing invariants for security protocol in order to enable verification in an untyped model.
- data Type
- data Typing
- mscTyping :: Protocol -> Maybe Typing
- isaType :: IsarConf -> Maybe Role -> Type -> Doc
- isaOptType :: IsarConf -> Maybe Role -> Maybe Type -> Doc
- sptType :: Maybe Role -> Type -> Doc
- sptOptType :: Maybe Role -> Maybe Type -> Doc
- sptTyping :: Typing -> Doc
|NonceT Role Id|
|EncT Type Type|
|TupT Type Type|
|SymKT Type Type|
|SumT Type Type|
A type assignment for variables of several roles.
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 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.
Pretty print a type that may be a weak atomicity type.
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.
Pretty print a type that may be a weak atomicity type in the security protocol theory format.