Module Abstract

module Abstract: sig  end

Abstract syntax for protocol specifications

type eva_label =

`\|`	`EVA_NOLABEL`	`(*`	`empty label`	`*)`
`\|`	`EVA_LABEL of string`	`(*`	`other label`	`*)`

Label of message, claim or session

type eva_llabel = {

	`lla_loc : Location.location;`
	`lla_label : eva_label;`

}

Located label

type eva_type =

`\|`	`EVA_VOID`	`(*`	`NULL type`	`*)`
`\|`	`EVA_PRINCIPAL`	`(*`	`predefined type "principal"`	`*)`
`\|`	`EVA_NUMBER`	`(*`	`predefined type "number"`	`*)`
`\|`	`EVA_AALGO`	`(*`	`predefined type for asymmetric encryption algo`	`*)`
`\|`	`EVA_SALGO`	`(*`	`predefined type for symmetric encryption algo`	`*)`
`\|`	`EVA_TALGO`	`(*`	`union of the two above`	`*)`
`\|`	`EVA_USERTYPE of string`	`(*`	`type of the specification`	`*)`
`\|`	`EVA_BASETYPE of string`	`(*`	`type of the specification declared as basetype, subtype of EVA_USERTYPE`	`*)`
`\|`	`EVA_FUN of eva_type`	`(*`	`type of symbols of invertible functions from numbers to the given type`	`*)`
`\|`	`EVA_HFUN of eva_type`	`(*`	`type of symbols of one-way functions from numbers to the given type`	`*)`
`\|`	`EVA_KEY of eva_type`	`(*`	`type of symbol of asymetric key constructor, declared as an element of keypair.`	`*)`

EVA types

Located type

type eva_ltype = {

	`lty_loc : Location.location;`
	`lty_type : eva_type;`

}

type eva_scope =

`\|`	`EVA_CST`	`(*`	`global constant`	`*)`
`\|`	`EVA_PARAM`	`(*`	`session parameter`	`*)`
`\|`	`EVA_PRIVATE`	`(*`	`local var of process`	`*)`

Quality of identifiers

type eva_lscope = {

	`lsc_loc : Location.location;`
	`lsc_scope : eva_scope;`

}

type eva_id =

`\|`	`EVA_ID of string`

Protocol identifier It can be either a parameter, a constant, a private (process) variable.

type eva_lid = {

	`lid_loc : Location.location;`
	`lid_id : eva_id;`

}

Located identifier

type eva_value =

`\|`	`EVA_INTRUDER`	`(*`	`special value for the intruder's name`	`*)`
`\|`	`EVA_VALUE of string`	`(*`	`arbitrary value`	`*)`

Value to be assigned to a identifier in a session declaration

type eva_lvalue = {

	`lva_loc : Location.location;`
	`lva_value : eva_value;`

}

Located value

type eva_term =

`\|`	`EVA_TERM_ID of string`	`(*`	`parameter or private variable (first order symbol or function symbol or keypair symbol)`	`*)`
`\|`	`EVA_TERM_CST of string`	`(*`	`constant symbol (first order symbol or function symbol or keypair symbol)`	`*)`
`\|`	`EVA_TERM_VALUE of eva_value`	`(*`	`first order value, for formulas only`	`*)`
`\|`	`EVA_TERM_ALIAS of string * eva_lterm`	`(*`	`alias symbol`	`*)`
`\|`	`EVA_LOCATED of eva_lid * eva_lid`	`(*`	`located variable, only for formulas name of identifier name of role`	`*)`
`\|`	`EVA_QUANTIFIED of string * eva_type`	`(*`	`quantified variable, only for axioms and assume name of the identifier type declared in quantification (default is EVA_NUMBER)`	`*)`
`\|`	`EVA_P of eva_lterm`	`(*`	`coercion symbol EVA_PRINCIPAL -> EVA_NUMBER term to cast`	`*)`
`\|`	`EVA_A of eva_lterm`	`(*`	`coercion symbol EVA_TALGO -> EVA_NUMBER term to cast`	`*)`
`\|`	`EVA_SA of eva_lterm`	`(*`	`coercion symbol EVA_SALGO -> EVA_TALGO term to cast`	`*)`
`\|`	`EVA_AA of eva_lterm`	`(*`	`coercion symbol EVA_AALGO -> EVA_TALGO term to cast`	`*)`
`\|`	`EVA_U of (string * eva_lterm)`	`(*`	`coercion symbol (EVA_USERTYPE t) -> EVA_NUMBER identifier of the user type term to cast`	`*)`
`\|`	`EVA_CONS of eva_lterm list`	`(*`	`tuple of terms`	`*)`
`\|`	`EVA_APP of eva_lid * eva_lterm list`	`(*`	`application of function symbol root symbol arguments`	`*)`
`\|`	`EVA_CRYPT of eva_algo * eva_lterm * eva_lterm`	`(*`	`cipher text algo key content`	`*)`
`\|`	`EVA_SIGN of eva_algo * eva_lterm * eva_lterm`	`(*`	`signature algo key content`	`*)`
`\|`	`EVA_PCENT of eva_lterm * eva_lterm`	`(*`	`Lowe's notation`	`*)`

