Language
--------

language	:= (<def>)*
def		:= (<directive> | <protocol> | <rundef> | <unstrusted>)

//directive	:= <dir_require>
//dir_require	:= require <filename>;

protocol	:= protocol <protocolname> ( <rolelist> ) { <roledef>* } optsc
protocolname	:= <id>

intruderknow	:= public <termlist>;
roledef		:= role <rolename> { <actions> } optsc
rolename	:= <id> 
actions		:= (<action>;)+
action		:= (<read> | <send> | <claim>)
decl		:= (<const> | <var>)+
const		:= const <termlist> [ : <typeterm> ];
var		:= var <termlist> [ : <typelist> ];

read		:= read [_<label>]  (<term>,<term>,<term>);
send		:= send [_<label>]  (<term>,<term>,<term>);
claim		:= claim [_<label>] (<term>,<termlist>);
label		:= <id>;

rundef		:= <protocolname>.<rolename> ( <instancelist> ) ;
instancelist	:= (<agent>|<typeterm>)*

agent		:= <term>
typeterm	:= <term>
typelist	:= <termlist>

untrusted	:= untrusted <termlist>;

termlist	:= <term> [, <termlist>]
term		:= (<baseterm> | <encterm> | <tupleterm> | <function>)
encterm		:= { <term> } <term>
function	:= <term> ( <term> )
baseterm	:= (<variable> | <const>)
variable	:= <id>
const		:= <id>

optsc		:= [ ; ]
id		:= (<digit>|<uppercase>|<lowercase>)+