CIL Abstract Syntax

The core of the CIL output is the set of multiset rewrite rules. There is also a symbol table containing type signatures and other information, and a slot table relating protocol variables to state fact argument positions. Axioms, assumptions, goals, and environment data are retained from the CAPSL. Assumptions and goals are localized by indicating the current state to which they apply. Eventually goals will be reduced to rule-oriented statements. Some of the axioms are equations needed for algebraic reductions.

Rules are omitted if they are the same as in the CAPSL abstract syntax.

CIL specifications are written out using a functional notation, in which node arg* is expressed as node(arg, arg, ...). There is a Java class treeparse available for re-parsing a CIL spec in this notation into a labelled-node parse tree data structure. There is an example of this notation below.

The Syntax

specification: CILspec symbols slots axioms assums 
                rules goals envs

env: env id agents exposed order

symbol: symbol ident status idents ident props

slot: slot term ident number  

status: op | pvar | var | type

prop: ident  /* CAPSL properties */

axioms: axioms stmt*

assums: assums locassert*

goals: goals locassert*

locassert: loc nodes assert

node: node ident number  /* ident is role, number is state label */

/* assert, stmt as in CAPSL abstract syntax */

rule: rule facts idents facts

fact: message | state

message: msg ident ident terms

state: state role label terms

term: fncall | ident

fncall: ident ( term* )

CIL Example: EKE

