Portability | GHC only |
---|---|
Maintainer | Simon Meier <iridcode@gmail.com> |
Safe Haskell | None |
Wellformedness checks for intruder variants, protocol rules, and properties.
The following checks are/should be performed (FIXME: compare the list below to what is really implemented.)
- protocol rules
- no fresh names in rule. (protocol cond. 1) ==> freshNamesReport
- no Out or K facts in premises. (protocol cond. 2) ==> factReports
- no Fr, In, or K facts in conclusions. (protocol cond. 3) ==> factReports
- vars(rhs) subset of vars(lhs) u V_Pub ==> multRestrictedReport
- lhs does not contain reducible function symbols (*-restricted (a)) ==> multRestrictedReport
- rhs does not contain * (*-restricted (b)) ==> multRestrictedReport
- all facts are used with the same arity.
- fr, in, and out, facts are used with arity 1.
- fr facts are used with a variable of sort msg or sort fresh
- fresh facts of the same rule contain different variables. [TODO]
- no protocol fact uses a reserved name => [TODO] change parser to ensure this and pretty printer to show this.
- security properties
- all facts occur with the same arity in the action of some protocol rule.
- no node variable is used in a message position and vice versa.
- type WfErrorReport = [WfError]
- checkWellformedness :: OpenTheory -> WfErrorReport
- noteWellformedness :: WfErrorReport -> OpenTheory -> OpenTheory
- prettyWfErrorReport :: WfErrorReport -> Doc
Wellformedness checking
type WfErrorReport = [WfError]Source
checkWellformedness :: OpenTheory -> WfErrorReportSource
All 2-multicombinations of a list. multicombine2 :: [a] -> [(a,a)] multicombine2 xs0 = do (x,xs) zip xs0 $ tails xs0; (,) x <$ xs
Returns a list of errors, if there are any.
noteWellformedness :: WfErrorReport -> OpenTheory -> OpenTheorySource
Adds a note to the end of the theory, if it is not well-formed.