arXiv Science⌕ Search

arXiv subjects

Bryan Ford

Publications and source records attributed to Bryan Ford.

At least 19 recordsLinked to original sources
arXiv2026

Idealizing Useful Fictions in Omega Grounded Arithmetic

Grounded arithmetic is a family of formal systems for reasoning about computation in which a statement may be asserted only when a terminating computation backs it; the logics are paracomplete - for a sentence whose backing computation never settles, neither the sentence nor its negation is derivable, so paradoxes like the Liar are harmless rather than explosive. The reflective member of the family, RGA, can quantify over its own computations, but cannot certify that its own unbounded searches have definite yes-or-no answers. This paper studies what happens when that openness is closed by exactly one rule - ATI, the $\omega$-grounded universal: if every numeric instance of a universal sentence is certified decided, the universal is certified decided. The resulting system, OGA, shares RGA's syntax and rules symbol-for-symbol otherwise, and every consequence is developed as a machine-checked theorem. Decidedness certificates become abundant - every totality question about a computable function is certified to have an answer, whether or not anyone can produce it - and this is exactly the provable separation between the two systems. OGA is complete for its own semantics; certified-but-unresolved sentences receive values built from the system's own open questions. Provability remains recursively enumerable, with a primitive-recursive certificate checker, while $\omega$-truth deliberately is not. Within that asymmetry, incompleteness takes a new form. The G\"odel sentence is classified, unconditionally, as a genuine fiction: neither provable nor refutable, yet valued, and carrying a computable pedigree recording exactly what adopting it as an axiom commits one to. The adoption is itself a theorem suite: extending OGA by any finite stock of true fictions is consistent, and independently certified adoptions can never collide.

math.LO↗
arXiv2026

Internalized Truth in Reflective Grounded Arithmetic

By Tarski's undefinability theorem, no consistent classical formal system that includes arithmetic can define its own truth predicate. Reflective Grounded Arithmetic (RGA) is a powerful arithmetic whose universal quantifier is grounded in its own reflected proof search, and whose paracompleteness circumvents Tarski's theorem. This paper presents a machine-checked Isabelle/HOL development that defines a truth predicate for RGA's full language, quantifiers included, as an internal term of RGA itself. This term is compiled from a primitive-recursive decider for its operational semantics, and proven adequate in both directions. Around this predicate the development closes a square of metatheorems: for every formula RGA proves, RGA derives the formula's internal truth; every grounded-true formula is internally provable; internal truth implies internal provability; and the consistency of RGA follows. The two directions run on disjoint internal machines---a certified decider and a certified proof-checker, both RGA terms. Reaching these results involved substantial ordinary reasoning carried out within RGA: coded syntax and substitution, compiled primitive-recursive functions with symbolic unfolding laws, internal strong induction, and a verified proof-checker for the system written in the system's own formal language. The development thus demonstrates along the way that RGA is a workable formal system supporting nontrivial mathematical reasoning.

math.LO↗
arXiv2026

Computable Quantification in Reflective Grounded Arithmetic

Informal statements of G\"odel's incompleteness theorems often run: "no consistent formal system with arithmetic can be complete" - omitting the fact that the theorems as proved assume classical logic. This paper presents reflective grounded arithmetic (RGA), a paracomplete arithmetic in which truth is grounded in computation rather than assumed by classical fiat, and in which universal quantification is grounded reflectively: a universal statement is true when the system's own proof search certifies its schematic instance, and false when it refutes a particular numeral instance. RGA permits unconstrained recursive definitions, proves the totality of addition and multiplication as internally quantified theorems, and represents exactly the recursively enumerable sets - the ingredient list of the folklore G\"odel statement - while remaining consistent. This work proves, with all results machine-checked in Isabelle/HOL: soundness and consistency; open completeness - provability coincides with grounded truth on well-formed statements; N-soundness - every provable totality claim is backed by an actual value; a Church-Turing characterization of RGA's expressive power; and $\omega$-incompleteness - grounded truth is recursively enumerable, and therefore some family of statements has every numeric instance provable while its universal closure is not merely unprovable but semantically ungrounded. The resulting logic occupies a Markov-flavored, substructural corner distinct from both classical and intuitionistic arithmetic: double-negation elimination holds, quantified excluded middle fails, refuted universals yield explicit counterexample witnesses, and the deduction theorem's abstraction direction fails precisely at ungrounded hypotheses.

