Fairness in Non-Repudiation Protocols (NuSMV)

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)))

References