Portability | portable |
---|---|
Maintainer | Simon Meier <iridcode@gmail.com> |
Safe Haskell | None |
Signatures for the terms and multiset rewriting rules used to model and reason about a security protocol. modulo the full Diffie-Hellman equational theory and once modulo AC.
- data Signature a = Signature {
- _sigMaudeInfo :: a
- type SignaturePure = Signature MaudeSig
- emptySignaturePure :: SignaturePure
- sigpMaudeSig :: SignaturePure :-> MaudeSig
- type SignatureWithMaude = Signature MaudeHandle
- toSignatureWithMaude :: FilePath -> SignaturePure -> IO SignatureWithMaude
- toSignaturePure :: SignatureWithMaude -> SignaturePure
- sigmMaudeHandle :: SignatureWithMaude :-> MaudeHandle
- prettySignaturePure :: HighlightDocument d => SignaturePure -> d
- prettySignatureWithMaude :: HighlightDocument d => SignatureWithMaude -> d
Signature type
A theory signature.
Signature | |
|
Pure signatures
type SignaturePure = Signature MaudeSigSource
A Signature
without an associated Maude process.
emptySignaturePure :: SignaturePureSource
The empty pure signature.
sigpMaudeSig :: SignaturePure :-> MaudeSigSource
Access the maude signature.
Using Maude to handle operations relative to a Signature
type SignatureWithMaude = Signature MaudeHandleSource
A Signature
with an associated, running Maude process.
:: FilePath | Path to Maude executable. |
-> SignaturePure | |
-> IO SignatureWithMaude |
Ensure that maude is running and configured with the current signature.
toSignaturePure :: SignatureWithMaude -> SignaturePureSource
The pure signature of a SignatureWithMaude
.
sigmMaudeHandle :: SignatureWithMaude :-> MaudeHandleSource
Access the maude handle in a signature.
Pretty-printing
prettySignaturePure :: HighlightDocument d => SignaturePure -> dSource
Pretty-print a signature with maude.
prettySignatureWithMaude :: HighlightDocument d => SignatureWithMaude -> dSource
Pretty-print a pure signature.