math.LO↗
arXiv2025

Have a thing? Reasoning around recursion with dynamic typing in grounded arithmetic

Neither the classical nor intuitionistic logic traditions are perfectly aligned with the purpose of reasoning about computation, as neither can permit unconstrained recursive definitions without inconsistency: recursive definitions must normally be proven terminating before admission and use. Grounded arithmetic or GA is a formal-reasoning foundation allowing direct expression of arbitrary recursive definitions. GA adjusts traditional inference rules so that terms that express nonterminating computations harmlessly denote no semantic value ($\bot$) instead of yielding inconsistency. Recursive functions are proven terminating in GA essentially by "dynamically typing" terms, or equivalently, symbolically reverse-executing the computations they denote via inference rules. Once recursive functions have been proven terminating, logical reasoning about them reduces to familiar classical rules. We summarize the development and lessons learned from two mechanically-checked formulations of GA, finding both syntactically consistent and semantically sound with respect to an underlying computable model. Propositional grounded arithmetic or PGA is a quantifier-free system for inductive grounded reasoning about open formulas. PGA has logical expressiveness comparable to Skolem's PRA, but has general-recursive (Turing-complete) functional expressiveness. PGA builds upon a simpler system of basic grounded arithmetic or BGA, which omits logical operators entirely. BGA and PGA are not only sound but semantically complete, a combination impossible for powerful classical systems with arithmetic, due to G\"odel's incompleteness theorems. These results suggest that powerful and consistent formal reasoning with unconstrained recursive definitions is possible, potentially enabling new computation-centric formal languages, proof assistants, and type systems in the future.

cs.PL↗
arXiv2025

Towards the ideals of Self-Recovery and Metadata Privacy in Social Vault Recovery

Social key recovery mechanisms enable users to recover their vaults with the help of trusted contacts, or trustees, avoiding the need for a single point of trust or memorizing complex strings. However, existing mechanisms overlook the memorability demands on users for recovery, such as the need to recall a threshold number of trustees. Therefore, we first formalize the notion of recovery metadata in the context of social key recovery, illustrating the tradeoff between easing the burden of memorizing the metadata and maintaining metadata privacy. We present Apollo, the first framework that addresses this tradeoff by distributing indistinguishable data within a user's social circle, where trustees hold relevant data and non-trustees store random data. Apollo eliminates the need to memorize recovery metadata since a user eventually gathers sufficient data from her social circle for recovery. Due to indistinguishability, Apollo protects metadata privacy by forming an anonymity set that hides the trustees among non-trustees. To make the anonymity set scalable, Apollo proposes a novel multi-layered secret sharing scheme that mitigates the overhead due to the random data distributed among non-trustees. Finally, we provide a prototype implementation of Apollo and report on its performance. Apollo reduces the chances of malicious recovery to between 0.005% and 1.8%, depending on the adversary's ability to compromise. The multi-layered design shows a latency reduction from 1.1x to 740kx compared to a single-layered approach, depending on the number of reconnections.

cs.CR↗
arXiv2024

Reasoning Around Paradox with Grounded Deduction

How can we reason around logical paradoxes without falling into them? This paper introduces grounded deduction or GD, a Kripke-inspired approach to first-order logic and arithmetic that is neither classical nor intuitionistic, but nevertheless appears both pragmatically usable and intuitively justifiable. GD permits the direct expression of unrestricted recursive definitions -- including paradoxical ones such as 'L := not L' -- while adding dynamic typing premises to certain inference rules so that such paradoxes do not lead to inconsistency. This paper constitutes a preliminary development and investigation of grounded deduction, to be extended with further elaboration and deeper analysis of its intriguing properties.

math.LO↗
arXiv2024

E-Vote Your Conscience: Perceptions of Coercion and Vote Buying, and the Usability of Fake Credentials in Online Voting

