scyther-proof-0.3.0: Automatic generation of Isabelle/HOL correctness proofs for security protocols.




Symbolic events that we are reasoning about



data Event Source

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


Step TID RoleStep

The thread executed the role step.

Learn Message

The message was learnt by the intruder.

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.

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 -> 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.




:: 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.