CAPSL Syntax

This appendix has an informal presentation of the CAPSL concrete syntax and some information about the parser. (4/4/00)

Informal Grammar

In this grammar, curly brackets { } indicate a sequence of one or more of the enclosed item. A vertical bar | separates choices. Optional items are enclosed in square brackets [ ]. Literal tokens appear enclosed in single quotes ', except for keywords, which are all caps. Implementations may permit keywords in lower case or mixed case.

There is a general meta-rule for forming non-terminals representing lists of items separated by commas:

x_list:
   x | x ',' x_list

Comments in CAPSL (and in this grammar) are surrounded by /* and */; for example, /* this is a comment */.

The grammar permits constructs that are illegal for semantic reasons, such as improper ordering or type inconsistency. The grammar also permits some illegal constructs that could have been eliminated with a more elaborate grammar, but can also be handled by later checks. An example is that the % operator should be used only in message fields.

Identifiers are a sequence of alphabetic characters and digits, and may also contain the underline _ character. An identifier that consists solely of digits is a number.

specification:
   {protocol | typespec | environment}

protocol:
   PROTOCOL ident ';'
   {declaration}
   [ASSUMPTIONS
	{assertion ';'}]
   MESSAGES
      phrase_seq
   [GOALS
	{assertion ';'}]
   END;

typespec:
   TYPESPEC ident ';'
   {declaration}
   AXIOMS {statement ';'}
   END;

environment:
   ENVIRONMENT ident ';'
   {declaration}
   [AXIOMS
      {statement ';'}]  
   {agent}
   [EXPOSED term_list ';']
   [ORDER order ';']
   END;

agent:
   AGENT ident HOLDS
      {equation ';'}

order:
   ident            /* of agent */
   | 
   '(' order ';' order ')' 
   | 
   '(' order '||' order ')'

declaration:
   IMPORTS ident_list ';'
   |
   FUNCTIONS {func_dec}
   |
   VARIABLES {variable_dec}
   |
   CONSTANTS {variable_dec}
   |
   DENOTES {equation [':' ident_list] ';'}
   |
   TYPES {type_dec}

assertion:
   HOLDS ident ':' ident_list
   |
   BELIEVES ident ':' assertion
   |
   KNOWS ident ':' assertion
   |
   ASSUME assertion     /* as an action */
   |
   PROVE assertion      /* as an action */
   |
   SECRET ident [':' ident_list]
   |
   AGREE ident_list ':' ident_list '|' ident_list
   |
   PRECEDES ident ':' ident '|' ident_list
   |
   statement

statement:
   logicstmt
   |
   IF logicstmt THEN simplestmt [ELSE simplestmt] ENDIF
   | 
   INVERT term ':' ident | term_list

logicstmt:
   simplestmt
   |
   simplestmt AND simplestmt
   |
   NOT '(' simplestmt ')'

simplestmt:
   equation 
   | 
   term  

equation:
   term '=' term

variable_dec:
   ident_list ':' ident [',' property_list] ';'

type_dec:
   ident_list [':' ident] ';'

func_dec:
   ident '(' ident_list ')' ':' ident [',' property_list] ';' 

phrase_seq:
	phrase
	|
	phrase ['/'] phrase_seq   /* see text for use of '/' */

phrase:
   [{action ';'}]
   message
   [{action ';'}]
   |
   invocation
   |
   selection

action:
   equation | ASSUME assertion | PROVE assertion

invocation:
   INCLUDE ident ';'    /* naming a protocol */

selection:
   IF statement THEN phrase ELSE phrase ENDIF ';'

message:
   [number '.'] ident '->' ident ':' term_list ';' 

property:
   CRYPTO | FRESH | RANDOM | PRIVATE | EXPOSED | ASSOC | COMM

term:
   ident
   |
   functioncall
   |
   bracket
   |
   lowe
   |
   paren

functioncall :
   ident '(' term_list ')'

/* arithmetic expressions with +, -, *, /, and ^
(for exponentiation) are supported, and
treated as function calls on pls, mns, etc. */

bracket:
   '{' term_list '}' ['''] [term]     /* single quote for decrypt */
   |
   '[' term_list ']' ['''] [term]

lowe:
   term '%' term

paren:
   '(' term ')'

Parser

There is a Java applet parser that was generated using JavaCC; it produces a parse tree consistent with the abstract syntax. There is a type checker that is not yet available as an applet. The program will be further developed into a CIL translator. To use the parser applet, type or paste a CAPSL specification into the upper window and press the Parse button.

The JavaCC source, showing the grammar, is in the file capsl.jj.