1
Q
How does Applied Pi-Calculus work?
A
Processes correspond to agents.
Sending messages modelled as communication in process calculus.
Attacker modelled as an arbitary process running in parallel with agent processes.
2
Q
What capabilities does Proverif have?
A
Reachability properties: Is a certain event reachable?
Correspondance assertions: if event e executed, then event e’ has been previously executed.
Observational equivalences: An attacker cannot tell which of two processes has been executed.