Online voting is attractive for convenience and accessibility, but is more susceptible to voter coercion and vote buying than in-person voting. One mitigation is to give voters fake voting credentials that they can yield to a coercer. Fake credentials appear identical to real ones, but cast votes that are silently omitted from the final tally. An important unanswered question is how ordinary voters perceive such a mitigation: whether they could understand and use fake credentials, and whether the coercion risks justify the costs of mitigation. We present the first systematic study of these questions, involving 150 diverse individuals in Boston, Massachusetts. All participants "registered" and "voted" in a mock election: 120 were exposed to coercion resistance via fake credentials, the rest forming a control group. Of the 120 participants exposed to fake credentials, 96% understood their use. 53% reported that they would create fake credentials in a real-world voting scenario, given the opportunity. 10% mistakenly voted with a fake credential, however. 22% reported either personal experience with or direct knowledge of coercion or vote-buying incidents. These latter participants rated the coercion-resistant system essentially as trustworthy as in-person voting via hand-marked paper ballots. Of the 150 total participants to use the system, 87% successfully created their credentials without assistance; 83% both successfully created and properly used their credentials. Participants give a System Usability Scale score of 70.4, which is slightly above the industry's average score of 68. Our findings appear to support the importance of the coercion problem in general, and the promise of fake credentials as a possible mitigation, but user error rates remain an important usability challenge for future work.

cs.HC↗
arXiv2023

Breaking Blockchain Rationality with Out-of-Band Collusion

Blockchain systems often rely on rationality assumptions for their security, expecting that nodes are motivated to maximize their profits. These systems thus design their protocols to incentivize nodes to execute the honest protocol but fail to consider out-of-band collusion. Existing works analyzing rationality assumptions are limited in their scope, either by focusing on a specific protocol or relying on non-existing financial instruments. We propose a general rational attack on rationality by leveraging an external channel that incentivizes nodes to collude against the honest protocol. Our approach involves an attacker creating an out-of-band bribery smart contract to motivate nodes to double-spend their transactions in exchange for shares in the attacker's profits. We provide a game theory model to prove that any rational node is incentivized to follow the malicious protocol. We discuss our approach to attacking the Bitcoin and Ethereum blockchains, demonstrating that irrational behavior can be rational in real-world blockchain systems when analyzing rationality in a larger ecosystem. We conclude that rational assumptions only appear to make the system more secure and offer a false sense of security under the flawed analysis.

cs.GT↗
arXiv2022

Matchertext: Towards Verbatim Interlanguage Embedding

Embedding text in one language within text of another is commonplace for numerous purposes, but usually requires tedious and error-prone "escaping" transformations on the embedded string. We propose a simple cross-language syntactic discipline, matchertext, which enables the safe embedding a string in any compliant language into a string in any other language via simple "copy-and-paste" - in particular with no escaping, obfuscation, or expansion of embedded strings. We apply this syntactic discipline to several common and frequently-embedded language syntaxes such as URIs, HTML, and JavaScript, exploring the benefits, costs, and compatibility issues in adopting the proposed matchertext discipline. One early matchertext-based language is MinML, a concise but general alternative syntax for writing HTML or XML.

cs.PL↗
arXiv2022

F3B: A Low-Overhead Blockchain Architecture with Per-Transaction Front-Running Protection

Front-running attacks, which benefit from advanced knowledge of pending transactions, have proliferated in the blockchain space since the emergence of decentralized finance. Front-running causes devastating losses to honest participants and continues to endanger the fairness of the ecosystem. We present Flash Freezing Flash Boys (F3B), a blockchain architecture that addresses front-running attacks by using threshold cryptography. In F3B, a user generates a symmetric key to encrypt their transaction, and once the underlying consensus layer has finalized the transaction, a decentralized secret-management committee reveals this key. F3B mitigates front-running attacks because, before the consensus group finalizes it, an adversary can no longer read the content of a transaction, thus preventing the adversary from benefiting from advanced knowledge of pending transactions. Unlike other mitigation systems, F3B properly ensures that all unfinalized transactions, even with significant delays, remain private by adopting per-transaction protection. Furthermore, F3B addresses front-running at the execution layer; thus, our solution is agnostic to the underlying consensus algorithm and compatible with existing smart contracts. We evaluated F3B on Ethereum with a modified execution layer and found only a negligible (0.026%) increase in transaction latency, specifically due to running threshold decryption with a 128-member secret-management committee after a transaction is finalized; this indicates that F3B is both practical and low-cost.

cs.CR↗
arXiv2022

Baxos: Backing off for Robust and Efficient Consensus

