Symbolic Verification of Computational Security for Branching-Time Properties

zum Volltext (264 kB)   ZIP
Beteiligte Person(en) / Institution(en)Autor :
DatumErschienen :
  • September 2008
Seitenbereich30 S.

Two different models for security of cryptographic protocols have been developed: Symbolic security is an abstract notion which can often be verified automatically. Computational security is defined in a realistic concurrent model against arbitrary, randomized polynomial-time attacks. A recent research trend is to prove that often, these security notions coincide, thereby transferring the decidability results from the abstract setting into the more realistic computational model. Previous results in this area are only concerned with trace properties, i.e., security goals that can be characterized as properties of single protocol runs. We prove the first equivalence result for a more complex class of goals, which include balance for contract signing protocols. Our result shows that computational security for these protocols can be verified automatically. The proof relies on a careful "derandomization" of realistic attacks.
Statische URL
IDNummer des Berichts :
  • TR_0809