Relativistic implementation of the Needham-Schroeder public key protocol

by José M. Rodríguez Caballero
Update: November 23, 2020.
Abstract. We express a relativistic version of the Needham-Schroeder public key protocol using the graph-theoretical tools of the Wolfram Language.
Twitter: https://twitter.com/JosManu92295689

Preliminary Code


Needham-Schroeder public key protocol

Inertial frames.

We chose the units in such a way that the speed of light is c = 1.
Alice is at position {0, 0, 0} at time t = 0, her velocity vector is {0.1, 0, 0}. This reference frame is represented until t = 2, the discretization of ϵ = 0.1.
In[]:=
A:=Agent[{0,0,0},{0.1,0,0},0,2,0.1](*Alice,Red*)
Bob is at position {0.1, 0, 0} at time t = 0, her velocity vector is {0, 0.1, 0}. This reference frame is represented until t = 2, the discretization of ϵ = 0.1.
In[]:=
B:=Agent[{0.1,0,0},{0,0.1,0},0,2,0.1](*Bob,Blue*)
Server is at position {0, 0.1, 0} at time t = 0, her velocity vector is {0, 0, 0.1}. This reference frame is represented until t = 2, the discretization of ϵ = 0.1.
In[]:=
S:=Agent[{0,0.1,0},{0,0,0.1},0,2,0.1](*Server,Green*)
Association of strings with the agents.
In[]:=
SAssoc = <|"A"A, "B"B, "S"S|>;
Colors of the agents.
In[]:=
Colors=Join[Style[#,Red]&/@A,​​Style[#,Blue]&/@B,​​Style[#,Green]&/@S​​];

Causal influence

Causal influences among Alice, Bob and the Server will be represented by a graph G.
In[]:=
G=HighlightGraph[CausalInfluence[Join[A,B,S]],Colors];
Transitive reduction of G.
In[]:=
TransitiveReductionGraph[G]
Out[]=
The protocol will be represented as a list L of labeled arrows of a graph H, where the vertex are events. This graph will be automatically constructed in a way that it will respect causality, i.e., for any arrow from event u to event v we have that v is causally influenced by u.
In[]:=
L=WorldLine[WorldLine[WorldLine[FromMessages[{​​"A  S : (A, B)",​​"S  A : { pkB, B }skS",​​"A  B : { Na, A }",​​"B  S : (B, A)",​​"S  B : { pkA, A }skS",​​"B  A : { Na, Nb }pkA",​​"A  B : { Nb }pkB"​​},SAssoc,G],A,G],B,G],S,G];
In[]:=
H=HighlightGraph[Graph[First/@L,EdgeLabelsL],Colors];
Representation of the Needham-Schroeder public key protocol as the labeled graph H.
In[]:=
H
Out[]=
Causal influences belonging to H are represented in red, causal influences that do not belong to H are represented in blue.
In[]:=
HighlightGraph[Subgraph[G,VertexList[H]],EdgeList[H],EdgeLabelsL]
Out[]=
We check that the protocol respects the relativistic causality.
In[]:=
SubsetQ[EdgeList[G],EdgeList[H]]
Out[]=
True

References

Needham, Roger; Schroeder, Michael (December 1978). "Using encryption for authentication in large networks of computers". Communications of the ACM. 21 (12): 993–999. CiteSeerX 10.1.1.357.4298. doi:10.1145/359657.359659. S2CID 7704786.