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
Events
The logical denotation of an event of the execution of a security protocol.
substEv :: Equalities -> Event -> EventSource
Substitute an event according to the equalities.
substEvOrd :: Equalities -> (Event, Event) -> (Event, Event)Source
Substitute an event order according to the equalities.
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 -> BoolSource
Is the event order cyclic?
before :: EventOrder -> Event -> Event -> BoolSource
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
:: 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) -> DocSource
Render an event order in the Isar format. See isaEvent
for an
explanation of the mapping.
sptEvent :: Mapping -> Event -> DocSource
Render a fact that an event happened in security protocol theory format.
sptRawEvent :: Mapping -> Event -> DocSource
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] -> DocSource
Render an event order in security protocol theory format.