Symbolic events that we are reasoning about
- data Event
- substEv :: Equalities -> Event -> Event
- substEvOrd :: Equalities -> (Event, Event) -> (Event, Event)
- evTIDs :: Event -> [TID]
- evOrdTIDs :: (Event, Event) -> [TID]
- type EventOrder = Set (Event, Event)
- cyclic :: EventOrder -> Bool
- before :: EventOrder -> Event -> Event -> Bool
- isaEvent :: IsarConf -> Mapping -> Event -> Doc
- isaEventOrd :: IsarConf -> Mapping -> (Event, Event) -> Doc
- sptEvent :: Mapping -> Event -> Doc
- sptRawEvent :: Mapping -> Event -> Doc
- sptEventOrd :: Mapping -> [Event] -> Doc
The logical denotation of an event of the execution of a security protocol.
|Step TID RoleStep|
The thread executed the role step.
The message was learnt by the intruder.
Substitute an event order according to the equalities.
The event order induced by the trace of the reachable state we are reasoning about.
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.
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.
Render an event in the Isar format.
Render an event order in the Isar format. See
isaEvent for an
explanation of the mapping.
Render a fact that an event happened in security protocol theory format.
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).