Theory.Tools.Wellformedness

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

1. no fresh names in rule. (protocol cond. 1) ==> freshNamesReport
2. no Out or K facts in premises. (protocol cond. 2) ==> factReports
3. no Fr, In, or K facts in conclusions. (protocol cond. 3) ==> factReports
4. vars(rhs) subset of vars(lhs) u V_Pub ==> multRestrictedReport
5. lhs does not contain reducible function symbols (*-restricted (a)) ==> multRestrictedReport
6. rhs does not contain * (*-restricted (b)) ==> multRestrictedReport
7. all facts are used with the same arity.
8. fr, in, and out, facts are used with arity 1.
9. fr facts are used with a variable of sort msg or sort fresh
10. fresh facts of the same rule contain different variables. [TODO]
11. no protocol fact uses a reserved name => [TODO] change parser to ensure this and pretty printer to show this.

security properties

1. all facts occur with the same arity in the action of some protocol rule.
2. no node variable is used in a message position and vice versa.

Wellformedness checking

type WfErrorReport = [WfError]

checkWellformedness :: OpenTheory -> WfErrorReport

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 -> OpenTheory

Adds a note to the end of the theory, if it is not well-formed.

prettyWfErrorReport :: WfErrorReport -> Doc