Coding the reduction in spi-calculus​
​José M. Rodríguez Caballero, University of Tartu

ABSTRACT

We present an implementation of the reduction in spi-calculus using the Wolfram Language.

Motivation

Variations of π-calculus have been implemented in general proof assistants like Coq and Isabelle/HOL, and in cryptographically specific softwares like ProVerif. In this presentation we explore an implementation of spi-calculus in the Wolfram Language.

Why the Wolfram Language?

The Wolfram Language is a general multi-paradigm computational language which emphasizes symbolic computation, rule-based programming and functional programming.
In the modest opinion of the speaker (far from being an expert opinion), the above mentioned features are precisely the features needed in symbolic cryptography. Accepting this premise, it makes sense to explore the potential of the Wolfram Language in symbolic cryptography.

Basic data structure: "object"

Creating a new object

An object is a pair consisting of a string and data that we declare to be type of this string.
In[]:=
NewObject[t_,v_]:={t,v}

Example

In[]:=
rose=NewObject["flower",Import["ExampleData/rose.gif"]]
Out[]=
flower,


Question whether some data is an object

Input: a string x.
​
Output: a Boolean.
​
Meaning: ObjectQ[x] is true if and only if x is an object, i.e., x = NewObject[t,v] for some string t and some data v.
In[]:=
ObjectQ[x_]:=If[ListQ[x],​​If[Length[x] == 2,​​If[StringQ[First[x]],​​True,​​False],​​False],​​False]

Example

In[]:=
ObjectQ[rose]
Out[]=
True

Type of an object

The type of an object.
In[]:=
TypeObject[x_]:=First[x]

Example

In[]:=
TypeObject[rose]
Out[]=
flower

Value of an object

The value of an object.
In[]:=
ValueObject[x_]:=Last[x]

Example

In[]:=
ValueObject[rose]
Out[]=

Ill-defined object

The object FailureObject[] is used to indicate that some function concerning objects is ill-defined.
In[]:=
FailureObject[]:={"failure",}

Example

In[]:=
FailureObject[]
Out[]=
{failure,Null}

Conditional definition

The function Define[x,P,F] is used to define a function under the assumption that x satisfies the predicate P. If x does not satisfy the predicate P, the function returns FailureObject[].
In[]:=
Define[x_,P_,F_]:=If[P[x],​​F,​​FailureObject[]]

Example

I recall the object rose.
In[]:=
rose
Out[]=
rose,

In[]:=
Define[rose,ObjectQ,rose+rose]
Out[]=
2flower,

Because rose+rose is not an object
In[]:=
ObjectQ[rose+rose]
Out[]=
False
the following conditional definition returns that the result is ill-defined.
In[]:=
Define[rose+rose,ObjectQ,rose+rose]
Out[]=
{failure,Null}

Conditional properties

The function NewProperty[x,P,Q] returns the Q[x] if x satisfies the predicate P, and its returns False otherwise. This function is necessary, because Q[x] may be ill-defined if x does not satisfies P. The name of this function is motivated by the intuition that we take an object x satisfying P and we want to know whether it satisfies Q (a new property).
In[]:=
NewProperty[x_,P_,Q_]:=If[P[x],Q[TypeObject[x],ValueObject[x]],False]

Example

The object rose contains an image.
In[]:=
NewProperty[rose,ObjectQ,Function[{t,v},ImageQ[v]]]
Out[]=
True
The number 5 contains an image.
In[]:=
NewProperty[5,ObjectQ,Function[{t,v},ImageQ[v]]]
Out[]=
False

Refining predicates by mean of the type

The function SubProperty[x,P,n] returns TypeObject[x]==n, assuming that x satisfies property P. The name of this function is motivated by the intuition that we have an object x, satisfying P and we are interested in knowing whether the type of this object is n.
In[]:=
SubProperty[x_,P_,n_]:=NewProperty[x,P,Function[{t,v}, t==n]]

Example

In[]:=
SubProperty[rose,ObjectQ,"flower"]
Out[]=
True
In[]:=
SubProperty[rose,ObjectQ,"animal"]

Terms of spi-calculus

Checking terms

We let a names of spi-calculus to be any data structure in the Wolfram language.
The values of variables are strings.
The values of numbers are positive integers.
The values of pairs are lists of length 2.
Given a data structure x, TermQ[x] is True if x is a term, otherwise it is false.

Name

Example

NameRose is a term,
but rose is not a term

Variable

Example

Number

Zero:
Successor:
PredTerm is auxiliary (predecessor function).

Examples

Pair

Examples

Encryption

The first variable is the key, the second variable is the message: {y}_x.

Example

The rose is encrypted. The key is "Press closer".

Processes of spi-calculus

Checking processes

Nil

This process consists in doing nothing.

Example

Output

Example

The rose is sent throughout internet.
The name "Oscar Wilde" is send via internet.

Input

Example

A channel of communication x is received from internet and a rose is send via this communication channel. For example, if x is substituted by "Oscar Wilde", then the rose is delivered to Oscar Wilde.

Parallel composition

Example

The Nightingale sends the channel "She" to the Student and the Student gives the rose to her friend (via the communication channel "She").

Replication

Example

The process RoseProtocol is repeated.

Restriction

Example

Taking the channel of communication in SendChannel as a bounded variable.

Match

Example

If the Student is the rose's owner, then do process RepRoseProtocol.

Pair Splitting

Example

Let (x, y) = M in OutputProcess[VarTerm["x"],VarTerm["y"],RoseProtocol].
​
Informally, if (x,y) = M, then send the message registered in VarTerm["y"] throughout the channel registered in VarTerm["x"], and then do RepRoseProtocol.

Case

Example

If t = 0 then PairRepRoseProtocol else MatchRepRoseProtocol.

Decryption

Example

Substitution in spi-calculus

Substitution in terms

Examples

Substitution in processes

Examples

Reduction in spi-calculus

Reduction relation

References

Main reference

The present implementation of a part of spi-calculus was based on the following paper:
Abadi, Martin, and Andrew D. Gordon. "A calculus for cryptographic protocols: The spi calculus." Information and computation 148.1 (1999): 1-70.