Selecting the region
The analysis starts from a chosen region of the binary — the code that implements the protocol role under study.
Demo
A guided run on Basic Access Control
Basic Access Control is the protocol an e-passport uses to authenticate a reader before releasing any data. It is small enough to follow end to end, and interesting enough to have known privacy problems. This walkthrough runs CryptoBAP over it, from binary region to verifier verdict.
What you will see
Following the run
Lifting and instrumenting
The region is transpiled to BIR and instrumented with a leakage contract, so the attacker’s observations become part of the program semantics.
Collecting traces
Symbolic execution walks every path through the region, recording the events and observations produced along each one.
Reading the verdict
The extracted Sapic+ model is handed to DeepSec, which decides trace equivalence — the property that unlinkability rests on.
Next