Abstract | ||
---|---|---|
We consider a mild extension of universal algebra in which terms are built both from deterministic and probabilistic variables,
and are interpreted as distributions. We formulate an equational proof system to establish equality between probabilistic
terms, show its soundness, and provide heuristics for proving the validity of equations. Moreover, we provide decision procedures
for deciding the validity of a system of equations under specific theories that are commonly used in cryptographic proofs,
and use concatenation, truncation, and xor. We illustrate the applicability of our formalism in cryptographic proofs, showing
how it can be used to prove standard equalities such as optimistic sampling and one-time padding as well as non-trivial equalities
for standard schemes such as OAEP.
|
Year | DOI | Venue |
---|---|---|
2010 | 10.1007/978-3-642-17511-4_4 | Logic Programming and Automated Reasoning/Russian Conference on Logic Programming |
Keywords | Field | DocType |
one-time padding,non-trivial equality,probabilistic term,decision procedure,standard equality,probabilistic variable,mild extension,standard scheme,cryptographic proof,equational proof system,system of equations,universal algebra,one time pad | Optimal asymmetric encryption padding,Computer science,Algorithm,Mathematical proof,Heuristics,Concatenation,Probabilistic logic,Soundness,Padding,Universal algebra | Conference |
Volume | ISSN | ISBN |
6355 | 0302-9743 | 3-642-17510-4 |
Citations | PageRank | References |
7 | 0.44 | 15 |
Authors | ||
5 |
Name | Order | Citations | PageRank |
---|---|---|---|
Gilles Barthe | 1 | 2337 | 152.36 |
Marion Daubignard | 2 | 54 | 3.79 |
Bruce M. Kapron | 3 | 308 | 26.02 |
Yassine Lakhnech | 4 | 913 | 78.50 |
Vincent Laporte | 5 | 81 | 3.61 |