Fairness in Non-Repudiation Protocols

Description of the Case Study

A non-repudiation protocol ensures that a receiver obtains a receipt from the sender, called non-repudiation of origin (NRO), and the sender ends up having an evidence, named non-repudiation of receipt (NRR), through a trusted third party. A non-repudiation protocol is fair if both NRR and NRO are either both received or both not received by the parties.

\[\begin{split}\varphi_{\text{fair}} = \exists \pi_A . \forall \pi_B . (\lozenge m_{\pi_A}) \land (\lozenge NRR_{\pi_A}) \land (\lozenge NRO_{\pi_A}) \land \\ \big( (\Box \bigwedge_{\mathit{act} \in \mathit{Act}_P} act_{\pi_A} \leftrightarrow act_{\pi_B}) \rightarrow ((\lozenge NRR_{\pi_B}) \leftrightarrow (\lozenge NRO_{\pi_B})) \big) \land \\ \big( (\Box \bigwedge_{\mathit{act} \in \mathit{Act}_Q} \neg act_{\pi_A} \leftrightarrow act_{\pi_B}) \rightarrow ((\lozenge NRR_{\pi_B}) \leftrightarrow (\lozenge NRO_{\pi_B})) \big)\end{split}\]

We studied two different protocols from [JMM11], namely, \(T_{\text{incorrect}}\) that chooses not to send out NRR after receiving NRO, and a correct implementation \(T_{\text{correct}}\) which is fair. For \(T_{\text{correct}}\), HyperQB returns UNSAT in the halting optimistic semantics which indicates that the protocol satisfies fairness. For \(T_{\text{incorrect}}\), HyperQB returns SAT in the halting pessimistic semantics which implies that fairness is violated.

Benchmarks

The Model(s)

-- Non-repudiation Protocol
-- (adopted from: Wojciech Jamroga, Sjouke Mauw, and Matthijs Melissen. Fairness in nonrepudiation protocols. In Proc. of the 7th Int’l Workshop on Security and Trust Management (STM’11))
-- (1) skip until P->T: m ;
-- (2) skip until P->T: NRO ;
-- (3) T->Q: m ;
-- (4) skip until Q->T: NRR;
-- (5) T->Q: NRO;
-- (6) T->P: NRR;
-- (7) terminate

MODULE main
VAR
	-- P
	sender_actions: 0..4; 	-- 0: skip;
							-- 1: send receiver msg;
							-- 2: send third-party msg:
							-- 3: send receiver NRO;
							-- 4: send send third-party NRO;
	-- Q
	receiver_actions: 0..2; -- 0: skip;
							-- 1: send sender NRR;
							-- 2: send third-party NRR:
	-- T
	thirdparty_actions: 0..3; -- 0: skip;
							-- 1: send receiver msg
							-- 2: send sender NRO;
							-- 3: send receiver NRR:


	take_turns: 0..2; -- 0: sender, 1:receiver, 2:thridparty

	line: 1..7;
ASSIGN
	init(sender_actions) := 0;
	init(receiver_actions) := 0;
	init(thirdparty_actions) := 0;

	init(take_turns) := 0;
	init(line) := 1;


	next(line) :=
		case
			(line=1 & !(sender_actions=2)) : {1}; -- skip
			(line=1 & sender_actions=2) : {2};  -- P->T:m
			(line=2 & !(sender_actions=4)) : {2} ; -- skip
			(line=2 & (sender_actions=4)) : {3} ; -- P->T: NRO
			line=3 : {4} ;
			line=4 : {5} ; -- BUG, no skip until Q->T: NRR!
			(line=5 & !(receiver_actions=2)) : {5}; -- skip
			(line=5 & (receiver_actions=2)) : {6} ; -- Q->T NRR
			line=6 : {7} ;
			line=7 : {7} ; -- terminate
		esac;

	next(take_turns) :=
		case
			(line=3) : (take_turns);
			(line=5) : (take_turns);
			(line=6) : (take_turns);
			(take_turns=0) : 1;
			(take_turns=1) : 2;
			(take_turns=2) : 0;
		esac;

	next(sender_actions) :=
		case
			(take_turns=0) : {0,1,2,3,4};
			!(take_turns=0) : 0;
		esac;

	next(receiver_actions) :=
		case
			(take_turns=1) : {0,1,2};
			!(take_turns=1) : 0;
		esac;

	next(thirdparty_actions) :=
		case
			(line=3) : {1};
			(line=4) : {2};
			(line=6) : {3};
			(take_turns=2) : {0,1,2,3};
			!(take_turns=2) : 0;
		esac;

DEFINE

Formula

exists A. forall B.
( 
	F(*line[A]=3*) 
	/\ F(*line[A]=5*) 
	/\ F(*line[A]=6*)
)
/\
( 
	(G(*sender_actions[A]=sender_actions[B]*)) 
	-> 
	(F(*line[B]=5*))<->(F(*line[B]=6*)) 
) 
/\
( 
	(G(*receiver_actions[A]=receiver_actions[B]*)) 
	-> 
	(F(*line[B]=5*))<->(F(*line[B]=6*))
)