// non-repudiation protocol (with malicious recipient) Markowitch & Roggeman [MR99]
// extension and modification of the PTA model from R. Lanotte, A. Maggiolo-Schettini and A. Troina [LMT05]
// malicious recipient

pta

// need to generate geometric distribution on the fly i.e. the value of n (the number of messages sent)
// as otherwise the recipient would have too much information - could use the value of n and 
// win with probability 1
// really motivation for partially observable adversaries, but this fixes the problem
// an alternative would be to make the adversary to make all its choices in advance
// but this would be more complicated

// possible changes/extensions:

// add a delay for the time to send a message from the originator
// or can we suppose the originator sends its message immediately?

// increase/vary the delays - can use this to show they do not influence zone based
// and how to use scaling to approximate for digital clocks

// note to self: the correctness of boundary region graph/corner based abstraction points
// to the fact it should be feasible to extend the digital clocks approach to deal with strict bounds

// constants
const double p; // parameter of geometric distribution (choose number of messages)
const int ad = 1; // min time to send an ack
const int AD = 5; // deadline (if ack not arrived then end protocol)

module originator

	// location of originator
	o : [0..4];
	// 0 - init
	// 1 - send
	// 2 - waiting
	// 3 - finished
	// 4 - error

	x : clock;

	invariant
		(o=0 => true) &
		(o=1 => x<=0) &
		(o=2 => x<=AD) &
		(o=3 => true) &
		(o=4 => true)
	endinvariant

	// init
	[req] o=0 -> (o'=1) & (x'=0); // receive a request from the recipient
	
	// send
	[message] o=1 & x<=0 -> (o'=2); // send first message immediately
	
	// waiting
	[ack]  o=2 & x<AD -> 1-p : (o'=1) & (x'=0)  //  received an ack and not last
	                                                       + p : (o'=3) & (x'=0); // receive an ack and last
	[] o=2 & x>=AD -> (o'=4) & (x'=0); // ack not arrived within expected interval (stop) - strick bounds allowed
	// needs fixing for digital clocks
	
endmodule

module malicious_recipient

	r : [0..9];
	// 0 - request
	// 1 - wait
	// 2 - ack
	// 3 - decode1 // decode probabilistically and quickly (can potentially do twice before AD)
	// 4 - decode1 // decode probabilistically (can potentially only do once before AD)
	// 5 - decode3 // decode correctly
	// 6 - send act (after successfully decoded and not last)
	// 7 - decoded

	y : clock;

	invariant
		(r=0 => y<=0) &
		(r=1 => true) &
		(r=2 => true) &
		(r=3 => y<=3) &
		(r=4 => y<=5) &
		(r=5 => y<=10) &
		(r=6 => true) &
		(r=7 => true)
	endinvariant

	[req] r=0 & y=0 -> (r'=1); // initiate protocol
	[message] r=1 -> (r'=2) & (y'=0); // receive message
	[ack] r=2 -> (r'=1); // send ack (no time bound now as malicious)
	
	// try and decode
	//[] r=2 -> (r'=3) & (y'=0); // decode probabilistically and quickly
	[] r=2 -> (r'=4) & (y'=0); // decode probabilistically
	[] r=2 -> (r'=5) & (y'=0); // decode correctly
	
	// decoding (successfully and last, successfully and not last or unsuccessfully)
	[] r=3 & y>=2 -> p*0.01 : (r'=7) & (y'=0) + (1-p)*0.01 : (r'=6) & (y'=0) + 0.99 : (r'=2) & (y'=0);
	[] r=4 & y>=4 -> p*0.25 : (r'=7) & (y'=0) + (1-p)*0.25 : (r'=6) & (y'=0) + 0.75 : (r'=2) & (y'=0);
	[] r=5 & y>=8 -> p : (r'=7) & (y'=0) + (1-p) : (r'=6) & (y'=0);

	// decoded and not last (continue by sending ack)
	// could combine with location 2, but would have the opportunity of decoding again 
	// which is obviously a stupid thing to do so keep separate
	[ack] r=6 -> (r'=1) & (y'=0);

endmodule

// decodes last (nth) message
label "gains_information" = r=7;