// CODE FOR THESIS FIGURE 4.2

// Protocol BB84: quantum key distribution VERSION 3.0
// By N. Papanikolaou

// EAVESDROPPING ATTACK : Random substitution

probabilistic

// Reading correct value with wrong basis:
//prob LUCKY = 0.5;
prob LUCKY;
// With what probability does Eve put a 0 on channel?
prob REPLACE = 0.5;
// number of bits to transmit
const N;


// Eavesdropping attack: Eve replaces 0 with probability REPLACE on channel and 1 with probability 1-REPLACE
// She uses the same probabilities to replace channel basis
module Channel
ch_state : [0..6];
ch_bas : [0..1];
ch_bit : [0..1];

[aliceput] 	(ch_state=0) -> (ch_state'=1) & (ch_bas'=al_bas) & (ch_bit'=al_bit);
[evemeasure] 	(ch_state=1) & (ch_bas=eve_bas) -> (ch_state'=2);
[evemeasure] 	(ch_state=1) & (ch_bas!=eve_bas) -> LUCKY : (ch_state'=2) & (ch_bit'=ch_bit) + (1-LUCKY) : (ch_state'=2) & (ch_bit'=1-ch_bit);
[eveget]	(ch_state=2) -> (ch_state'=3);
[eveput]	(ch_state=3) -> REPLACE : (ch_state'=4) & (ch_bit'=0) + (1-REPLACE) : (ch_state'=4) & (ch_bit'=1);
[eveputbasis]	(ch_state=4) -> REPLACE : (ch_state'=5) & (ch_bas'=0) + (1-REPLACE) : (ch_state'=5) & (ch_bas'=1);
//[bobmeasure]	(ch_state=4) -> (ch_state'=5);
//[bobmeasure]	(ch_state=4) & (ch_bas!=bob_bas) -> LUCKY : (ch_state'=5) & (ch_bit'=ch_bit) + (1-LUCKY) : (ch_state'=5) & (ch_bit'=1-ch_bit);
[bobget]	(ch_state=5) -> (ch_state'=0);
endmodule

module Alice
al_state : [0..5];
al_index : [1..N];
al_bas : [0..1];
al_bit : [0..1];

[]		(al_state=0) & (eve_state>0) -> (al_state'=1) & (al_bas'=0);
[]		(al_state=0) & (eve_state>0) -> (al_state'=1) & (al_bas'=1);
[]		(al_state=1) -> (al_state'=2) & (al_bit'=0);
[]		(al_state=1) -> (al_state'=2) & (al_bit'=1);
[aliceput]	(al_state=2) -> (al_state'=3);
[reveal]	(al_state=3) -> (al_state'=4);
[loop]		(al_state=4) & (al_index<N) -> (al_state'=0) & (al_index'=al_index+1);
[loop]		(al_state=4) & (al_index=N) -> (al_state'=5);
[stop]		(al_state=4) -> (al_state'=4);
[stop]		(al_state=5) -> (al_state'=5);
endmodule

module Bob
bob_state : [0..7];
bob_bas : [0..1];
bob_bit : [0..1];

[]		(bob_state=0) & (eve_state>0) -> (bob_state'=2) & (bob_bas'=0);
[]		(bob_state=0) & (eve_state>0) -> (bob_state'=2) & (bob_bas'=1);
//[bobmeasure]	(bob_state=1) -> (bob_state'=2);
[bobget]	(bob_state=2) & (bob_bas=ch_bas) -> (bob_state'=3) & (bob_bit'=ch_bit);
[bobget]	(bob_state=2) & (bob_bas!=ch_bas) -> LUCKY : (bob_bit'=ch_bit) & (bob_state'=3) + (1-LUCKY) : (bob_bit'=1-ch_bit) & (bob_state'=3);
[reveal]	(bob_state=3) & (bob_bas!=al_bas) -> (bob_state'=4); // bob used different basis from alice
[reveal]	(bob_state=3) & (bob_bas=al_bas) & (bob_bit=al_bit) -> (bob_state'=4);
[reveal]	(bob_state=3) & (bob_bas=al_bas) & (bob_bit!=al_bit) -> (bob_state'=7);
[loop]		(bob_state=4) & (al_index<N) -> (bob_state'=0);
[loop]		(bob_state=4) & (al_index=N) -> (bob_state'=6);
[stop]		(bob_state=6) -> (bob_state'=6); // no eavesdropping detected
[stop]		(bob_state=7) -> (bob_state'=7); // eavesdropping detected
endmodule


module Eve
eve_state : [0..4];
eve_bas : [0..1];
eve_bit : [0..1];

[]		(eve_state=0) -> (eve_state'=1) & (eve_bas'=0);
[]		(eve_state=0) -> (eve_state'=1) & (eve_bas'=1);
[evemeasure]	(eve_state=1) -> (eve_state'=2);
[eveget]	(eve_state=2) & (eve_bas=ch_bas) -> (eve_state'=3) & (eve_bit'=ch_bit);
[eveget]	(eve_state=2) & (eve_bas!=ch_bas) -> LUCKY : (eve_state'=3) & (eve_bit'=ch_bit) + (1-LUCKY) : (eve_state'=3) & (eve_bit'=1-ch_bit);
[eveput]	(eve_state=3) -> (eve_state'=4);
[eveputbasis]   (eve_state=4) -> (eve_state'=0);
endmodule