Adecs - Vincent Cheval

A decision algorithm for proving symbolic equivalence of constraint systems

Description

The program decides symbolic trace equivalence where the inputs are given as deducible constraint systems.

Download

The program is written in Ocaml. The tar.gz file Adecs_v0.2.tar.gz contains

  • An executable for MacOS X : adecs
  • All the current source code and a MakeFile. You need Objective Caml ; and for the MacOS X users, you need Xcode, which is available on the Apple Web Site or on your (Snow) Leopard DVD.
  • Examples : We used several constraint systems as benchmarks. Some of them are well known protocols (like Needham-Schroeder, Handshake Protocol , EPT, etc), and others were mostly used to debug the tool.

You can download the previous version here : ADECS.tar.gz

Features

The current tool accepts any pair of constraint systems with the same structure (i.e. number of constraints, size of the frame, see the technical-report for more details), with the Dolev-Yao cryptographic primitives, and decides the symbolic equivalence between them. If they are not equivalent, the tool also gives a witness for the non-equivalence.

Here is the description of the program:

Synopsis

  • adecs [-witness] [-t title] -p path
  • adecs -example
  • adecs -help

Options

  • -t title : Display title at the beginning of the output. The standard title is : An example
  • -p path : This option is mandatory if -example or -help aren't used. The program will find the definition of the two constraint systems in the file located by path
  • -witness : Ask the program to display the witness of the non-equivalence if the constraint systems aren't in symbolic equivalence. This option may be sometimes a little bit slow in some specific inputs.
  • -example : Run the program on all examples in the directory Exemple (with the option -witness)
  • -help : Display the help

Changelog

Adecs_v0.2

  • Modification of the input format : The constraints and the frame can't be defined separatly now. We also add a new input format which follow the formalism of the technical report. The primitive enca was changed to aenc
  • The structure of the source code was completly changed. We renammed all rule files by their name in the paper (instead of r_1, r_2,...). Bug correction in several rules.
  • The witness of the non static equivalence was removed : There is still few bugs and it could give sometimes not a good witness. This feature will be available in the next version.

Example

Symbolic equivalence :Here's the example of a simple Handshake Protocol where the offline guessing attack is described

Constraints_System = 
{ 
	Constraints = 
	{
		enc(M,K) ||- enc(x,K)
		enc(M,K),enc(pa(x,x),K) ||- enc(pa(M,M),K)
	}
	
	Frame =
	{
		enc(M,K),enc(pa(x,x),K), K
	}
}

Constraints_System = 
{ 
	Constraints = 
	{
		enc(M,K) ||- enc(x,K)
		enc(M,K),enc(pa(x,x),K) ||- enc(pa(M,M),K)
	}
	
	Frame =
	{
		enc(M,K),enc(pa(x,x),K), K_2
	}
}

Thus, we obtain :

The constraint systems aren't in symbolic equivalence ! (done in 58 nodes)
One witness of the non-equivalence is given by the following recipe :
X_2(2) = ax_2
X_1(1) = ax_1
This recipe is solution of C_1 with a first order solution such that :
x = M
and it is also a solution of C_2 with a first order solution such that :
x = M
but the static equivalence isn't preserved

Satisfiability : The attack Man in the middle in the protocol of Needham-Schroeder. In this example, we show the new formalism :


Constraints_System = 
{ 
	Constraints = 
	{
		X_1[4] ||- aenc(pa(x,y),pub(B))
		X_2[5] ||- aenc(pa(Na,z),pub(A))
		X_3[6] ||- aenc(Nb,pub(B))
		X_4[6] ||- Nb
	}
	
	Frame =
	{
		ax_1 ->> P,
		ax_2 ->> pub(B), 
		ax_3 ->> pub(A), 
		ax_4 ->> aenc(pa(pub(A),Na),pub(P)),
		ax_5 ->> aenc(pa(y,Nb),x),
		ax_6 ->> aenc(z,pub(P))
	}
	
}

Constraints_System = 
{ 
}

Thus, we obtain :


The constraint systems aren't in symbolic equivalence ! (done in 32 nodes)
One witness of the non-equivalence is given by the following recipe :
X_4(6) = adec(ax_6, ax_1)
X_3(6) = aenc(adec(ax_6, ax_1), ax_2)
X_2(5) = ax_5
X_1(4) = aenc(adec(ax_4, ax_1), ax_2)
This recipe is only a solution on C_1 with a first order solution such that :
y = Na
x = pub(A)
z = Nb

As you can see, we only denote in a constraint its recipe variable. So for the first constraint, its recipe is X_1 and its support is equal to 4. The second constraint system is null. Remember that in this formalism, the recipe variables have to be the same in the both constraint systems, except where one of them is null (see the following example).


Constraints_System = 
{ 
	Constraints =
	{
		X_1[2] ||- x
		X_2[4] ||- A
		X_3[4] ||- A
		X_4[4] ||- z
	}

	Frame = 
	{ 
		ax_1 ->> enc(A,B), 
		ax_2 ->> C, 
		ax_3 ->> x, 
		ax_4 ->> pa(B,enc(x,D)) 
	}
}

Constraints_System = 
{ 
	Constraints =
	{
		X_1[2] ||- enc(x,y)
		X_2[4] ||- A
		X_3[4] ||- pa(C,D)
		X_4[4] ||- z
	}

	Frame = 
	{ 
		ax_1 ->> enc(A,B), 
		ax_2 ->> C, 
		ax_3 ->> x, 
		ax_4 ->> y 
	}
}