Adversary Safety by Construction in a Language of Cryptographic Protocols
2022 IEEE 35th Computer Security Foundations Symposium (CSF)(2022)
摘要
Compared to ordinary concurrent and distributed systems, cryptographic protocols are distinguished by the need to reason about interference by adversaries. We suggest a new layered approach to tame that complexity, via an executable protocol language whose semantics does not reveal an adversary directly, instead enforcing a set of intuitive hygiene rules. By virtue of those rules, protocols written in this language provably behave identically with or without interference by active Dolev-Yao-style adversaries. As a result, formal reasoning about protocols can be simplified enough that even naïve model checking can establish correctness of a multiparty protocol, through analysis of a state space with no adversary. We present the design and implementation of SPICY, short for Secure Protocols Implemented CorrectlY, including the semantics of its input languages; the essential safety proofs, formalized in the Coq theorem prover; and the automation techniques. We provide a preliminary evaluation of the tool's performance and capabilities via a handful of case studies.
更多查看译文
关键词
formal verification,coq,cryptography,protocol analysis
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络
Chat Paper
正在生成论文摘要