Deniability (NuSMV)

Description of the Case Study

Deniability requires that every observable execution can be explained by multiple secrets that remain indistinguishable to an observer. We follow Sahai, Subramanyan, and Sinha [SSS20] and the wallet examples of Backes, Köpf, and Rybalchenko [BKR09], checking the case \(N = 1\) where one alternative execution suffices. In the wallet protocol, an adversary attempts to infer the confidential balance (sec) by repeatedly withdrawing a fixed amount (obs). HyperQB verifies both a small illustrative model and the full specification. Under the halting optimistic semantics the solver reports UNSAT, showing that the system successfully hides the initial balance by presenting indistinguishable traces with different secrets.

The NuSMV model(s)

--(adopted from: Michael Backes, Boris Kopf, and Andrey Rybalchenko. Automatic discovery and quantification of information leaks. In 2009 30th IEEE Symposium on Security and Privacy)
MODULE main
 VAR
    PC: 1..6;
    num_itr: 0..11;
    init_balance: 0..20;
    debits_amount: 1..10;
    halt: boolean;
 ASSIGN
    -- Initial Conditions
    init(init_balance) := {0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20};
    init(debits_amount) := {1,2,3,4,5,6,7,8,9,10};
    init(num_itr) := 0;
    init(PC) := 1; -- but program counter starts at 1.
    init(halt) := FALSE;

    -- Transition Relations
    next(init_balance) :=
      case
        ((PC=3) & (init_balance - debits_amount > 0)): (init_balance - debits_amount);
        TRUE: init_balance;
      esac;

    next(debits_amount) :=
      case
        TRUE: debits_amount;
      esac;

    next(num_itr) :=
      case
        (PC=4): num_itr;
        TRUE: num_itr;
      esac;

    next(PC) :=
      case
        (PC=1): 2; -- num_itr = 0
        ((PC=2) & (init_balance > debits_amount)): 3; -- while (init_balance >= debits amount)
        ((PC=2) & (init_balance <= debits_amount)): 5;
        (PC=3): 4; -- init_balance -= debits_amount
        (PC=4): 2; -- num_itr += 1
        (PC=5): 6; -- Return num_itr += 1
        (PC=6): 6; -- (END)
        TRUE: PC;
      esac;

    next(halt) :=
      case
        (PC=6): TRUE;
        TRUE: halt;
      esac;

The HyperLTL formula(s)

The specification below states that every observable trace \(\pi_A\) must admit two companion traces, \(\pi_B\) and \(\pi_C\), that match all observable events yet disagree on the secret. HyperQB instantiates the existential traces to demonstrate indistinguishability or produce a counterexample if the system leaks information.

\[\begin{split}\begin{aligned} \varphi_{\text{den}} = {} & \forall \pi_A . \exists \pi_B . \exists \pi_C . \\ & \Box \Big( (\mathit{obs}_{\pi_A} \leftrightarrow \mathit{obs}_{\pi_B}) \land (\mathit{obs}_{\pi_A} \leftrightarrow \mathit{obs}_{\pi_C}) \land (\mathit{sec}_{\pi_B} \not\leftrightarrow \mathit{sec}_{\pi_C}) \Big) \end{aligned}\end{split}\]
Forall A . Exists B . Exists C .
G(
  (debits_amount[A]=debits_amount[B])
  &
  (debits_amount[A]=debits_amount[C])
  &
  ~(init_balance[B]=init_balance[C])
)

References