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.

(<PType> <Kind> <Ident>)

1.1.1.

<Kind>

const | var

1.1.2.

<PType>

principal (controls <Principal>)*

1.2

(<Type> <Kind> <Ident>)

1.2.1.

<Type>	:=		<ConsType>
		\|	<DepType>

1.2.1.1.

nonce

stkey

term

1.2.1.2.

<DepType>	:=		ltkey <Principal>*
		\|	pubkey <Principal>
		\|	privkey <Principal>

1.3.

<CompositeTerm>	:=		(<Function> <Exp>+)
		\|	(tuple <Exp>*)

1.3.1.

(<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.

2.1.

(<Kind> <Ident>)

2.2.

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.

agent

3.2.

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.

(seq <Program>*)

(par <Program>*)

4.

(process <Agent>+)

5.

<Run>

(<RunType> <Edge>*)

5.1.

run

5.2.

<Edge>	:=	(map <RecvRef> <SendRef>)
<RecvRef>	:=	(recvref <Principal> <Ident>)
<SendRef>	:=	(sendref <Principal> <Ident>)

6.

(protocol <ProtocolDescription> <Process> <Security>)

6.1.

6.3.