What is a “name/variable of base type” in applied $\pi$-calculus?

Question

I'm studying the articleVerifying privacy-type properties of electronic voting protocols which uses Applied $\pi$-calculus to formalize voting protocols and verifies some privacy-related properties.

In certain parts of the paper they define some transformations over processes which are defined inductively. For example:

Definition (Process $P^{ch}$) Let $P$ be a plain process and $ch$ a channel name. We define $P^{ch}$ as follows:

• $0^{ch} \equiv 0$
• $(P|Q)^{ch} \equiv P^{ch} \equiv Q^{ch}$
• $(\nu n.P)^{ch} \equiv \nu n.out(ch, n).P^{ch}$ when $n$ is name of base type
• $(\nu n.P)^{ch} \equiv \nu n.P^{ch}$ otherwise
• $\ldots$

The idea is that they want to model a voter, which is a process, that wants to provide information about how he voted to the attacker (think: guy $X$ buys the vote of $Y$ and wants a "receipt" to be sure that $Y$ voted how he wanted). What I don't understand exactly is when is that $n$ a "name of base type"?

I've read the article Mobile Values, New Names, and Secure Communication where Applied $\pi$-calculus was first defined but here they just say that they assume that terms have some kind of type-system behind the scenes and the only thing they say is that the type system must include the type $\texttt{Channel}\langle \tau\rangle$ for every type $\tau$.

So, does the condition "when $n$ is name of base type" simply means "$n$ is not the name of a channel"? This would make sense, because in formalizing these protocols it is assumed that there exists some private channels between voter and authorities that the attacker can not eavesdrop due to physical limitations (they represent the voting booth).

Answer 1

“Base type” is a type that isn't built from other types. Types built from other types include data structures (e.g. lists, arrays, pairs, …), functions, etc. In the context of the pi-calculus, base types exclude channel types.

Some typical example of base types in practice are integers, booleans, floating point, etc. From a theoretical point of view, a base type is one that is a base case in the type grammar, and more generally this implies that there's no type equation that relates this type with “interesting” constructed types. For example, a value of a base type is not a channel or anything that contains a channel.

“$n$ is name of base type” here means that $n$ is a channel that transports opaque values, as opposed to a channel that can transport a channel name. So $(\nu n.P)^{ch} \equiv \nu n.\mathsf{out}(ch, n).P^{ch}$ holds only when the output operation isn't extruding any of the channels in $P$.