|
|
|
|
| Synopsis |
|
| type Protocol = (String, Types, Knowledge, Abstraction, Actions, Goals) | | | | | type Types = [(Type, [Ident])] | | | type Knowledge = [(Ident, [Msg])] | | | type Peer = (Ident, Bool, Maybe Msg) | | | type Channel = (Peer, ChannelType, Peer) | | | type Action = (Channel, Msg, Maybe Msg, Maybe Msg) | | | type Actions = [Action] | | | | | | | type Goals = [Goal] | | | type Abstraction = [(Ident, Msg)] |
|
|
| Documentation |
|
| type Protocol = (String, Types, Knowledge, Abstraction, Actions, Goals) |
| The type Protocol is the type for the result of the AnB-Parser,
i.e. the topmost structure of the Abstract Syntax Tree (AST)
|
|
| data Type |
| The (atomic) type identifiers
| | Constructors | | Agent Bool Bool | flags: static, honest; both currently unused
| | Number | aka nonce
| | PublicKey | | | SymmetricKey | | | Function | for free user-defined function symbols (no input/output type specification)
| | Purpose | special type for the purpose-argument of witness and request facts
| | Untyped | default for constants/variables that do not have a type declaration
|
|  Instances | |
|
|
| type Types = [(Type, [Ident])] |
| A type declaration consist of a type and a list of identifiers
(constants or variables) that have that type
|
|
| type Knowledge = [(Ident, [Msg])] |
| A knowledge declaration consists of an identifier for a role
(constant or variable; should be of type Agent!) and a list of
messages that this role initially knows. The variables in that
knowledge should always be of type Agent; this is not checked now,
however.
|
|
| type Peer = (Ident, Bool, Maybe Msg) |
| A peer is the endpoint of a channel (i.e. sender or
receiver). The identifier is the real name (according to the
specification), the bool says whether this agent is
pseudonymous. The third is the pseudonym in case the agent is
pseudonymous.
|
|
| type Channel = (Peer, ChannelType, Peer) |
| A channel is characterized by a sender and receiver peer, and by
a channel type, e.g. ((A,False,Nothing),Secure,(B,True,PKB))
|
|
| type Action = (Channel, Msg, Maybe Msg, Maybe Msg) |
| An action consists of a channel (sender, channeltype, receiver)
and a message being sent. Additionally, there are two optional
message terms for modeling zero-knowledge protocols, namely a
pattern for the receiver, and a message that the sender must know
|
|
| type Actions = [Action] |
| List of actions
|
|
| data ChannelType |
| The different supported channel types
| | Constructors | | Insecure | -> standard channel
| | Authentic | *-> sender and intended recipient secured
| | Confidential | ->* recipient secured
| | Secure | *->* both authentic and confidential
| | FreshAuthentic | *->> like authentic, but protected against replay
| | FreshSecure | *->>* like secure, but protected against replay
|
| | Instances | |
|
|
| data Goal |
| The pre-defined set of goals
| | Constructors | | ChGoal Channel Msg | Goals that are expressed in channel notation
| | Secret Msg [Peer] | Standard secrecy goal
| | Authentication Peer Peer Msg | Standard authentication
goal (including replay
protection; corresponds to
Lowe's injective
agreement)
| | WAuthentication Peer Peer Msg | Weaker form of
authentication: no
protection against
replay. Corresponds to
Lowe's non-injective
agreement.
|
| | Instances | |
|
|
| type Goals = [Goal] |
| List of gaols
|
|
| type Abstraction = [(Ident, Msg)] |
| For the annotation of abstractions: to express that a variable
(identifier) should be abstracted into a given term. This
represents replacing in the entire description all occurrences of
that variable with that term.
|
|
| Produced by Haddock version 2.6.0 |
