WOLFRAM NOTEBOOK

Insert New
Slide
​
Roboto
A
Slide Break Defaults…
​
Cell Actions
Window Options
Start Presentation
▼
Slide
1
of
40
​
​
​
​
​
​

Coding the reduction in spi-calculus

José M. Rodríguez Caballero, University of Tartu
​
​
Slide
2
of
40
​
​

ABSTRACT

We present an implementation of the reduction in spi-calculus using the Wolfram Language.
Slide
3
of
40
​
​

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.
Slide
4
of
40
​
​

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.
Slide
5
of
40
​
​
​
​
​
​

Basic data structure: "object"

Slide
6
of
40
​
​

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,
Slide
7
of
40
​
​

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
Slide
8
of
40
​
​

Type of an object

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

Example

In[]:=
TypeObject[rose]
Out[]=
flower
Slide
9
of
40
​
​

Value of an object

The value of an object.

Example

Slide
10
of
40
​
​

Ill-defined object

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

Example

Slide
11
of
40
​
​

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

I recall the object rose.
Because rose+rose is not an object
the following conditional definition returns that the result is ill-defined.
Slide
12
of
40
​
​

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

The object rose contains an image.
The number 5 contains an image.
Slide
13
of
40
​
​

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

Slide
14
of
40
​
​
​
​
​
​

Terms of spi-calculus

Slide
15
of
40
​
​

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.
Slide
16
of
40
​
​

Name

Example

NameRose is a term,
but rose is not a term
Slide
17
of
40
​
​

Variable

Example

Slide
18
of
40
​
​

Number

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

Examples

Slide
19
of
40
​
​

Pair

Examples

Slide
20
of
40
​
​

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".
Slide
21
of
40
​
​
​
​
​
​

Processes of spi-calculus

Slide
22
of
40
​
​

Checking processes

Slide
23
of
40
​
​

Nil

This process consists in doing nothing.

Example

Slide
24
of
40
​
​

Output

Example

The rose is sent throughout internet.
The name "Oscar Wilde" is send via internet.
Slide
25
of
40
​
​

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.
Slide
26
of
40
​
​

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").
Slide
27
of
40
​
​

Replication

Example

The process RoseProtocol is repeated.
Slide
28
of
40
​
​

Restriction

Example

Taking the channel of communication in SendChannel as a bounded variable.
Slide
29
of
40
​
​

Match

Example

If the Student is the rose's owner, then do process RepRoseProtocol.
Slide
30
of
40
​
​

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.
Slide
31
of
40
​
​

Case

Example

If t = 0 then PairRepRoseProtocol else MatchRepRoseProtocol.
Slide
32
of
40
​
​

Decryption

Example

Slide
33
of
40
​
​
​
​
​
​

Substitution in spi-calculus

Slide
34
of
40
​
​

Substitution in terms

Examples

Slide
35
of
40
​
​

Substitution in processes

Examples

Slide
36
of
40
​
​
​
​
​
​

Reduction in spi-calculus

Slide
37
of
40
​
​

Reduction relation

Slide
38
of
40
​
​
​
​
​
​

References

Slide
39
of
40
​
​

Main reference

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

Thank you for listening

Wolfram Cloud

You are using a browser not supported by the Wolfram Cloud

Supported browsers include recent versions of Chrome, Edge, Firefox and Safari.


I understand and wish to continue anyway »

You are using a browser not supported by the Wolfram Cloud. Supported browsers include recent versions of Chrome, Edge, Firefox and Safari.