Syntax and operational semantics for security protocols
摘要
This chapter introduces an operational semantics for a core of the applied π-calculus, sufficient to capture a range of protocols and threat models. The basics of syntax, binders and substitutions are explained. The syntax of threads modelling the behaviour of an individual role in a protocol is explained in relation to message sequence charts modelling protocols globally. An operational semantics is provided for threads, defining how honest agents behave in an adversarial environment. Secrecy is defined and a modal logic for expressing attacks is introduced. The operational semantics are then extended to networks where many threads may run concurrently. Exercises help the reader gain a feel for the rules of the operational semantics.