# Coding the reduction in spi-calculus

Coding the reduction in spi-calculus

José M. Rodríguez Caballero, University of Tartu

## ABSTRACT

ABSTRACT

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

## Motivation

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?

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"

Basic data structure: "object"

## Creating a new 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

Example

In[]:=

rose=NewObject["flower",Import["ExampleData/rose.gif"]]

Out[]=

flower,

## Question whether some data is an object

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.

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

Example

In[]:=

ObjectQ[rose]

Out[]=

True

## Type of an object

Type of an object

The type of an object.

In[]:=

TypeObject[x_]:=First[x]

### Example

Example

In[]:=

TypeObject[rose]

Out[]=

flower

## Value of an object

Value of an object

The value of an object.

In[]:=

ValueObject[x_]:=Last[x]

### Example

Example

In[]:=

ValueObject[rose]

Out[]=

## Ill-defined object

Ill-defined object

The object FailureObject[] is used to indicate that some function concerning objects is ill-defined.

In[]:=

FailureObject[]:={"failure",}

### Example

Example

In[]:=

FailureObject[]

## Conditional definition

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[].

### Example

Example

I recall the object rose.

Because rose+rose is not an object

the following conditional definition returns that the result is ill-defined.

## Conditional properties

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

### Example

Example

The object rose contains an image.

The number 5 contains an image.

## Refining predicates by mean of the type

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.

### Example

Example

# Terms of spi-calculus

Terms of spi-calculus

## Checking terms

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

Name

### Example

Example

NameRose is a term,

but rose is not a term

## Variable

Variable

### Example

Example

## Number

Number

Zero:

Successor:

PredTerm is auxiliary (predecessor function).

### Examples

Examples

## Pair

Pair

### Examples

Examples

## Encryption

Encryption

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

### Example

Example

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

# Processes of spi-calculus

Processes of spi-calculus

## Checking processes

Checking processes

## Nil

Nil

This process consists in doing nothing.

### Example

Example

## Output

Output

### Example

Example

The rose is sent throughout internet.

The name "Oscar Wilde" is send via internet.

## Input

Input

### Example

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

Parallel composition

### Example

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

Replication

### Example

Example

The process RoseProtocol is repeated.

## Restriction

Restriction

### Example

Example

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

## Match

Match

### Example

Example

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

## Pair Splitting

Pair Splitting

### Example

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.

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

Case

### Example

Example

If t = 0 then PairRepRoseProtocol else MatchRepRoseProtocol.

## Decryption

Decryption

### Example

Example

# Substitution in spi-calculus

Substitution in spi-calculus

## Substitution in terms

Substitution in terms

### Examples

Examples

## Substitution in processes

Substitution in processes

### Examples

Examples

# Reduction in spi-calculus

Reduction in spi-calculus

## Reduction relation

Reduction relation

# References

References

## Main reference

Main reference

The present implementation of a part of spi-calculus was based on the following paper:

# Thank you for listening

Thank you for listening