Task-PIOAs and Security Verification

Basic Theory of Task-PIOAs

The task-PIOA framework is a variant of the PIOA framework. It's defining feature is a less powerful mechanism for resolving nondeterminstic choices. This mechanism is based on the notion of tasks, which are equivalence classes of system actions that are scheduled by oblivious, global task sequences.
• Task-Structured Probabilistic I/O Automata.
  Ran Canetti, Ling Cheung, Dilsun Kaynar, Moses Liskov, Nancy Lynch, Olivier Pereira and Roberto Segala.
  • Journal submission (2007).
  • MIT CSAIL Technical Report MIT-CSAIL-TR-2006-060 (September 2006).
  • In Proceedings of the 8th International Workshop on Discrete Event Systems (WODES'06), Ann Arbor, Michigan, July 2006. pdf
  • An earlier tech report version appears as MIT-CSAIL-TR-2006-023 (March 2006).

Oblivious Transfer Case Study

We have successfully applied the task-PIOA framework to analyze an oblivious transfer protocol.
• Analyzing Security Protocol Using Time-Bounded Task-PIOAs.
  Ran Canetti, Ling Cheung, Dilsun Kaynar, Moses Liskov, Nancy Lynch, Olivier Pereira, and Roberto Segala.
  • In Journal of Discrete Event Dynamic Systems (DEDS), volume 18, number 1, March 2008. pdf
• Using Task-Structured Probabilistic I/O Automata to Analyze an Oblivious Transfer Protocol.
  Ran Canetti, Ling Cheung, Dilsun Kaynar, Moses Liskov, Nancy Lynch, Olivier Pereira and Roberto Segala.
  • In Proceedings of the 20th International Symposium on Distributed Computing (DISC'06), Stockholm, Sweden, September 2006. pdf
  • MIT CSAIL Technical Report MIT-CSAIL-TR-2006-047 (June 2006).
  • An earlier version appears as MIT-CSAIL-TR-2006-019 (March 2006).
• Using Probabilistic I/O Automata to Analyze an Oblivious Transfer Protocol.
  Ran Canetti, Ling Cheung, Dilsun Kaynar, Moses Liskov, Nancy Lynch, Olivier Pereira and Roberto Segala.
  • MIT CSAIL Technical Report MIT-CSAIL-TR-2006-046 (June 2006), also cited as MIT-LCS-TR-1001a.
  • An earlier version appears as MIT-CSAIL-TR-2005-055 (December 2005), also cited as MIT-LCS-TR-1001.
  • Cryptology ePrint Archive Report 2005/452. html

Scheduling in Simulation-Based Security

we add a new dimension to the analysis of simulation-based security, namely, the scheduling of concurrent processes. We show that, when we move from sequential scheduling (as used in previous studies) to task-based nondeterministic scheduling, the same logical statement gives rise to incomparable notions of security. Under task-based scheduling, the hierarchy based on placement of ``master process'' becomes obsolete, because no such designation is necessary to obtain meaningful runs of a system. On the other hand, the existence of ``forwarder processes'' remains an important factor.
• On the Role of Scheduling in Simulation-Based Security
  Ran Canetti, Ling Cheung, Nancy Lynch, and Olivier Pereira.
  • In 7th International Workshop on Issues in the Theory of Security (WITS'07), Braga, Portugal, March 2007. pdf
  • Cryptology ePrint Archive Report 2007/102. html

Compositional Security

We define secure emulation for the task-PIOA framework, in the spirit of UC-emulation proposed by Canetti. Our notion of secure emulation is composable, and is preserved when we apply a hiding operator.
• Compositional Security for Task-PIOAs.
  Ran Canetti, Ling Cheung, Dilsun Kaynar, Nancy Lynch, and Olivier Pereira.
  • In Proceedings of the 20th IEEE Computer Security Foundations Symposium, Venice, Italy, July 2007. pdf
• Using Task-Structured Probabilistic I/O Automata to Analyze Cryptographic Protocols.
  Ran Canetti, Ling Cheung, Dilsun Kaynar, Moses Liskov, Nancy Lynch, Olivier Pereira, and Roberto Segala.
  • In Proceedings of the Workshop on Formal and Computational Cryptography - FCC 2006, pp. 34-39, July 2006. pdf
• Using Probabilistic I/O Automata to Improve the Analysis of Cryptographic Protocols.
  Ran Canetti, Ling Cheung, Dilsun Kaynar, Moses Liskov, Nancy Lynch, Olivier Pereira, and Roberto Segala.
  • In ERCIM News 63:40-41, October 2005. html

Modeling Long-Lived Security

This work proposes a new paradigm for the analysis of long-lived security protocols. Entities are active for a potentially unbounded amount of real time, provided they perform only a polynomial amount of work per unit of real time. Moreover, the space used by these entities is allocated dynamically and must be polynomially bounded. A new notion of long-term implementation is proposed and shown to be preserved under polynomial parallel composition and exponential sequential composition. The use of this new paradigm is illustrated in an analysis of the long-lived timestamping protocol of Haber and Kamat.
• Modeling Computational Security in Long-Lived Systems.
  Ran Canetti, Ling Cheung, Dilsun Kaynar, Nancy Lynch, and Olivier Pereira.
  • To appear in CONCUR 2008: 19th International Conference on Concurrency Theory, Toronto, Canada, August 2008. pdf
  • Cryptology ePrint Archive Report 2007/406. html

Applications and Case Studies

• Verifying Statistical Zero Knowledge with Approximate Implementations
  Ling Cheung, Sayan Mitra, and Olivier Pereira.
  • Cryptology ePrint Archive Report 2007/195. html
• Automatic Verification of Simulatability in Security Protocols.
  Tadashi Araragi and Olivier Pereira.
  • In Proceedings of the Workshop on Formal and Computational Cryptography FCC 2007, July 2007.

People

• Ran Canetti
• Ling Cheung
• Dilsun Kaynar
• Moses Liskov
• Nancy Lynch
• Olivier Pereira
• Roberto Segala