module Intruder: sig end
Clauses defining intruder deduction rules
CONS
val intruder_empty : Clause.clause
empty_list
val intruder_P : Clause.clause
pairing
val intruder_P1 : Clause.clause
left projection
val intruder_P2 : Clause.clause
right projection
APP
val intruder_F : Symbols.eva_symbol_list -> Clause.clause list
application of known function symbol
val intruder_F1 : Symbols.eva_symbol_list -> Clause.clause list
inversion of known function symbol
CRYPT
we assume that the intruder knows all the encryption algos
(symmetric and asym)
val intruder_E : Clause.clause
encryption with known key
val intruder_Dcst : Symbols.eva_symbol_list -> Clause.clause list
decryption with constant symmetric key
val intruder_DI : Symbols.eva_symbol_list -> Clause.clause
decryption with symmetric key which is
the intruder's name (USEFUL ?).
val intruder_Dval : Symbols.eva_symbol_list -> Clause.clause list
decryption with symmetric key which is
a constant declared as value
val intruder_DCONS : Symbols.eva_symbol_list -> Clause.clause
decryption with symmetric key made of CONS
val intruder_DAPP : Symbols.eva_symbol_list -> Clause.clause list
decryption with symmetric key made of APP
with function symbol which is not a asymetric key.
val intruder_DCRYPT : Clause.clause
decryption with symmetric key made of CRYPT
we assume no use of SIGN
val intruder_DA : Symbols.eva_symbol_list -> Clause.clause list
decryption with asymmetric key made of APP with key symbol
or made of a singleton list containing an APP with key symbol
coercion
val intruder_coerce : Symbols.eva_symbol_list -> Clause.clause list
coercion functions
val intruder_coerce1 : Symbols.eva_symbol_list -> Clause.clause list
inversion of coercion functions
val rules : Symbols.eva_symbol_list -> Clause.clause list
list of clauses for the intruder deduction rules