Authentication examples

These examples study a simple authentication protocol with a N bits password. The input is checked against the password; if the result is true the attacker can observe an output of 1; otherwise the output is 0. Here is the program for a 2 bits secret:

observable int1 o;
public int2 input:=0;
secret int2 password;
if (password==input)
then assign o:=1;
else assign o:=0;
fi
return;