CILspec(
  symbols(
    symbol(Object,type,ids(),Object,props()),
    symbol(BASIC,op,ids(),Tspec,props()),
    symbol(Role,type,ids(),Object,props()),
    symbol(Spec,type,ids(),Object,props()),
    ...
    symbol(ENDPRELUDE,op,ids(),Tspec,props()),
    symbol(endprelude,op,ids(),Boolean,props()),
    symbol(EKE,op,ids(),Pspec,props()),
    symbol(A,pvar,ids(),Client,props()),
    symbol(B,pvar,ids(),Server,props()),
    symbol(Ra,pvar,ids(),Skey,props(FRESH,CRYPTO)),
    symbol(Rb,pvar,ids(),Skey,props(FRESH,CRYPTO)),
    symbol(Na,pvar,ids(),Nonce,props(CRYPTO,FRESH)),
    symbol(Nb,pvar,ids(),Nonce,props(CRYPTO,FRESH)),
    symbol(PA,pvar,ids(),Pval,props()),
    symbol(PB,pvar,ids(),Pval,props()),
    symbol(K,pvar,ids(),Skey,props()),
    symbol(T1,pvar,ids(),Field,props()),
    symbol(T2,pvar,ids(),Field,props()),
    symbol(T3,pvar,ids(),Field,props()),
    symbol(Test1,op,ids(),Espec,props()),
    symbol(Alice,op,ids(),Client,props()),
    symbol(Bob,op,ids(),Server,props()),
    symbol(Pa,op,ids(),Skey,props()),
    symbol(S12,op,ids(),Agent,props()),
    symbol(S13,op,ids(),Agent,props()),
    symbol(roleA,op,ids(),Role,props()),
    symbol(roleB,op,ids(),Role,props()),
    symbol(UNK,pvar,ids(),Principal,props())
  ),
  slots(
    slot(A,roleA,1),
    slot(B,roleA,2),
    slot(B,roleB,1),
    slot(Ra,roleA,3),
    slot(T1,roleA,4),
    slot(PA,roleB,2),
    slot(A,roleB,3),
    slot(Rb,roleB,4),
    slot(T2,roleB,5),
    slot(K,roleB,6),
    slot(Nb,roleB,7),
    slot(Nb,roleA,5),
    slot(PB,roleA,6),
    slot(K,roleA,7),
    slot(Na,roleA,8),
    slot(Na,roleB,8)
  ),
  axioms(
    eqn(first(cat(Al,Xl)),Al),
    eqn(rest(cat(Al,Xl)),Xl),
    invertible(cat(Al,Xl),Al,terms()),
    invertible(cat(Al,Xl),Xl,terms()),
    eqn(sd(Kl,se(Kl,Xl)),Xl),
    eqn(se(Kl,sd(Kl,Xl)),Xl),
    invertible(se(Kl,Xl),Xl,terms(Kl)),
    invertible(sd(Kl,Xl),Xl,terms(Kl)),
    eqn(xor(xor(Kl,Kl),K1l),K1l),
    invertible(xor(Kl,K1l),Kl,terms(K1l)),
    invertible(xor(Kl,K1l),K1l,terms(Kl)),
    eqn(ssk(Sl,Cl),csk(Cl)),
    if(keypair(PKl,PKIl),eqn(ped(PKIl,ped(PKl,Xl)),Xl),true),
    keypair(sk(PKUl),pk(PKUl)),
    invertible(ped(sk(PKUl),Xl),Xl,terms(pk(PKUl))),
    invertible(ped(pk(PKUl),Xl),Xl,terms(sk(PKUl))),
    eqn(kas(kap(Kl),K1l),kas(kap(K1l),Kl)),
    eqn(keypair(PKl,PKIl),verify(PKIl,seal(PKl,Xl),Xl)),
    eqn(head(con(Xl,Yl)),Xl),
    eqn(tail(con(Xl,Yl)),Yl),
    invertible(con(Xl,Yl),Xl,terms()),
    invertible(con(Xl,Yl),Yl,terms()),
    eqn(endprelude,true),
    eqn(Pa,csk(Alice))
  ),
  assums(loc(nodes(node(roleA,0),node(roleB,0)),holds(A,ids(B)))),
  rules(
    rule(facts(),ids(),facts(state(roleA,0,terms(A,B)))),
    rule(facts(),ids(),facts(state(roleB,0,terms(B)))),
    rule(
      facts(state(roleA,0,terms(A,B))),
      ids(Ra),
      facts(
        state(roleA,2,terms(A,B,Ra,se(csk(A),kap(Ra)))),
        msg(A,B,terms(A,se(csk(A),kap(Ra))))
      )
    ),
    rule(
      facts(state(roleB,0,terms(B)),msg(UNK,B,terms(A,se(ssk(B,A),PA)))),
      ids(Rb,Nb),
      facts(
        state(roleB,4,terms(B,PA,A,Rb,se(ssk(B,A),kap(Rb)),kas(PA,Rb),Nb)),
        msg(B,A,terms(B,se(ssk(B,A),kap(Rb)),se(kas(PA,Rb),Nb)))
      )
    ),
    rule(
      facts(
        state(roleA,2,terms(A,B,Ra,T1)),
        msg(UNK,A,terms(B,se(csk(A),PB),se(kas(PB,Ra),Nb)))
      ),
      ids(Na),
      facts(
        state(roleA,5,terms(A,B,Ra,T1,Nb,PB,kas(PB,Ra),Na)),
        msg(A,B,terms(A,se(kas(PB,Ra),cat(Na,Nb))))
      )
    ),
    rule(
      facts(
        state(roleB,4,terms(B,PA,A,Rb,T2,K,Nb)),
        msg(UNK,B,terms(A,se(K,cat(Na,Nb))))
      ),
      ids(),
      facts(
        state(roleB,6,terms(B,PA,A,Rb,T2,K,Nb,Na)),
        msg(B,A,terms(B,se(K,Na)))
      )
    ),
    rule(
      facts(
        state(roleA,5,terms(A,B,Ra,T1,Nb,PB,K,Na)),
        msg(UNK,A,terms(B,se(K,Na)))
      ),
      ids(),
      facts(state(roleA,6,terms(A,B,Ra,T1,Nb,PB,K,Na)))
    )
  ),
  goals(
    loc(nodes(node(roleA,6),node(roleB,6)),secret(K,ids())),
    loc(nodes(node(roleA,6),node(roleB,6)),precedes(B,A,ids(K,Nb))),
    loc(nodes(node(roleA,6),node(roleB,6)),precedes(A,B,ids(K,Na)))
  ),
  envs(
    environment(
      Test1,
      agents(
        agent(S12,eqns(eqn(A,Alice),eqn(B,Bob))),
        agent(S13,eqns(eqn(B,Bob)))
      ),
      exposed(terms(Pa)),
      order(par(S12,seq(S12,S12)))
    )
  )
)