Task-structured probabilistic I/O automata

作者：

Highlights：

• Task-PIOAs, a probabilistic modeling framework based on PIOAs.

• A nondeterministic resolution mechanism tailored for cryptographic applications.

• Notions of external behavior and implementation for task-PIOAs.

• A simulation relation for task-PIOAs that is sound for proving implementation.

• Composition results for task-PIOAs.

摘要

•Task-PIOAs, a probabilistic modeling framework based on PIOAs.•A nondeterministic resolution mechanism tailored for cryptographic applications.•Notions of external behavior and implementation for task-PIOAs.•A simulation relation for task-PIOAs that is sound for proving implementation.•Composition results for task-PIOAs.

论文关键词：Probabilistic automata,I/O automata,Formal modeling,Cryptographic protocols

论文评审过程：Received 25 December 2016, Accepted 16 September 2017, Available online 2 October 2017, Version of Record 14 March 2018.

论文官网地址：https://doi.org/10.1016/j.jcss.2017.09.007