David Ruescas ruescasd

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:

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

	analyzed: cai_attack.spthy

	processing time: 0.83s

	#!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

	/**
	* 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

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

	%*******************************************************************************%
	%****************************** 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).

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

	[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"

	// encode to m * legendre(m\|p)
	if (encode_m) {
	// need to encode the message given that p = 2q+1
	var y = m.add(BigInt.ONE);
	// euler criterion to determine quadratic residuosity
	var test = y.modPow(pk.q, pk.p);
	if (test.equals(BigInt.ONE)) {
	this.m = y;
	} else {
	this.m = y.negate().mod(pk.p);