Fairness: Non-Repudiation Protocols (NuSMV)

Description of the Case Study

Non-repudiation protocols aim to ensure that a sender cannot deny having sent a message (non-repudiation of origin, NRO) and that a receiver cannot deny having received it (non-repudiation of receipt, NRR). Fairness requires that these evidences are obtained symmetrically—either both parties possess their evidence or neither does. Following Jamroga, Mauw, and Melissen [JMM11], we model two variants: an incorrect protocol \(T_{\text{incorrect}}\) that withholds the receipt after obtaining NRO, and a corrected version \(T_{\text{correct}}\). When analysed with HyperQB, the faulty protocol yields a SAT counterexample under halting pessimistic semantics, demonstrating unfair behaviour. The corrected protocol produces UNSAT under halting optimistic semantics, confirming that it guarantees fairness.

The NuSMV model(s)

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

The HyperLTL formula(s)

Fairness is captured by a HyperLTL property requiring that whenever a cooperative environment delivers the same sequence of actions for two traces, the availability of NRO and NRR must match. The existential trace chooses an execution where the sender delivers the message and both evidences are eventually obtained; every trace that mirrors the sender or receiver schedules must exhibit the same eventual outcomes.

\[\begin{split}\begin{aligned} \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{aligned}\end{split}\]
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