Module Clause

module Clause: sig  end

Clauses

exception Clause_error of string * Location.location

Error from EVA input data.

val empty_list : Abstract.eva_value

Special value for empty list.

type htype =

`\|`	`VOID`	`(*`	`NULL type`	`*)`
`\|`	`PRINCIPAL`	`(*`	`predefined type "principal"`	`*)`
`\|`	`NUMBER`	`(*`	`predefined type "number"`	`*)`
`\|`	`AALGO`	`(*`	`predefined type for asymmetric encryption algo`	`*)`
`\|`	`SALGO`	`(*`	`predefined type for symmetric encryption algo`	`*)`
`\|`	`ALGO`	`(*`	`union of the two above`	`*)`
`\|`	`USERTYPE of string`	`(*`	`type of the specification`	`*)`
`\|`	`BASETYPE of string`	`(*`	`type of the specification declared as basetype, subtype of EVA_USERTYPE`	`*)`
`\|`	`FUN of htype`	`(*`	`type of invertible function symbols`	`*)`
`\|`	`HFUN of htype`	`(*`	`type of one-way function symbols`	`*)`
`\|`	`AKEY of htype`	`(*`	`type of asymetric key constructor symbol (declared as element of keypair).`	`*)`

extension of eva_type with types for functional symbols

type state = {

	`st_role : string;`
	`st_label : string;`
	`st_args : Abstract.eva_term list;`

}

A state is a predicate in the set (role, msg label) applied to a list of terms.

type literal =

`\|`	`STATE of state`	`(*`	`state`	`*)`
`\|`	`INTRUK of Abstract.eva_term`	`(*`	`intruder knowledge`	`*)`
`\|`	`HONEST of Abstract.eva_term`	`(*`	`for EVA_ATOM_HONEST`	`*)`
`\|`	`TYPE of Abstract.eva_type * Abstract.eva_term`	`(*`	`type predicate`	`*)`
`\|`	`TYPEA of Abstract.eva_type * Abstract.eva_algo`	`(*`	`type predicate for algos (in EVA, algos are not terms)`	`*)`
`\|`	`TYPEG of Abstract.eva_type * Abstract.eva_term`	`(*`	`generic type predicate DEPRECATED`	`*)`
`\|`	`USER of string * Abstract.eva_term`	`(*`	`for EVA_ATOM_USER`	`*)`

Literals with different predicates, see Abstract.eva_atom

type clause = {

	`cl_neg : literal list;`
	`cl_pos : literal list;`

}

Clauses

type tclause =

`\|`	`AXIOM of clause`
`\|`	`CONJ of clause`
`\|`	`COMMENT of string`

Terms utilities

val locate_term : Abstract.eva_term -> Abstract.eva_lterm

locate_term t

param t an EVA term

Returns a located term made of t.

val locate_id : string -> Abstract.eva_lid

locate_id s

param s an identifer (string)

Returns a located id made of s.

EVA Abstract specifications utilities

val unblock : Abstract.eva_process list -> Abstract.eva_process list

suppress block in processes

val unblock_messages : Abstract.eva_linstr list -> Abstract.eva_linstr list

val has_bang : Abstract.eva_lsession list -> bool

has_bang sl
Returns true iff the given list sl of located session declarations contains a bang. Returns false otherwise.

val string_of_label : Abstract.eva_label -> string

Litterals and clauses utilities

val string_of_llabel : Abstract.eva_llabel -> string

val subst_state : (string * Abstract.eva_term) list -> state -> state

subst_state su st

param su a substitution
param st a state

Returns the state obtained from st by appying the substitution su.

val is_grounding_state : (string * 'a) list -> state -> bool

is_grounding_state su st

param su a substitution
param st a state

Returns whether the given substitution su is grounding for the given state st.

val first_state_clauselist : clause list -> state

first_state_clauselist cl
Raises Not_found if there is no such literal
Returns the first positive literal of type STATE (= new state) found in the given clause list cl.

val states_clauselist : clause list -> state list

states_clauselist cl
Returns the list of positive literals of type STATE (= new state) found in the given clause list cl.

val states_role : string -> state list -> state list

states_role r sl
Returns the sublist of states of the given state list sl with the given role r.