Module Symbols

module Symbols: sig  end

Manage the abstract data type of symbols of the protocol specifications

There are 8 kinds of symbols:

first order identifiers (either constant or parameter or private process variable)
functional identifiers (either constant or parameter or private process variable)
constructors for asymetric keys, declared as component of a key pair
values for instanciation of sessions
intruder, a special reserved value
quantified variable in an axiom declaration or an "assume" formula
alias
user type

Exceptions

exception Symbols_error of string

raised by accessors

exception Symbols_not_found

raised by Symbols.assoc_symbol

exception Symbols_already of string

raised when adding a symbol already present to a symbol list the argumeent is the name of the symbol

Symbols type

type eva_symbol

type of symbols

constructors

val new_first_order_symbol : string ->
       Abstract.eva_scope -> Abstract.eva_type -> bool -> eva_symbol

Returns a symbol of kind "first order" with the given attributes:

name
quality
type
true if the identifier is fresh, false otherwise.

val new_functional_symbol : string ->
       Abstract.eva_scope ->
       Abstract.eva_type ->
       Abstract.eva_type list -> bool -> bool -> eva_symbol

Returns a symbol of kind "functional" with the given attributes:

name
quality
type
signature
true if the function is one-way, false otherwise.
true if the function is secret, false otherwise.

val new_key_symbol : string ->
       Abstract.eva_scope ->
       Abstract.eva_type ->
       Abstract.eva_type list -> string -> Abstract.eva_algo -> eva_symbol

Returns a symbol of kind "key" constructor with the given attributes:

name
quality
type
signature
name of the other key of the key pair
associed encryption algorithm

val new_value_symbol : string -> Abstract.eva_type -> eva_symbol

Returns a symbol of kind "value" with the given attributes:

name
type

val intruder_symbol : eva_symbol

Returns a symbol corresponding to the value "intruder"

val new_alias_symbol : string -> Abstract.eva_lterm -> eva_symbol

Returns a symbol of kind "alias" with the given attributes:

name
replacement located term

val new_quantified_symbol : string -> Abstract.eva_type -> eva_symbol

Returns a symbol of kind "quantified variable" with the given attributes:

identifier
type in quantification

val new_type_symbol : string -> bool -> eva_symbol

Returns a symbol of kind "type" with the given attributes:

name
true if it is a basetype, false otherwise

val new_predicate_symbol : string -> eva_symbol

Returns a symbol of kind "predicate" with the given attributes:

name

val is_first_order : eva_symbol -> bool

Returns true if the given symbol is of kind "first order", false otherwise

val is_functional : eva_symbol -> bool

Returns true if the given symbol is of kind "functional", false otherwise

val is_key : eva_symbol -> bool

Returns true if the given symbol is of kind "key", false otherwise

val is_value : eva_symbol -> bool

Returns true if the given symbol is of kind "value", false otherwise

val is_intruder : eva_symbol -> bool

Returns true if the given symbol is the "intruder" value, false otherwise

val is_quantified : eva_symbol -> bool

Returns true if the given symbol is of kind "quantified variable", false otherwise

val is_alias : eva_symbol -> bool

Returns true if the given symbol is of kind "alias", false otherwise

val is_type : eva_symbol -> bool

Returns true if the given symbol is of kind "type", false otherwise

val is_basetype : eva_symbol -> bool

Returns true if the given symbol is a user type declared as basetype, subcase of is_type false otherwise

val is_predicate : eva_symbol -> bool

Returns true if the given symbol is of kind "predicate", false otherwise

val get_name : eva_symbol -> string

Returns the name of the given symbol. Symbols of every kinds have a name.

val get_type : eva_symbol -> Abstract.eva_type

Raises Symbols_error if the given symbol is not typed.
Returns the type of the given symbol.

val get_scope : eva_symbol -> Abstract.eva_scope

Raises Symbols_error if the given symbol has no such characteristic.
Returns the scope of the given symbol.

val get_fresh : eva_symbol -> bool