Leader-based consensus algorithms are vulnerable to liveness and performance downgrade attacks. We explore the possibility of replacing leader election in Multi-Paxos with random exponential backoff (REB), a simpler approach that requires minimum modifications to the two phase Synod Paxos and achieves better resiliency under attacks. We propose Baxos, a new resilient consensus protocol that leverages a random exponential backoff scheme as a replacement for leader election in consensus algorithms. Our backoff scheme addresses the common challenges of random exponential backoff such as scalability and robustness to changing wide area latency. We extensively evaluate Baxos to illustrate its performance and robustness against two liveness and performance downgrade attacks using an implementation running on Amazon EC2 in a wide area network and a combination of a micro benchmark and YCSB-A workload on Redis. Our results show that Baxos offers more robustness to liveness and performance downgrade attacks than leader-based consensus protocols. Baxos outperforms Multi-Paxos and Raft up to 128% in throughput under liveness and performance downgrade attacks under worst case contention scenarios where each replica proposes requests concurrently.

cs.DC↗
arXiv2022

TRIP: Coercion-resistant Registration for E-Voting with Verifiability and Usability in Votegral

Online voting is convenient and flexible, but amplifies the risks of voter coercion and vote buying. One promising mitigation strategy enables voters to give a coercer fake voting credentials, which silently cast votes that do not count. Current systems along these lines make problematic assumptions about credential issuance, however, such as strong trust in a registrar and/or in voter-controlled hardware, or expecting voters to interact with multiple registrars. Votegral is the first coercion-resistant voting architecture that leverages the physical security of in-person registration to address these credential-issuance challenges, amortizing the convenience costs of in-person registration by reusing credentials across successive elections. Votegral's registration component, TRIP, gives voters a kiosk in a privacy booth with which to print real and fake credentials on paper, eliminating dependence on trusted hardware in credential issuance. The voter learns and can verify in the privacy booth which credential is real, but real and fake credentials thereafter appear indistinguishable to others. Only voters actually under coercion, a hopefully-rare case, need to trust the kiosk. To achieve verifiability, each paper credential encodes an interactive zero-knowledge proof, which is sound in real credentials but unsound in fake credentials. Voters observe the difference in the order of printing steps, but need not understand the technical details. Experimental results with our prototype suggest that Votegral is practical and sufficiently scalable for real-world elections. User-visible latency of credential issuance in TRIP is at most 19.7 seconds even on resource-constrained kiosk hardware. A companion usability study indicates that TRIP's usability is competitive with other e-voting systems, and formal proofs support TRIP's combination of coercion-resistance and verifiability.

cs.CR↗
arXiv2020

Identity and Personhood in Digital Democracy: Evaluating Inclusion, Equality, Security, and Privacy in Pseudonym Parties and Other Proofs of Personhood

Digital identity seems like a prerequisite for digital democracy: how can we ensure "one person, one vote" online without identifying voters? But digital identity solutions - ID checking, biometrics, self-sovereign identity, and trust networks - all present flaws, leaving users vulnerable to exclusion, identity loss or theft, and coercion. These flaws may be insurmountable because digital identity is a cart pulling the horse. We cannot achieve digital identity secure enough for the weight of digital democracy, until we build it on a solid foundation of "digital personhood." While identity is about distinguishing one person from another through attributes or affiliations, personhood is about giving all real people inalienable digital participation rights independent of identity, including protection against erosion of their democratic rights through identity loss, theft, coercion, or fakery. We explore and analyze alternative approaches to "proof of personhood" that may provide this missing foundation. Pseudonym parties marry the transparency of periodic physical-world events with the power of digital tokens between events. These tokens represent limited-term but renewable claims usable for purposes such as online voting or liquid democracy, sampled juries or deliberative polls, abuse-resistant social communication, or minting universal basic income in a permissionless cryptocurrency. Enhancing pseudonym parties to provide participants a moment of enforced physical security and privacy can address coercion and vote-buying risks that plague today's E-voting systems. We also examine other proposed approaches to proof of personhood, some of which offer conveniences such as all-online participation. These alternatives currently fall short of satisfying all the key digital personhood goals, unfortunately, but offer valuable insights into the challenges we face.

cs.CY↗
arXiv2020

Economic Principles of PoPCoin, a Democratic Time-based Cryptocurrency

