State Paper

State Paper

Ideas, case studies, open problems, etc.

Positioning

First, define and motivate niche. Then, show that we handle this niche. Our niche is the combination of reasoning about message deduction in the context of equational theories and a protocol with stateful control flow.

Case Studies

• Contract signing: ASW from StatVerif paper

• Certificate revocation: case studies done by ourselves

• TPM protocols: Envelope and BitLocker from TPM state register paper

• RFID protocols: StateVerif case study

  Saša Radomirović pointed us to the HHMB07 protocol in the Attacks on RFID protocos paper.

• Vehicular network protocols as investigated by Abstract Set membership paper by Moedersheim

Proof techniques

• abstract interpretation: forward derivation of additional invariants
• unique fact instances
• detect set of loop breakers and replace them with invariant denoting consequence of solving them