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.

错误:搜索内容不能为空,请输入英文关键词
错误:关键词超出字数限制,请精简
高级检索

Syntax and operational semantics for security protocols

  • Reynaldo Gil-Pons,
  • Ross Horne,
  • Sjouke Mauw,
  • Felix Stutz,
  • Semen Yurkov

摘要

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.