|
|
|
| Description |
| This module defines the Msg data type for the AnB translators and several functions for it.
|
|
| Synopsis |
|
|
|
| Documentation |
|
| type Ident |
| = String | this type is used for all symbols (constants, variables, functions, facts).
| | this is an internal constant to control the number of algebraic reasoning steps that the translator will use.
|
|
|
| data Operator |
| Type for operators (function symbols) in message terms.
| | Constructors | | Crypt | asymmetric encryption
| | Scrypt | symmetric encryption
| | Cat | concatenation---may be soon exchanged for family of n-tuples (n in Nat)
| | Inv | private key of a given public key -- we plan to introduce a distinction between these mappings and other operators
| | Exp | modular exponentation
| | Xor | bitwise exclusive OR
| | Apply | function application, e.g. Apply(f,x) for f(x) is old AVISPA IF standard for user defined functions, aka 1.5th-order logic!
| | Userdef Ident | user-defined function symbols, may replace the above Apply eventually.
|
|  Instances | |
|
|
| data Msg |
| THE main data type...
| | Constructors | | Atom Ident | Atomic terms, i.e. a constant (lower-case) or a variable (upper-case)
| | Comp Operator [Msg] | Composed term with an operator and a list of subterms
|
| | Instances | |
|
|
| type Theory = [(Msg, Msg)] |
| Equational theory as a set of pairs of messages that are supposed to be equal
|
|
| idents :: Msg -> [Ident] |
| Identifiers (constants and variables) occuring in a given message
|
|
| isConstant :: Ident -> Bool |
|
| isAtom :: Msg -> Bool |
|
| isVariable :: Ident -> Bool |
|
| vars :: Msg -> [Ident] |
|
| isCat :: Msg -> Bool |
|
| foldMsg :: (Ident -> a) -> (Operator -> [a] -> a) -> Msg -> a |
| A folding operation on messages (one functor for atomic and one for composed terms)
|
|
| addSub :: Substitution -> Ident -> Msg -> Substitution |
| addSub sigma x t yields the substition [x|->t] . sigma where
we assume that x and the variables of t are disjoint from the
domain of sigma and x does not occur in the range of sigma.
|
|
| type Substitution = Msg -> Msg |
| Substitutions when already extended to a homomorphism on Msg
|
|
| eqMod :: Int -> Theory -> [Msg] -> [Msg] |
| equivalence modulo a given number of applications of rules of a theory
|
|
| eqModBound :: Int |
|
| (===) :: Msg -> Msg -> Bool |
Variables of a given message
syntactic equivalence on Msg
|
|
| catty :: OutputType -> [Msg] -> [Char] |
|
| deCat :: Msg -> [Msg] |
|
| stdTheo :: [(Msg, Msg)] |
|
| synthesizable :: [Msg] -> Msg -> Bool |
| Ground Dolev-Yao: synthesizable ik m holds (for ground ik and
m) if m can be composed from messages in ik (i.e. without
analysis steps). This does take the standard equational theory into
account.
|
|
| analysis :: [Msg] -> [Msg] |
| Analysis according to Dolev-Yao: given ground set of messages,
compute the closure under analysis steps (pairs are filtered out).
|
|
| indy :: [Msg] -> Msg -> Bool |
| indy ik m holds for ground ik and m if ik |- m (Dolev-Yao
deduction modulo the standard equational theory).
|
|
| normalizeXor :: Msg -> Msg |
| Normalize a ground term modulo the cancelation theory for XOR
(i.e. t XOR t -> e and t XOR e -> t).
|
|
| ppId :: Ident -> String |
True for an atomic identifier that is a typename.
False for any term t=f(...) and f is a user-defined function
symbol.
print identifiers (filter for alpha-numeric characters)
|
|
| ppIdList :: [Ident] -> String |
|
| ppMsg :: OutputType -> Msg -> String |
print list of identifiers, separated by commata
print a message
|
|
| ppMsgList :: OutputType -> [Msg] -> [Char] |
|
| ppXList :: (a -> String) -> String -> [a] -> String |
remove the Cat-operator from a message (return the list of concatenated messages).
print non-empty list of messages [m1,...,mk] in the form
pair(m1,pair(m2,...,mk)) using ppMsg for printing messages with
the given output format.
print list of messages (comma-separated)
generic printing functional: given a printer for type alpha, a
seperator, and a list of alpha-type elements, compute the
printout of this list using the alpha-printer and interspered by
the seperator.
|
|
| match0 :: [(Msg, Msg)] -> Substitution -> [Substitution] |
| Matching function: takes a list of pairs (p,m) of messages and
an initial substitution sigma0. (Typically, this is called with
the identity as an initial substitution.) We require that sigma0
does not substitute variables that occur in any pair (p,m). The
procedure computes all substitutions sigma that extend the
initial substitution sigma0 such that p sigma=m. Warning:
variables in m may not be handled correctly,
|
|
| isAtype :: Msg -> Bool |
|
| isntFunction :: Msg -> Bool |
|
| Produced by Haddock version 2.6.0 |
