ruescasd

use crypto::context::Context;
use crypto::context::RistrettoCtx as RCtx;
use crypto::cryptosystem::elgamal::{Ciphertext, KeyPair};
use crypto::traits::groups::GroupElement;

fn main() {
    let keypair: KeyPair<RCtx> = KeyPair::generate();

    // voter submission

ruescasd

use crypto::context::RistrettoCtx as RCtx;
use crypto::cryptosystem::elgamal::{Ciphertext, KeyPair};
use crypto::groups::Ristretto255Group;
use crypto::groups::ristretto255::RistrettoElement;
use crypto::traits::groups::CryptoGroup;
use rnk::*;

type Ctx = RCtx;
type RGroup = Ristretto255Group;

ruescasd

#[enum_dispatch(Machine1Handler)]
enum Machine1 {
    Machine1StateA,
    Machine1StateB,
}
impl Machine1 {
    pub fn handle_input(&self, input: &Machine1Input) {
        // even if we were to name the trait functions with the same name, we can disambiguate them like this
        // otherwise we could simply call input.boomerang(self)
        Machine1Boomerang::boomerang(input, &self);

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