Abstract term

type eva_lterm = {

	`lte_loc : Location.location;`
	`lte_term : eva_term;`

}

Located term

type eva_algo =

`\|`	`EVA_VANILLA`	`(*`	`generic symmetric key algorithm`	`*)`
`\|`	`EVA_ALGO of eva_lterm`	`(*`	`other algorithm, the lterm is restricted to be a constant`	`*)`

Name of encryption algorithm

type eva_dcl =

`\|`	`EVA_DCL_ID of (eva_lid * bool) list * eva_lscope * eva_ltype`	`(*`	`declaration of first order identifiers list of pairs of (identifier name, flag) where the flag is true iff the identifier is declared to be fresh scope common to all the identifiers of the list type common all the identifiers of the list`	`*)`
`\|`	`EVA_DCL_FUN of eva_lid * eva_lscope * eva_ltype * eva_ltype list * bool * bool`	`(*`	`declaration of functional identifier name of the function symbol scope of the identifier domain type list of the respective types of the arguments of the function symbol flag true iff the function symbol is declared to be hash (one-way) flag true iff the function symbol is declared to be secret`	`*)`
`\|`	`EVA_DCL_KEYPAIR of eva_algo * eva_lid * eva_lid * eva_lscope * eva_ltype * eva_ltype list`	`(*`	`declaration of a pair of asymmetric keys associated encryption algorithm name of first key name of second key scope of both keys (domain) type of both keys list of the respective types of the arguments of both keys (can be empty)`	`*)`
`\|`	`EVA_DCL_ALIAS of eva_lid * eva_lterm`	`(*`	`declaration of an alias name of the alias term for replacement`	`*)`
`\|`	`EVA_DCL_LOCALALIAS of eva_lid list * eva_lid * eva_lterm`	`(*`	`declaration of local alias`	`*)`
`\|`	`EVA_DCL_BASETYPE of string`	`(*`	`declaration of user base type, specific to verifying tool`	`*)`
`\|`	`EVA_DCL_KNOW of eva_lid * eva_lterm list`	`(*`	`declaration of initial knowledge of a principal, for initialisation of the components of its local state principal name list of initial knowledge`	`*)`
`\|`	`EVA_DCL_EVERY of eva_lterm list`	`(*`	`declaration of initial knowledge of every principal`	`*)`
`\|`	`EVA_DCL_AXIOM of eva_lterm * eva_lterm * eva_type * (eva_lid * eva_ltype) list`	`(*`	`equational axiom left term right term type (of both left and right terms) quantified variables with types`	`*)`
`\|`	`EVA_DCL_VALUE of eva_lvalue list * eva_ltype`	`(*`	`values (for session instanciation) list of value identifiers declared type common all the identifiers of the list`	`*)`

Declarations in the EVA protocol specification

type eva_ldcl = {

	`ldc_loc : Location.location;`
	`ldc_dcl : eva_dcl;`

}

Located declaration

type eva_instr =

`\|`	`EVA_SKIP`	`(*`	`do nothing`	`*)`
`\|`	`EVA_MSG of eva_llabel * eva_lid * eva_lid * eva_lterm`	`(*`	`protocol message label sender receiver body`	`*)`
`\|`	`EVA_ASSIGN of eva_lid * eva_lid * eva_lterm`	`(*`	`assignment of a principal's local variable role variable value`	`*)`
`\|`	`EVA_COMP of eva_lid * eva_lid * eva_lterm`	`(*`	`comparison between two local variables in a principal's state role left variable right variable`	`*)`
`\|`	`EVA_BLOCK of eva_linstr list`	`(*`	`block of instructions`	`*)`
`\|`	`EVA_SWITCH of eva_lterm * eva_case list`	`(*`	`switch case branching`	`*)`

Protocol instruction

type eva_linstr = {

	`lin_loc : Location.location;`
	`lin_instr : eva_instr;`

}

Located instruction

