Pda S-Expression Grammar

Version from October 17, 2005

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>