Semantics of Applied Pi-Calculus

⚠️

This page is not part of the curriculum

Symbolic Cryptography

We consider cryptography as fully reliable - abstract everything away.

Example:

$\text{dec}(\text{enc}(M,K)K) \rarr M$

$\operatorname{ver}(\operatorname{sign}(x, s k(k)), v k(k)) \rarr x$

The Applied Pi-Calculus has a signature $\Sigma$ that consists of a 2 finite sets:

constructors i.e. $(\text{enc, sign})$

destructors i.e. $(\text{dec, ver})$

Destructors

Typical rules:

$\operatorname{fst}(\operatorname{pair}(x, y)) \rightarrow x$

$\operatorname{snd}(\operatorname{pair}(x, y)) \rightarrow y$

$\operatorname{dec}(\operatorname{enc}(x, y), y) \rightarrow x$

$\operatorname{deca}(\operatorname{enca}(x, \operatorname{ek}(y)), \operatorname{dk}(y)) \rightarrow x$

$\operatorname{ver}(\operatorname{sign}(x, \operatorname{sk}(y)), v k(y)) \rightarrow x$

They have evaluation rules :

$\sigma$ : variables $\mapsto$ terms (Substitution)

Examples

$\sigma=\{\operatorname{pair}(n, m) / x, k / y\}$

$\operatorname{ver}(\operatorname{sign}(\operatorname{pair}(n, m), \mathrm{sk}(k)), v k(k)) \Downarrow \text{pair}(n, m)$

The equality can be tested through: $\operatorname{eq}(x, x) \Downarrow x$

Equational Theory

is identified by signature $\Sigma$ .

We write $\Sigma \vdash M=N$

iff $M$ is equal to $N$ in the equational theory.

Processes

Almost identical to Pi-Calculus:

📎 (Original) Pi-Calculus

$P, Q, R::=$

$\operatorname{in}(c, x). P$ Receive on channel $c$ , bind result to $x$ , run $P$

$\text {out}(c, x) . P$ Send value of $y$ to channel $x$ , run $P$ - $x$ is then bound in $P$

$0$ Terminate process

$P \mid Q$ Run $P$ and $Q$ simultaniously

$! P$ Repeatedly generate copies of $P$

$\text {new } a.P$ Create a new variable $a$ , which is then bound in $P$

$\text {let } x=g\left(M_{1}, \ldots, M_{n}\right) \text { in } P \text { else } Q$

Guard + Pattern matching and binding a name (= value) to a variable

in $P$ or executing $Q$ if guard condition is not met.

Free- vs. Bound-Names

Free names are public, bound names are (initially) private.

If $P$ is closed, it does not have free variables.

We denote free / bounded names in $P$ as:

$\text{fn}(P)$ free name

$\text{bn}(P)$ bound name

$\text{fv}(P)$ free variable

$\text{bv}(P)$ bound variable

Operational Semantics

Reduction Relation $\rarr$

Describes the communication. (Internal Reduction)

$\text {out}(N, M). Q \mid \text{in}(N^{\prime}, x) .P ~~~ \rightarrow ~~~ Q \mid P\{M / x\}$
I/O: if $\Sigma \vdash N=N^{\prime}$ then the received $M$ in $P$ should be binded to $x$

$\text {let } x=g(M_{1}, \ldots, M_{n}) \text { in } P \text { else } Q\rightarrow P\{M / x\}$
$\text { if } g\left(M_{1}, \ldots, M_{n}\right) \Downarrow M$
$\text { if } \nexists M . g(M_{1}, \ldots, M_{n}) \downarrow M$ then $Q$ is executed independently

$! P \rightarrow P \mid ~! P$

$P \rightarrow Q \Rightarrow P \mid R \rightarrow Q \mid R$

$P \rightarrow Q \Rightarrow \text { new } a . P \rightarrow \text { new } a . Q$

$(P^{\prime} \equiv P, ~ P \rightarrow Q, ~~Q \equiv Q^{\prime}) ~~\Rightarrow ~~P^{\prime} \rightarrow Q^{\prime}$

Structural Equivalence $\equiv$

is the smallest equivalence relation on processes through renaming names and variables so that:

$P \mid \mathbf{0} \equiv P$

$P\mid Q \equiv Q \mid P$

$(P \mid Q)|R \equiv P|(Q \mid R)$

$\text { new } a \text { .new } b . P \equiv \text { new } b \text { .new } \text { a. } P$

$\textcolor{pink}{\text { new } a.(P \mid Q) \equiv P \mid \text { new } a.Q \quad \text { if } a \notin \operatorname{fn}(P)}$
because if $P \equiv Q \Rightarrow \text { new } a.P \equiv \text { new } a . Q$
goal: preventing unintentional leaking of secrets