Events

The logical denotation of an event of the execution of a security protocol.

Constructors

Step TID RoleStep	The thread executed the role step.
Learn Message	The message was learnt by the intruder.

Instances

Eq Event
Data Event
Ord Event
Show Event
Typeable Event
Isar Event

substEv :: Equalities -> Event -> Event Source

Substitute an event according to the equalities.

substEvOrd :: Equalities -> (Event, Event) -> (Event, Event)Source

Substitute an event order according to the equalities.

evTIDs :: Event -> [TID]Source

The threads associated to an event.

evOrdTIDs :: (Event, Event) -> [TID]Source

The threads associated to an event order.

Event Order

type EventOrder = Set (Event, Event)Source

The event order induced by the trace of the reachable state we are reasoning about.

cyclic :: EventOrder -> Bool Source

Is the event order cyclic?

before :: EventOrder -> Event -> Event -> Bool Source

Must an event have happened before another one with respect to the given event order.

before evord from to holds iff the event order evord implies that the event from must have happened before the event to in the reachable state we are reasoning about.

Output

isaEvent Source

Arguments

:: IsarConf
-> Mapping	A mapping of the logical variables. The thread id to role assigment is used for resolving steps to their abbreviated notation consisting of role name plus step label.
-> Event
-> Doc

Render an event in the Isar format.

isaEventOrd :: IsarConf -> Mapping -> (Event, Event) -> Doc Source

Render an event order in the Isar format. See isaEvent for an explanation of the mapping.

sptEvent :: Mapping -> Event -> Doc Source

Render a fact that an event happened in security protocol theory format.

sptRawEvent :: Mapping -> Event -> Doc Source

Render an event in security protocol theory format without any added tagging; i.e. learned messages are rendered as is, and executed steps are rendered as a tuple of thread identifier and role step (abbreviated if possible).

sptEventOrd :: Mapping -> [Event] -> Doc Source

Render an event order in security protocol theory format.