Reading prelude from pre.cap
Reading CAPSL spec from Standard Input
Type checking...
Wrote outable
Wrote outcil
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(Agent,type,ids(),Object,props()),
    symbol(Tspec,type,ids(),Spec,props()),
    symbol(Pspec,type,ids(),Spec,props()),
    symbol(Espec,type,ids(),Spec,props()),
    symbol(BOOLEAN,op,ids(),Tspec,props()),
    symbol(Boolean,type,ids(),Object,props()),
    symbol(true,op,ids(),Boolean,props()),
    symbol(false,op,ids(),Boolean,props()),
    symbol(and,op,ids(Boolean,Boolean),Boolean,props()),
    symbol(or,op,ids(Boolean,Boolean),Boolean,props()),
    symbol(not,op,ids(Boolean),Boolean,props()),
    symbol(if,op,ids(Boolean,Boolean,Boolean),Boolean,props()),
    symbol(FIELD,op,ids(),Tspec,props()),
    symbol(Field,type,ids(),Object,props()),
    symbol(Tape,type,ids(),Field,props()),
    symbol(Atom,type,ids(),Field,props()),
    symbol(Principal,type,ids(),Atom,props()),
    symbol(Nonce,type,ids(),Atom,props()),
    symbol(Number,type,ids(),Atom,props()),
    symbol(Nat,type,ids(),Atom,props()),
    symbol(cat,op,ids(Field,Field),Tape,props(ASSOC)),
    symbol(first,op,ids(Tape),Atom,props()),
    symbol(rest,op,ids(Tape),Field,props()),
    symbol(Al,var,ids(),Atom,props()),
    symbol(Xl,var,ids(),Field,props()),
    symbol(SKEY,op,ids(),Tspec,props()),
    symbol(Skey,type,ids(),Atom,props()),
    symbol(sha,op,ids(Field),Skey,props()),
    symbol(mac,op,ids(Skey,Field),Skey,props()),
    symbol(DSKE,op,ids(),Tspec,props()),
    symbol(se,op,ids(Skey,Atom),Atom,props()),
    symbol(sd,op,ids(Skey,Atom),Atom,props()),
    symbol(se,op,ids(Skey,Field),Field,props()),
    symbol(sd,op,ids(Skey,Field),Field,props()),
    symbol(Kl,var,ids(),Skey,props()),
    symbol(K1l,var,ids(),Skey,props()),
    symbol(XOR,op,ids(),Tspec,props()),
    symbol(xor,op,ids(Skey,Skey),Skey,props(ASSOC,COMM)),
    symbol(SKCS,op,ids(),Tspec,props()),
    symbol(Client,type,ids(),Principal,props()),
    symbol(Server,type,ids(),Principal,props()),
    symbol(Sl,var,ids(),Server,props()),
    symbol(Cl,var,ids(),Client,props()),
    symbol(csk,op,ids(Client),Skey,props(PRIVATE)),
    symbol(ssk,op,ids(Server,Client),Skey,props(PRIVATE)),
    symbol(MSKN,op,ids(),Tspec,props()),
    symbol(Node,type,ids(),Principal,props()),
    symbol(msk,op,ids(Node,Node),Skey,props(COMM,PRIVATE)),
    symbol(ARITH,op,ids(),Tspec,props()),
    symbol(1,op,ids(),Skey,props()),
    symbol(pls,op,ids(Skey,Skey),Skey,props(ASSOC,COMM)),
    symbol(mns,op,ids(Skey),Skey,props()),
    symbol(tms,op,ids(Skey,Skey),Skey,props(ASSOC,COMM)),
    symbol(div,op,ids(Skey,Skey),Skey,props()),
    symbol(exp,op,ids(Skey,Skey),Skey,props()),
    symbol(PKEY,op,ids(),Tspec,props()),
    symbol(Pkey,type,ids(),Atom,props()),
    symbol(PKl,var,ids(),Pkey,props()),
    symbol(PKIl,var,ids(),Pkey,props()),
    symbol(keypair,op,ids(Pkey,Pkey),Boolean,props(COMM)),
    symbol(SPKE,op,ids(),Tspec,props()),
    symbol(ped,op,ids(Pkey,Atom),Atom,props()),
    symbol(ped,op,ids(Pkey,Field),Field,props()),
    symbol(PPK,op,ids(),Tspec,props()),
    symbol(PKUser,type,ids(),Principal,props()),
    symbol(sk,op,ids(PKUser),Pkey,props(PRIVATE)),
    symbol(pk,op,ids(PKUser),Pkey,props()),
    symbol(PKUl,var,ids(),PKUser,props()),
    symbol(KEYAGREEMENT,op,ids(),Tspec,props()),
    symbol(Pval,type,ids(),Atom,props()),
    symbol(kap,op,ids(Skey),Pval,props()),
    symbol(kas,op,ids(Pval,Skey),Skey,props()),
    symbol(PKSeal,op,ids(),Tspec,props()),
    symbol(Pseal,type,ids(),Atom,props()),
    symbol(seal,op,ids(Pkey,Field),Pseal,props()),
    symbol(verify,op,ids(Pkey,Pseal,Field),Boolean,props()),
    symbol(TIMESTAMP,op,ids(),Tspec,props()),
    symbol(Timestamp,type,ids(),Atom,props()),
    symbol(LIST,op,ids(),Tspec,props()),
    symbol(List,type,ids(),Atom,props()),
    symbol(con,op,ids(Field,Field),List,props()),
    symbol(head,op,ids(List),Field,props()),
    symbol(tail,op,ids(List),Field,props()),
    symbol(Xl,var,ids(),Field,props()),
    symbol(Yl,var,ids(),Field,props()),
    symbol(ENDPRELUDE,op,ids(),Tspec,props()),
    symbol(endprelude,op,ids(),Boolean,props()),
    symbol(NSPK,op,ids(),Pspec,props()),
    symbol(A,pvar,ids(),PKUser,props()),
    symbol(B,pvar,ids(),PKUser,props()),
    symbol(Na,pvar,ids(),Nonce,props(CRYPTO,FRESH)),
    symbol(Nb,pvar,ids(),Nonce,props(CRYPTO,FRESH)),
    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(Na,roleA,3),
    slot(Na,roleB,2),
    slot(A,roleB,3),
    slot(Nb,roleB,4),
    slot(Nb,roleA,4)
  ),
  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)
  ),
  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(Na),
      facts(state(roleA,1,terms(A,B,Na)),msg(A,B,terms(ped(pk(B),cat(Na,A)))))
    ),
    rule(
      facts(state(roleB,0,terms(B)),msg(UNK,B,terms(ped(pk(B),cat(Na,A))))),
      ids(Nb),
      facts(
        state(roleB,2,terms(B,Na,A,Nb)),
        msg(B,A,terms(ped(pk(A),cat(Na,Nb))))
      )
    ),
    rule(
      facts(
        state(roleA,1,terms(A,B,Na)),
        msg(UNK,A,terms(ped(pk(A),cat(Na,Nb))))
      ),
      ids(),
      facts(state(roleA,3,terms(A,B,Na,Nb)),msg(A,B,terms(ped(pk(B),Nb))))
    ),
    rule(
      facts(state(roleB,2,terms(B,Na,A,Nb)),msg(UNK,B,terms(ped(pk(B),Nb)))),
      ids(),
      facts(state(roleB,3,terms(B,Na,A,Nb)))
    )
  ),
  goals(
    loc(nodes(node(roleA,3),node(roleB,3)),secret(Na,ids(A,B))),
    loc(nodes(node(roleA,3),node(roleB,3)),secret(Nb,ids(A,B))),
    loc(nodes(node(roleA,3),node(roleB,3)),precedes(B,A,ids(Na))),
    loc(nodes(node(roleA,3),node(roleB,3)),precedes(A,B,ids(Nb)))
  ),
  envs()
)