0.
<Ident> := <symbol>*
<Nat> := <numeral>*
<String> := <symbol>*
1.
<Exp> := <AtomExp>
| <CompositeTerm>
<AtomExp> := <Principal>
| <AtomTerm>
1.1.
<Principal> := (<PType> <Kind> <Ident>)
1.1.1.
<Kind> := const | var
1.1.2.
<PType> := principal (controls <Principal>)*
1.2
<AtomTerm> := (<Type> <Kind> <Ident>)
1.2.1.
<Type> := <ConsType>
| <DepType>
1.2.1.1.
<ConsType> := nonce | stkey | term
1.2.1.2.
<DepType> := ltkey <Principal>*
| pubkey <Principal>
| privkey <Principal>
1.3.
<CompositeTerm> := (<Function> <Exp>+)
| (tuple <Exp>*)
1.3.1.
<Function> := (<OutType> <InType> <Kind> <Parameters> <Ident>)
1.3.1.
<OutType> := encr | sig | hash | function // more??
<InType> := <Nat> // arity
<Parameters> := (parameters <Exp>*)
<InParameters> := (inparameters <Exp>*)
<OutParameters> := (outparameters <Exp>*)
1.4.
<BTerm> := (boolean <Exp> == <Exp>)
2.
<Action> := <AtomAction>
| <CompositeAction>
2.1.
<AtomAction> := (<Kind> <Ident>)
2.2.
<CompositeAction> := <InternalAction> | <ExternalAction>
2.2.1.
<InternalAction> := (new <ConsType> var <Ident>)
| (match <Exp> <Exp>) // refine this
| (cond <Bterm> <Action>)
2.2.2.
<ExternalAction> := (send <Principal> <Principal> <Exp>)
| (receive (principal var <Ident>)
(principal var <Ident>)
(term var <Ident>))
3.
<Agent> := (<AgentType> <AgentDescription> <Program>)
3.1.
<AgentType> := agent
3.2.
<AgentDescription> := <Principal> <InParameters> <OutParameters> <Spec>
3.2.1.
<Spec> := (spec <String>)
specifies the axioms that the agent uses in her reasoning.
need to refine this category to the s-exp grammar suitable to
translate for theorem provers.
3.3.
<Program> := <Action>
| (seq <Program>*)
| (par <Program>*)
4.
<Process> := (process <Agent>+)
5.
<Run> := (<RunType> <Edge>*)
5.1.
<RunType> := run
5.2.
<Edge> := (map <RecvRef> <SendRef>)
<RecvRef> := (recvref <Principal> <Ident>)
<SendRef> := (sendref <Principal> <Ident>)
6.
<Protocol> := (protocol <ProtocolDescription> <Process> <Security>)
6.1.
<ProtocolDescription> := <Ident> <Parameters>
6.3.
<Security> := <Run>+ <Spec>