ruescasd

theory trustee_setup

begin

#include "../common/primitives.spthy.inc"

/* Bootstrapping facts 

Because tamarin does not support indexed arrays, the election configuration message splits
into  several facts. 

ruescasd

Voter casts:

b = (g^r, m*h^r)

pc_1 = g^c1*h^r_c1

EA computes:

pc_2 = g^c2*h^r_c2

ruescasd

/*
$tamarin-prover --prove --output-json=trace.json cai_attack.spthy
// Attack 1
==============================================================================
summary of summaries:

analyzed: cai_attack.spthy

  processing time: 0.83s

ruescasd

use cry_rts::trait_methods::*;
pub fn main() {
  println!("{:#?}", (*cryptol_gen::primitives::prg_ddh__test::main).display())
}

ruescasd

#!cryptol
#![allow(unused_variables)]
#![allow(unused_imports)]
use cry_rts::trait_methods::*;

/**
Returns the smaller of two comparable arguments.
Bitvectors are compared using unsigned arithmetic.

```cryptol

ruescasd

/**
 * Test of Pseudo-random Generator from the DDH Assumption
 * Section 10.1 of the EVS Draft, February 3, 2024.
 *
 * @author Frank Zeyda ([email protected])
 * @copyright Free & Fair 2025
 * @version 0.1
 */
module Primitives::PRG_DDH_Test where

ruescasd

/// Example of how to implement this without mutable state.
/// This is a more functional approach, but I would not implement it this way
/// in real code because 1) it is probably less efficient, and 2) requires 
/// an extra dependency (itertools).
use itertools::Itertools;
fn tally_votes(election: &Election, votes: &[Vote]) -> ResultData {
    let grouped = votes
        .into_iter()
        .filter(|v| v.contest_id == election.id)
        .map(|v| (v.choice_id, v))

ruescasd

%*******************************************************************************%
%******************************** EXECUTION ************************************%
%*******************************************************************************%

do(act_sign_config(ConfigHash), A, T) :-
	posted(config(ConfigHash, _, _, SelfT, A), T),
	not posted(config_signature(ConfigHash, A), T),
	not pending(_, A, T),
	active(A, T), a(A).

ruescasd

[package]
name = "b3"
version = "0.1.0"
edition = "2018"

# See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html

[dependencies]
rand = "0.7.3"
sha2 = "0.9.1"

ruescasd

Keybase proof

I hereby claim:

• I am ruescasd on github.
• I am czakalwe (https://keybase.io/czakalwe) on keybase.
• I have a public key whose fingerprint is E2C2 47D4 54F9 DC7E 8AB1 2448 AE6A A7BC 726D A9FD

To claim this, I am signing this object: