C | |
| comma_sep [Hornpp] |
standard comma separation to use for
pp_list
|
E | |
| empty_list [Clause] |
Special value for empty list.
|
F | |
| first_state_clauselist [Clause] | first_state_clauselist cl
|
H | |
| has_bang [Clause] | has_bang sl
|
| horn_assume_lstatement [Import] | |
| horn_claim_lstatement [Import] | horn_claim_lstatement rl stl f
|
| horn_instr [Import] | horn_instr st lab i
|
| horn_linstr [Import] | horn_linstr st lab i
|
| horn_linstrlist [Import] | horn_linstrlist st il
|
| horn_lprotocol [Import] | horn_protocol sl pr
|
| horn_lsession [Import] | horn_session stl sl s
|
| horn_process [Import] | horn_process init_state pr
|
| horn_signature [Signature] | |
| horn_spec [Import] | horn_spec sp
|
| hornpp_clause [Hornpp] | hornpp_clause sl c
print the given clause c
using the given symbol list sl.
|
| hornpp_id [Hornpp] | hornpp_id sl i
prints the given identifier i
using the given symbol list sl.
|
| hornpp_label [Hornpp] | hornpp_label l
prints the given label l.
|
| hornpp_lid [Hornpp] | hornpp_lid sl i
prints the given located identifier i
using the given symbol list sl.
|
| hornpp_literal [Hornpp] | hornpp_literal sign sl l
prints the given literal l
preceeded by the given string sign
and using the given symbol list sl.
|
| hornpp_llabel [Hornpp] | hornpp_label l
prints the given located label l.
|
| hornpp_lscope [Hornpp] | hornpp_lscope s
prints the given located scope s.
|
| hornpp_lterm [Hornpp] | hornpp_lterm sl t
prints the given located term t
using the given symbol list sl.
|
| hornpp_ltype [Hornpp] | hornpp_ltype t
prints the given located type t.
|
| hornpp_lvalue [Hornpp] | hornpp_lvalue v
prints the given located value v.
|
| hornpp_scope [Hornpp] | hornpp_scope s
prints the given scope s.
|
| hornpp_tclause [Hornpp] | hornpp_tclause sl c
print the given tclause c
using the given symbol list sl.
|
| hornpp_term [Hornpp] | hornpp_term sl t
prints the given term t
using the given symbol list sl.
|
| hornpp_type [Hornpp] | hornpp_type t
prints the given type t.
|
| hornpp_value [Hornpp] | hornpp_value v
prints the given value v.
|
I | |
| intruder_DA [Intruder] |
decryption with asymmetric key made of APP with key symbol
or made of a singleton list containing an APP with key symbol
|
| intruder_DAPP [Intruder] |
decryption with symmetric key made of APP
with function symbol which is not a asymetric key.
|
| intruder_DCONS [Intruder] |
decryption with symmetric key made of CONS
|
| intruder_DCRYPT [Intruder] |
decryption with symmetric key made of CRYPT
|
| intruder_DI [Intruder] |
decryption with symmetric key which is
the intruder's name (USEFUL ?).
|
| intruder_Dcst [Intruder] |
decryption with constant symmetric key
|
| intruder_Dval [Intruder] |
decryption with symmetric key which is
a constant declared as value
|
| intruder_E [Intruder] |
encryption with known key
|
| intruder_F [Intruder] |
application of known function symbol
|
| intruder_F1 [Intruder] |
inversion of known function symbol
|
| intruder_P [Intruder] |
pairing
|
| intruder_P1 [Intruder] |
left projection
|
| intruder_P2 [Intruder] |
right projection
|
| intruder_coerce [Intruder] |
coercion functions
|
| intruder_coerce1 [Intruder] |
inversion of coercion functions
|
| intruder_empty [Intruder] |
empty_list
|
| is_grounding_state [Clause] | is_grounding_state su st param su a substitution, param st a state
|
L | |
| locate_id [Clause] | locate_id s param s an identifer (string)
|
| locate_term [Clause] | locate_term t param t an EVA term
|
N | |
| newline2_sep [Hornpp] |
double new line separation to use for pp_list
|
| newline_sep [Hornpp] |
standard new line separation to use for
pp_list
|
| null_sep [Hornpp] |
standard null separation to use for
pp_list
|
P | |
| prologpp_clause [Prologpp] | prologpp_clause sl cl
pretty print the given clause cl
using the given symbol list sl.
|
| prologpp_tclause [Prologpp] | prologpp_clause sl c
pretty print the given tclause c
using the given symbol list sl.
|
R | |
| rules [Intruder] |
list of clauses for the intruder deduction rules
|
S | |
| semicol_sep [Hornpp] |
standard semicolumn separation to use for
pp_list
|
| states_clauselist [Clause] | states_clauselist cl
|
| states_role [Clause] | states_role r sl
|
| string_of_label [Clause] |
Litterals and clauses utilities
|
| string_of_llabel [Clause] | |
| subst_state [Clause] | subst_state su st param su a substitution, param st a state
|
T | |
| tptppp_clause [Tptppp] | tptppp_clause sl c
pretty prints the given clause c in the TPTP format,
using the given symbol list sl.
|
| tptppp_tclauses [Tptppp] | tptppp_tclauses sl cl
pretty prints the given list of tclause cl in the TPTP format,
using the given symbol list sl.
|
| typing_A [Signature] |
typing of coercion symbol A
|
| typing_AA [Signature] |
typing of coercion symbol AA
|
| typing_P [Signature] |
typing of coercion symbol P
|
| typing_SA [Signature] |
typing of coercion symbol SA
|
| typing_U [Signature] |
typing of coercion symbol U
|
| typing_algo [Signature] |
typing the union of symmetric and assymetric algorithms
|
| typing_app [Signature] |
typing of APP
|
| typing_cons [Signature] |
typing of CONS
|
| typing_crypt_algo [Signature] |
typing of CRYPT, variable algo
|
| typing_cst [Signature] |
typing of declared constants
|
| typing_emptylist [Signature] |
typing of the empty list
|
| typing_intruder [Signature] |
typing of the the intruders name
|
| typing_val [Signature] |
typing of declared values (ie other constants)
|
| typing_vanilla [Signature] |
typing of the VANILLA
in this settings, VANILLA is a (constant) function symbol.
|
U | |
| unblock [Clause] |
suppress block in processes
|
| unblock_messages [Clause] |