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