|
|
|
|
| Synopsis |
|
|
|
| Documentation |
|
| type ProtocolState = [LMsg] |
| The type ProtocolState characterizes the local state of an
honest agent in a protocol execution by a set of labeled messages,
i.e. the form the messages are supposed to have according to the
AnB specification and the actual view on that form that the agent
in question has.
|
|
| mkname :: Msg -> Msg |
| This function generates a unique variable name of the form Xsomething from a given message;
|
|
| initialState :: [Msg] -> ProtocolState |
| generate the initial state of a local agent from its knowledge specification
|
|
| receiveMsg :: Msg -> ProtocolState -> ProtocolState |
| compute the new protocol state of an agent that corresponds to
the reception of a new message. This is typically used for the LHS
state-fact of an honest agent in a transition rule: given the state
after the last transition rule (a list of labeled messages) and the
newly received message (without label), compute the labeled
messages for the state-fact of the LHS.
|
|
| sendMsg :: Msg -> ProtocolState -> ProtocolState |
| Counterpart to receiveMsg: given a message to be sent (according
to the protocol specification) and the current execution state as a
list of labeled messages, check that, and how, this sendendum can
be generated and add it with appropriate label to the protocol state.
|
|
| receiveLMsg :: LMsg -> ProtocolState -> ProtocolState |
| Variant of receiveMsg when pattern for the received message is
given (for modeling zero-knowledge proofs).
|
|
| lversion :: Bool |
| switch for an experimental version
|
|
| synthesisPattern :: ProtocolState -> Msg -> Maybe Msg |
| Given a protocol state and an unlabled message (on AnB level) to
compose, check if that is possible, and if so, give a label for that.
|
|
| Produced by Haddock version 2.6.0 |
