| Portability | portable |
|---|---|
| Maintainer | Simon Meier <iridcode@gmail.com> |
| Safe Haskell | None |
Theory.Model.Signature
Contents
Description
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.
Constructors
| Signature | |
Fields
| |
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.
Arguments
| :: 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.