module Signature: sig end
clauses for typing the reserved symbols of the signature
val typing_cst : Symbols.eva_symbol_list -> Clause.clause list
typing of declared constants
val typing_intruder : Clause.clause
typing of the the intruders name
val typing_val : Symbols.eva_symbol_list -> Clause.clause list
typing of declared values (ie other constants)
val typing_emptylist : Clause.clause
typing of the empty list
val typing_cons : Clause.clause
typing of CONS
val typing_app : Symbols.eva_symbol_list -> Clause.clause list
typing of APP
val typing_vanilla : Clause.clause list
typing of the VANILLA
in this settings, VANILLA is a (constant) function symbol.
val typing_algo : Clause.clause list
typing the union of symmetric and assymetric algorithms
val typing_crypt_algo : Clause.clause
typing of CRYPT, variable algo
the abstract spec should not contain EVA_SIGN
val typing_P : Clause.clause
typing of coercion symbol P
val typing_A : Clause.clause
typing of coercion symbol A
val typing_SA : Clause.clause
typing of coercion symbol SA
val typing_AA : Clause.clause
typing of coercion symbol AA
val typing_U : Symbols.eva_symbol_list -> Clause.clause list
typing of coercion symbol U
val horn_signature : Symbols.eva_symbol_list -> Clause.clause list