Scyther.Protocol

Security protocol represented as a set of roles which are sequences of send and receive steps.

Types

newtype Id

An identifier.

Constructors

Id

Fields

getId :: String

Instances

Eq Id

Data Id

Ord Id

Show Id

Typeable Id

Isar Id

data Pattern

A message pattern.

Constructors

PConst Id

A global constant.

PFresh Id

A message to be freshly generated.

PAVar Id

An agent variable.

PMVar Id

A message variable.

PHash Pattern

Hashing

PTup Pattern Pattern

Pairing

PEnc Pattern Pattern

Symmetric or asymmetric encryption (depent on the key).

PSign Pattern Pattern

A signature to be verified with the given key.

PSymK Pattern Pattern

A long-term unidirectional symmetric key.

PShrK Pattern Pattern

A long-term bi-directional symmetric key.

PAsymPK Pattern

A long-term public key.

PAsymSK Pattern

A long-term private key

Instances

Eq Pattern

Data Pattern

Ord Pattern

Show Pattern

Typeable Pattern

Isar Pattern

newtype Label

A label of a role step.

Constructors

Label

Fields

getLabel :: String

Instances

Eq Label

Data Label

Ord Label

Show Label

Typeable Label

Isar Label

data RoleStep

A role step.

Constructors

Send Label Pattern

A send step.

Recv Label Pattern

A receive step.

Instances

Eq RoleStep

Data RoleStep

Ord RoleStep

Show RoleStep

Typeable RoleStep

Isar RoleStep

data Role

A role of a protocol. Its name has no operational meaning, but is carried along to allow for human readable printing.

Constructors

Role

Fields

roleName :: String

roleSteps :: [RoleStep]

Instances

Eq Role

Data Role

Ord Role

Show Role

Typeable Role

Isar Role

data Protocol

A protocol. As for roles, its name has no operational meaning, but is carried along to allow for human readable printing.

Constructors

Protocol

Fields

protoName :: String

protoRoles :: [Role]

Instances

Eq Protocol

Data Protocol

Ord Protocol

Show Protocol

Typeable Protocol

Isar Protocol

type RoleStepOrder = [((RoleStep, Role), (RoleStep, Role))]

An order relation on role steps of a role.

Queries

Patterns

patFMV :: Pattern -> Set Id

Free message variables of a pattern.

patFAV :: Pattern -> Set Id

Free agent variables of a pattern.

subpatterns :: Pattern -> Set Pattern

Pattern subterms.

patternparts :: Pattern -> Set Pattern

Accessible pattern subterms.

splitpatterns :: Pattern -> Set Pattern

Splitting top-level pairs.

Role Steps

stepPat :: RoleStep -> Pattern

Pattern of of a role step

stepLabel :: RoleStep -> String

The string label of a role step.

stepFMV :: RoleStep -> Set Id

Frees message variables of a role step.

stepFAV :: RoleStep -> Set Id

Frees agent variables of a role step.

Roles

roleFMV :: Role -> Set Id

Free message variables of a role.

roleFAV :: Role -> Set Id

Free agent variables of a role.

lookupRoleStep :: String -> Role -> Maybe RoleStep

Find a role step in a role according to its label.

wfRole :: Role -> [ProtoIllformedness]

Check if a role is well-formed; i.e., all steps are distinct, no message variable is sent before it is received, and patterns do not contain long-term-keys in accessible positions.

roleOrd :: Role -> RoleStepOrder

The order of role steps as they are given in the role.

Protocols

lookupRole :: String -> Protocol -> Maybe Role

Find a role in a protocol according to its name.

stateLocale :: Protocol -> String

The name of the locale assuming a reachable state of the given protocol.

restrictedStateLocale :: Protocol -> String

The name of the locale assuming a reachable state satisfying the axioms of the theory.

weakAtomicityLocale :: Protocol -> String

The name of the locale assuming weak atomicity of the given protocol.

weakAtomicityInvariant :: Protocol -> String

The name of the weak atomicity type invariant of the given protocol.

labelOrd :: Protocol -> RoleStepOrder

The order of role steps in the protocol such that every send step is occurs before every receive step having the same label.

protoOrd :: Protocol -> RoleStepOrder

The combination of all role orders and the label order of the protocol.

Wellformedness

data ProtoIllformedness

Instances

Eq ProtoIllformedness

Ord ProtoIllformedness

Show ProtoIllformedness

wfProto :: Protocol -> [ProtoIllformedness]

Check if a protocol is well-formed; i.e., all roles are well-formed.

sptProtoIllformedness :: ProtoIllformedness -> Doc

Pretty print a protocol ill-formedness.

Output

isaRoleStep :: IsarConf -> Maybe Role -> RoleStep -> Doc

Pretty print a rolestep in ISAR format. If a role is given, then the label of the role step in this role is used to abbreviate the step name.

sptId :: Id -> Doc

sptLabel :: Label -> Doc

sptPattern :: Pattern -> Doc

sptRoleStep :: Maybe Role -> RoleStep -> Doc

Pretty print a rolestep. If a role is given, then the label of the role step in this role is used to abbreviate the step name.

sptRole :: Role -> Doc

Pretty print a role in SP theory format.

sptProtocol :: Protocol -> Doc

Pretty print a protocol in SP theory format.