{"doi":"10.1145/2660267.2660276","title":"A Computationally Complete Symbolic Attacker for Equivalence Properties","abstract":null,"journal":"Proceedings of the 2014 ACM SIGSAC Conference on Computer and Communications Security","year":2014,"id":597674,"datarank":0.5533319181170905,"base_score":3.6888794541139363,"endowment":3.6888794541139363,"self_citation_contribution":0.5533319181170905,"citation_network_contribution":0.0,"self_endowment_contribution":0.5533319181170905,"citer_contribution":0.0,"corpus_percentile":null,"corpus_rank":null,"citation_count":39,"citer_count":0,"citers_with_citation_signal":0,"citers_with_endowment":0,"datacite_reuse_total":1,"is_dataset":false,"is_dataset_confidence":null,"is_data_producer":false,"deposit_databanks":null,"is_oa":false,"file_count":0,"downloads":0,"has_version_chain":false,"published_date":null,"fair_score":null,"fair_percentile":null,"algorithm_id":"datarank_citation_only_1hop_v6","ranking_scope":"data_only","authors":[{"id":1531214,"name":"Hubert Comon-Lundh","orcid":null,"position":1,"is_corresponding":false},{"id":1531213,"name":"Gergei Bana","orcid":null,"position":0,"is_corresponding":false}],"reference_count":0,"raw_metadata":{"has_enrichment":true,"resolved":true,"title":"A Computationally Complete Symbolic Attacker for Equivalence Properties","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.","is_dataset_classified":null,"base_score":3.6888794541139363,"endowment":3.6888794541139363,"datacite_reuse_total":1,"file_count":0,"downloads":0,"views":0,"has_version_chain":false,"is_dataset":false,"is_oa":false,"pmid":"23304386","pmcid":null,"openalex_id":"https://openalex.org/W2155728227","authors":[],"funders":[{"funder_name":"European Research Council","grant_id":"259639","title":"CRYSP: A Novel Framework for Collaboratively Building Cryptographically Secure Programs and their Proofs"},{"funder_name":"Agence Nationale de la Recherche","grant_id":"ANR-2010-VERS-004","title":null},{"funder_name":"Fundação para a Ciência e a Tecnologia","grant_id":"PTDC/EIA- CCO/113033/2009","title":null}],"total_grants":3,"fwci":null,"citation_percentile":null,"influential_citations":0,"citation_trend":[{"year":2015,"count":4},{"year":2016,"count":2},{"year":2017,"count":3},{"year":2018,"count":1},{"year":2019,"count":3},{"year":2020,"count":2},{"year":2021,"count":2},{"year":2022,"count":4},{"year":2023,"count":5},{"year":2024,"count":8},{"year":2025,"count":4},{"year":2026,"count":1}],"oa_status":"closed","license":"https://www.acm.org/publications/policies/copyright_policy#Background","oa_locations":[{"url":"https://dl.acm.org/doi/10.1145/2660267.2660276","host_type":"publisher"},{"url":"https://dl.acm.org/doi/pdf/10.1145/2660267.2660276","host_type":"publisher"},{"url":"https://doi.org/10.1145/2660267.2660276","host_type":""},{"url":"https://inria.hal.science/hal-01102216","host_type":"repository"},{"url":"https://inria.hal.science/hal-01102216v1","host_type":""},{"url":"https://dx.doi.org/10.1145/2660267.2660276","host_type":""},{"url":"https://zenodo.org/records/14574125","host_type":""},{"url":"http://dx.doi.org/10.1145/2660267.2660276","host_type":""}],"fields_of_study":["Advanced Authentication Protocols Security","User Authentication and Security Systems","Digital Rights Management and Security","0202 electrical engineering, electronic engineering, information engineering","02 engineering and technology","0102 computer and information sciences","01 natural sciences"],"mesh_terms":[],"keywords":["Soundness","Reachability","Mathematical proof","Computer science","Symbolic trajectory evaluation","Theoretical computer science","Symbolic execution","Equivalence (formal languages)","Axiom","Modular design","Computational complexity theory","Algorithm","Model checking","Programming language","Mathematics","Discrete mathematics","European Research Council","[INFO.INFO-CR] Computer Science [cs]/Cryptography and Security [cs.CR]"],"sdg_mappings":[{"sdg_number":16,"sdg_label":"16. Peace & justice"}],"linked_datasets":[{"doi":"10.4230/lipics.csl.2025.24","title":"Propositional Logics of Overwhelming Truth","publisher":"Schloss Dagstuhl – Leibniz-Zentrum für Informatik","resource_type":"ConferencePaper"}],"clinical_trials":[],"software_tools":[],"database_accessions":[],"source":"live","citation_network_status":"fetched"},"created_at":"2026-07-28T13:55:07.735348Z","pmid":null,"pmcid":null,"fwci":null,"citation_percentile":null,"influential_citations":0,"oa_status":null,"license":null,"views":0,"total_file_size_bytes":0,"version_count":0,"fair_f":null,"fair_a":null,"fair_i":null,"fair_r":null,"fair_zscore":null,"fair_rationale":null,"fair_model":null,"fair_agent_version":null,"fair_fulltext_source":null,"fair_has_llm":null,"fair_computed_at":null,"clinical_trials":[],"software_tools":[],"db_accessions":[],"linked_datasets":[],"topics":[]}