Raises Symbols_error if the given symbol has no such characteristic.
Returns the "fresh" characteristic of the given symbol.

val get_hash : eva_symbol -> bool

Raises Symbols_error if the given symbol has no such characteristic.
Returns the "hash" characteristic of the given symbol.

val get_secret : eva_symbol -> bool

Raises Symbols_error if the given symbol has no such characteristic.
Returns the "secret" characteristic of the given symbol.

val get_signature : eva_symbol -> Abstract.eva_type list

Raises Symbols_error if the given symbol has no such characteristic.
Returns the signature of the given symbol.

val get_symkey : eva_symbol -> string

Raises Symbols_error if the given symbol has no such characteristic.
Returns the name of the symmetric key associed to the given symbol.

val get_algo : eva_symbol -> Abstract.eva_algo

Raises Symbols_error if the given symbol has no such characteristic.
Returns the algorithm associed with the given symbol.

val get_term : eva_symbol -> Abstract.eva_lterm

Raises Symbols_error if the given symbol is not of kind "alias".
Returns the term associed with the given alias symbol.

type eva_symbol_list

Abstract type for lists of symbols

val empty_symbol_list : eva_symbol_list

generic empty symbol list.

val memassoc_symbol : string -> eva_symbol_list -> bool

Returns true if the given symbol list sl contains a symbol declared with the given name, returns false otherwise.

val assoc_symbol : string -> eva_symbol_list -> eva_symbol

Raises Symbols_not_found if the given name is not declared in sl.
Returns the symbol declared with the given name in the given symbol list sl.

val append_symbol : eva_symbol -> eva_symbol_list -> eva_symbol_list

Raises Symbols_already with the name of s if there is already a symbol with the same name as s in the given symbol list sl.
Returns a symbols list obtained by adding the given symbol s at the end of the given symbol list sl.

val add_symbol : eva_symbol -> eva_symbol_list -> eva_symbol_list

add_symbol s sl
Returns a symbols list obtained by adding the given symbol s at the end of the given symbol list sl only if sl does not already contain a symbol with the same name as s.

val overwrite_symbol : eva_symbol -> eva_symbol_list -> eva_symbol_list

Returns a symbols list obtained from the the given symbol s and the given symbol list sl as follows:

if sl contains no symbol with the name of s, append s to sl
if sl contains a symbol s1 with the name of s, returns sl where s has been replaced by s1.

val append_symbollist : eva_symbol_list -> eva_symbol_list -> eva_symbol_list

Raises Symbols_already if l1 contains already one symbol with the same name as a symbol of l2.
Returns the symbols list obtained by adding the symbols in the second given list l2 at the end of the first symbols list l1.

val overwrite_symbollist : eva_symbol_list -> eva_symbol_list -> eva_symbol_list

Returns the symbols list obtained by overwriting the symbols in second the given list l2 with the symbols in the first given list l1 (see Symbols.overwrite_symbol).

val symbol_list_length : eva_symbol_list -> int

Returns the length of the given symbol list sl.

val iter_symbollist : (eva_symbol -> unit) -> eva_symbol_list -> unit

Iterator for symbol lists. Apply in a row the given function f to each of the symbols contained in the given symbol list sl.

val map_symbollist : (eva_symbol -> 'a) -> eva_symbol_list -> 'a list

map_symbollist f sl
Returns the list (f s1); ...; (f sn) where s1...sn are the symbols of the given symbol list sl.

val fold_left_symbollist : ('a -> eva_symbol -> 'a) -> 'a -> eva_symbol_list -> 'a

fold_left_symbollist f a sl
Returns f (... (f (f a s1) s2) ...) sn where s1...sn are the symbols of the given symbol list sl.

val fold_right_symbollist : (eva_symbol -> 'a -> 'a) -> eva_symbol_list -> 'a -> 'a

fold_right_symbollist f sl b
Returns f s1 (f s2 (... (f sn b) ...)) where s1...sn are the symbols of the given symbol list sl.