 data Atom
 data Formula
 substAtom :: Equalities > Atom > Atom
 relabelTIDs :: [TID] > Formula > Formula
 hasQuantifiers :: Formula > Bool
 conjuncts :: Formula > [Formula]
 conjunctionToAtoms :: MonadPlus m => Formula > m [Atom]
 isTypingFormula :: Formula > Bool
 destTypingFormula :: Formula > Maybe Typing
 atomTIDs :: Atom > [TID]
 findRole :: TID > Formula > Maybe Role
 isaCompr :: IsarConf > Message > Doc
 isaUncompr :: IsarConf > Message > Doc
 sptAtom :: Mapping > Atom > Doc
 isaAtom :: IsarConf > Mapping > Atom > Doc
 isaFormula :: IsarConf > Mapping > Formula > Doc
 sptFormula :: Mapping > Formula > Doc
Data Types
A representable logical atom.
AFalse 

AEq AnyEq  An equality 
AEv Event  An event must have happened. 
AEvOrd (Event, Event)  An event order. 
ACompr Message  A compromised agent variable. 
AUncompr Message  An uncompromised agent variable. 
AHasType MVar (Maybe Type)  A claim that a variable is of the given type; Nothing stands for weaklyatomic. 
ATyping Typing  A claim that the current state of a protocol is approximated by the given typing. 
AReachable Protocol  A claim that the current state is reachable. 
A representable logical formula. Currently these are monotonic formula.
Construction
substAtom :: Equalities > Atom > AtomSource
Substitute all variables in an atom.
NOTE: A HasType
atom will only have its thread identifier substituted, but
not the whole message variable.
relabelTIDs :: [TID] > Formula > FormulaSource
Relabel quantified TIDs according to the given list of labels.
Queries
hasQuantifiers :: Formula > BoolSource
True iff the formula does contain an existential quantifier.
conjunctionToAtoms :: MonadPlus m => Formula > m [Atom]Source
Convert a formula consisting of conjunctions only to a list of atoms. Uses
fail
for error reporting.
isTypingFormula :: Formula > BoolSource
A formula is a single atom claiming welltypedness.
destTypingFormula :: Formula > Maybe TypingSource
Extract the typing from a singleton welltypedness formula.
findRole :: TID > Formula > Maybe RoleSource
Find the first conjoined thread to role equality for this thread, if there is any.
Pretty Printing
isaUncompr :: IsarConf > Message > DocSource
An uncompromised agent variable in Isar format.
sptFormula :: Mapping > Formula > DocSource
A formula in security protocol theory format.