Scyther.Theory.Html

Converting security protocol theories to a bunch of HTML files and images.

Documentation

data GenerationInput

Input for generation process that needs to be supplied from a caller of theoryToHtml.

Constructors

GenerationInput

Fields

giHeader :: String

Arbitrary html for the header

giTime :: UTCTime

Generation time.

giSystem :: String

Description of the system we run on.

giInputFile :: FilePath

Path to input file.

giTemplate :: FilePath

Path to template index.

giOutDir :: FilePath

Path to the output directory.

giMarkup :: HtmlMarkup Doc

Document representing theory to output.

giProofScript :: FilePath -> String

A function mapping the output file name to a string representation of Isabelle/HOL certificate. The generation time will be measured as the time it takes to write this string to the output file.

giDotTool :: String

dot tool to use.

giCmdLine :: String

The command line that was used in this call to scyther-proof.

giIsabelle :: Maybe (FilePath -> IO (IO String, Maybe String))

A checking function calling isabelle with the right parameters and returning an IO function for retrieving the logfile contents and an error message in case the check didn't succeed.

theoryToHtml :: GenerationInput -> IO ()

Convert a security protocol theory to a HTML file visualizing it.

evalHtmlMarkup :: HtmlMarkup a -> a