In "Mobile Values, New Names, and Secure Communication", Abadí and Fournet describe thet Applied-$\pi$-Calculus. Although I understood a great part of the description of the Applied $\pi$-Calculus, I'm still a bit confused as to what exactly its formal semantics consists of.
The authors define (on page 2):
A signature $\Sigma$ consists of a finite set of function symbols, such as
f
,encrypt
, andpair
m each with an arity.
On page 3, they say that
Given a signature $\Sigma$, we equip it with an equational theory, that is, with an equivalence relation on terms that is closed under substitution of terms for variables.
Then they proceed, still on page 3, to define Structural equivalence, which also is an equivalence relation, but defined on extended processes and not terms.
So after reading the paper a number of times and consulting some other resources on the Internet, I have concluded that the semantics of the $\pi$-Calculus depends on a given signature (and hence is "parametrized" in a sense); and that it is composed of:
- the signature and its equational theory, which is provided by us, depending on the application context (I may include symmetric cryptography functions and some equations modeling their behavior, and no asymmetric constructions at all, for example);
- the structural equivalence relation for processes;
- the internal reduction relation (structural semantics used for plain processes);
- the reduction relation including interaction with the environment.
Is this correct, or did I miss anything?