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