While democracy is founded on the principle of equal opportunity to manage our lives and pursue our fortunes, the forms of money we have inherited from millenia of evolution has brought us to an unsustainable dead-end of exploding inequality. PoPCoin proposes to leverage the unique historical opportunities that digital cryptocurrencies present for a "clean-slate" redesign of money, in particular around long-term equitability and sustainability, rather than solely stability, as our primary goals. We develop and analyze a monetary policy for PoPCoin that embodies these equitability goals in two basic rules that maybe summarized as supporting equal opportunity in "space" and "time": the first by regularly distributing new money equally to all participants much like a basic income, the second by holding the aggregate value of these distributions to a constant and non-diminishing portion of total money supply through demurrage. Through preliminary economic analysis, we find that these rules in combination yield a unique form of money with numerous intriguing and promising properties, such as a quantifiable and provable upper bound on monetary inequality, a natural "early adopter's reward" that could incentivize rapid growth while tapering off as participation saturates, resistance to the risk of deflationary spirals, and migration incentives opposite those created by conventional basic incomes.

cs.CY↗
arXiv2020

Democratic Value and Money for Decentralized Digital Society

Classical monetary systems regularly subject the most vulnerable majority of the world's population to debilitating financial shocks, and have manifestly allowed uncontrolled global inequality over the long term. Given these basic failures, how can we avoid asking whether mainstream macroeconomic principles are actually compatible with democratic principles such as equality or the protection of human rights and dignity? This idea paper takes a constructive look at this question, by exploring how alternate monetary principles might result in a form of money more compatible with democratic principles -- dare we call it "democratic money"? In this alternative macroeconomic philosophy, both the supply of and the demand for money must be rooted in people, so as to give all people both equal opportunities for economic participation. Money must be designed around equality, not only across all people alive at a given moment, but also across past and future generations of people, guaranteeing that our descendants cannot be enslaved by their ancestors' economic luck or misfortune. Democratic money must reliably give all people a means to enable everyday commerce, investment, and value creation in good times and bad, and must impose hard limits on financial inequality. Democratic money must itself be governed democratically, and must economically facilitate the needs of citizens in a democracy for trustworthy and unbiased information with which to make wise collective decisions. An intriguing approach to implementing and deploying democratic money is via a cryptocurrency built on a proof-of-personhood foundation, giving each opt-in human participant one equal unit of stake. Such a cryptocurrency would have both interesting similarities to, and important differences from, a Universal Basic Income (UBI) denominated in an existing currency.

cs.CY↗
arXiv2020

A Liquid Perspective on Democratic Choice

The idea of liquid democracy responds to a widely-felt desire to make democracy more "fluid" and continuously participatory. Its central premise is to enable users to employ networked technologies to control and delegate voting power, to approximate the ideal of direct democracy in a scalable fashion that accounts for time and attention limits. There are many potential definitions, meanings, and ways to implement liquid democracy, however, and many distinct purposes to which it might be deployed. This paper develops and explores the "liquid" notion and what it might mean for purposes of enhancing voter choice by spreading voting power, improving proportional representation systems, simplifying or aiding voters in their choice, or scaling direct democracy through specialization. The goal of this paper is to disentangle and further develop some of the many concepts and goals that liquid democracy ideas often embody, to explore their justification with respect to existing democratic traditions such as transferable voting and political parties, and to explore potential risks in liquid democracy systems and ways to address them.

cs.CY↗
arXiv2020

Que Sera Consensus: Simple Asynchronous Agreement with Private Coins and Threshold Logical Clocks

It is commonly held that asynchronous consensus is much more complex, difficult, and costly than partially-synchronous algorithms, especially without using common coins. This paper challenges that conventional wisdom with que sera consensus QSC, an approach to consensus that cleanly decomposes the agreement problem from that of network asynchrony. QSC uses only private coins and reaches consensus in $O(1)$ expected communication rounds. It relies on "lock-step" synchronous broadcast, but can run atop a threshold logical clock (TLC) algorithm to time and pace partially-reliable communication atop an underlying asynchronous network. This combination is arguably simpler than partially-synchronous consensus approaches like (Multi-)Paxos or Raft with leader election, and is more robust to slow leaders or targeted network denial-of-service attacks. The simplest formulations of QSC atop TLC incur expected $O(n^2)$ messages and $O(n^4)$ bits per agreement, or $O(n^3)$ bits with straightforward optimizations. An on-demand implementation, in which clients act as "natural leaders" to execute the protocol atop stateful servers that merely implement passive key-value stores, can achieve $O(n^2)$ expected communication bits per client-driven agreement.

cs.DC↗