Non-Interference Until Close: Secure Winner Disclosure in Fixed-Bid Auctions (NuSMV)

Description of the Case Study

In this case study, we model a real-world bidding system adopted from [Arden12]. The bidding service accepts a fixed, predetermined number of bids during an active bidding phase. All bids are processed and compared internally, and no user-visible indication of the winner, or any information that could allow users to infer the winner, is released before the bidding phase ends and all bids have been received.

The intended security requirement is a simplified non-interference property with declassification at the moment the auction closes. Concretely, throughout the bidding phase the observable outputs must be independent of the bid values (no premature leakage); only when the auction ends is a single piece of information, the final winner, declassified and made observable. This ensures that intermediate outputs cannot influence participant behavior or reveal partial outcomes, while still allowing the correct winner to be announced once the process is complete.

This case study evaluates four versions: three are satisfiable and one is unsatisfiable.

The NuSMV model(s)

MODULE main

VAR
    -- Determines if bidding is still occurring
    bidding : boolean;

    -- Current proccessed bid
    curr_bid : 1..4;

    -- Potential winner while still bidding
    potential : 0..3;

    -- Final winner  
    winner : 0..3;
    
    max_bid : 2..6;
    
    -- Bids
    bid_one : 3..4;

    bid_two : 2..3;

    bid_three : 5..6;

        

ASSIGN
    -- Initial values
    init(bidding) := TRUE;
    init(curr_bid) := 1;
    init(potential) := 0;  
    init(winner) := 0;
    init(max_bid) := 3;
    init(bid_one) := 4;
    init(bid_two) := 3;
    init(bid_three) := 6;
    
    next(bid_one) := bid_one;
    next(bid_two) := bid_two;
    next(bid_three) := bid_three;

    -- Updates bidding variable when bidding is done
    next(bidding) :=
        case
            (bidding) & (curr_bid = 4): FALSE;
            (!bidding): FALSE;
            TRUE: TRUE;
        esac;
    
    -- Winner revealed if bidding is over
    next(winner) :=
        case
            (!bidding) : potential;
            TRUE: 0;  
        esac;
    

    -- Updates max bid, if the current bid is greater than max bid then it's the new max
    next(max_bid) :=
        case
            (curr_bid = 1) & (max_bid < bid_one): bid_one;
            (curr_bid = 2) & (max_bid < bid_two): bid_two;
            (curr_bid = 3) & (max_bid < bid_three): bid_three;
            TRUE: max_bid;
        esac;

    -- Updates potential winner
    next(potential) :=
        case
            (max_bid = bid_one): 1;
            (max_bid = bid_two): 2;
            (max_bid = bid_three): 3;
            TRUE: potential;
        esac;

    -- Increment current bid
    next(curr_bid) :=
        case
            (curr_bid < 4): curr_bid + 1;
            TRUE: curr_bid;
        esac;

The HyperLTL formula

This requirement can be specified as simplified non-interference with declassification (NI-D) as follows:

\[\varphi_{bid}^{\text{NI-D}} = \forall \pi_1.\forall \pi_2.\ \Box\left( \mathit{winner}_{\pi_1} = \mathit{winner}_{\pi_2} \right) \mathbin{\mathbf{W}} \#_{\pi_1}\]
Forall A . Forall B . G((bidding[A] & bidding[B]) -> (winner[A] = winner[B]))

References