type eva_case = {

	`case_case : eva_lterm;`
	`case_block : eva_linstr list;`
	`case_loc : Location.location;`

}

case for EVA_SWITCH

type eva_protocol =

`\|`	`EVA_MP of eva_linstr list`	`(*`	`presentation a la BAN of all the processes in one block`	`*)`
`\|`	`EVA_PROCESS of eva_process list`	`(*`	`separate presentation of the processes`	`*)`

Description of the messages of the protocol

type eva_lprotocol = {

	`lpr_loc : Location.location;`
	`lpr_protocol : eva_protocol;`

}

Located protocol message description

type eva_process = {

`pr_role : eva_lid;`	`(*`	`the principal running the process`	`*)`
`pr_privates : eva_lid list;`	`(*`	`private variables They all have type number`	`*)`
`pr_messages : eva_linstr list;`	`(*`	`instructions`	`*)`

}

Process associated to a principal. the messages contains protocol constant and parameters and other private variables declared under the field private.

type eva_constraint =

`\|`	`EVA_EQ_CONSTRAINT of eva_lid * eva_lid`	`(*`	`id == id`	`*)`
`\|`	`EVA_NEQ_CONSTRAINT of eva_lid * eva_lid`	`(*`	`id != id`	`*)`
`\|`	`EVA_MEMBERSHIP_CONSTRAINT of eva_lid * eva_lterm list`	`(*`	`id in { val list }`	`*)`
`\|`	`EVA_DOMAIN_CONSTRAINT of eva_lid * string`	`(*`	`id in the interpretation of the predicate`	`*)`

Constraints on the session domains

type eva_lconstraint = {

	`lco_loc : Location.location;`
	`lco_constraint : eva_constraint;`

}

Located constraint

type eva_session =

`\|`	`EVA_BANG`
`\|`	`EVA_CONSTRAINED_SESSIONS of eva_lconstraint list`	`(*`	`infinite parallel constraint sessions`	`*)`
`\|`	`EVA_SESSIONS of (eva_lid * eva_lterm) list`	`(*`	`copies of a single session association list (var = value)`	`*)`
`\|`	`EVA_SESSION of eva_llabel * (eva_lid * eva_lterm) list`	`(*`	`single session label association list (var = value)`	`*)`

Declaration of a system assignment for verification

type eva_lsession = {

	`lse_loc : Location.location;`
	`lse_session : eva_session;`

}

Located session declaration

type eva_atom =

`\|`	`EVA_TRUE`
`\|`	`EVA_FALSE`
`\|`	`EVA_ATOM_EQ of eva_lterm * eva_lterm`
`\|`	`EVA_ATOM_NEQ of eva_lterm * eva_lterm`
`\|`	`EVA_ATOM_HONEST of eva_lterm`
`\|`	`EVA_ATOM_SECRET of eva_lterm`
`\|`	`EVA_ATOM_USER of eva_lid * eva_lterm`	`(*`	`Located atom`	`*)`

Atom in formula

type eva_latom = {

	`lat_loc : Location.location;`
	`lat_atom : eva_atom;`

}

type eva_statement =

`\|`	`EVA_ASSUME of (eva_lid * eva_ltype) list * eva_latom list * eva_latom`	`(*`	`hypothesis quantification formula tail of Horn clause head of Horn clause`	`*)`
`\|`	`EVA_CLAIM of eva_llabel * eva_latom list * eva_latom`	`(*`	`formula to verify optional label tail of Horn clause head of Horn clause`	`*)`

Formula

type eva_lstatement = {

	`lst_loc : Location.location;`
	`lst_statement : eva_statement;`

}

Located formula

type eva_spec = {

`sp_label : eva_lid;`	`(*`	`protocol label`	`*)`
`sp_declarations : eva_ldcl list;`	`(*`	`the declarations (and axioms) of the spec`	`*)`
`sp_protocol : eva_lprotocol;`	`(*`	`the messages of the spec`	`*)`
`sp_valuedcl : eva_ldcl list;`	`(*`	`declarations of values (for the session domains) in the spec`	`*)`
`sp_sessions : eva_lsession list;`	`(*`	`the session defined in the spec`	`*)`
`sp_statements : eva_lstatement list;`	`(*`	`the hypotheses and formulas in the spec`	`*)`

}

Top level container for a protocol specification in EVA syntax.

The fields declarations, valuedcl, sessions, statements contain exact copies of declarations in EVA concrete syntax.

The messages and instructions of the protocol (field protocol) may be presented in two ways:

one single list defining all the processes,
one seperate list for each process (i.e. each principal).