A Computationally Complete Symbolic Attacker for Equivalence Properties (bibtex)
by Gergei Bana, Hubert Comon-Lundh
Abstract:
We consider the problem of computational indistinguishability of protocols. We design a symbolic model, amenable to automated deduction, such that a successful inconsistency proof implies computational indistinguishability. Conversely, symbolic models of distinguishability provide clues for likely computational attacks. We follow the idea we introduced earlier for reachability properties, axiomatizing what an attacker cannot violate. This results a computationally complete symbolic attacker, and ensures unconditional computational soundness for the symbolic analysis. We present a small library of computationally sound, modular axioms, and test our technique on an example protocol. Despite additional difficulties stemming from the equivalence properties, the models and the soundness proofs turn out to be simpler than they were for reachability properties.
Reference:
A Computationally Complete Symbolic Attacker for Equivalence Properties (Gergei Bana, Hubert Comon-Lundh), In ACM Conference on Computer and Communications Security (CCS'14), ACM, 2014.
Bibtex Entry:
@inproceedings{BanComCCS14,
 author = {Bana, Gergei and Comon-Lundh, Hubert},
 title = {A Computationally Complete Symbolic Attacker for Equivalence Properties},
 booktitle = {ACM Conference on Computer and Communications Security (CCS'14)},
 year = {2014},
 month = {Nov},
 pages = {609--620},
 publisher = {ACM},
 address = {New York, NY, USA},
 keywords = {computational soundness, protocol indistinguishability, security protocols, symbolic verification},
 abstract = {We consider the problem of  computational indistinguishability of protocols. 
We design a symbolic model, amenable to automated deduction, such that a successful inconsistency proof implies computational indistinguishability. Conversely, symbolic models of distinguishability provide clues for likely computational attacks. We follow the idea 
we introduced earlier for reachability properties,  axiomatizing what an attacker  cannot violate.  This results a computationally complete symbolic attacker, and ensures unconditional computational soundness for the symbolic analysis. We present a small library of computationally sound, modular axioms, and test our technique on an example protocol. Despite additional difficulties stemming from the equivalence properties, the models and the soundness proofs turn out to be simpler than they were for reachability properties.}
}
Powered by bibtexbrowser