|
|
|
|
| Synopsis |
|
|
|
| Documentation |
|
| type LMsg = (Msg, Msg) |
| Labeled message: the message itself as it was specified in AnB,
and another message labeling it, representing the view that a
particular agent has on it. Example: (h(N),HN) if we have what is
supposed to be a hash of a nonce, and we model an agent who cannot
check this (because he does not know the nonce and cannot invert
it).
|
|
| lanalysis :: [LMsg] -> ([LMsg], [LMsg]) |
| Main analysis function: given a set of labeled messages, compute
the closure under analysis rules. This is typically used in the
translation step after an agent has learned a new message. The
existing labels of the messages may be updated by this, because
analysis reveals new checks that can be performed. Also, the result
distinguishes the old and new messages (i.e. messages that were
part of the given knowledge but may have new labels are
distinguished from messages obtained by analysis steps).
|
|
| mkname :: Msg -> Msg |
| This function generates a unique variable name of the form Xsomething from a given message;
|
|
| zipl :: [a] -> [b] -> [(a, b)] |
| Like zip with an additional check that the lengths of the zipped lists are identical
|
|
| Produced by Haddock version 2.6.0 |
