Security Protocol Verification using Task-PIOAs

This five-year project, funded primarily by an NSF ITR grant with PIs Lynch, Micali, and Rivest, is developing a new formal framework for modeling and analyzing security protocols. The framework is in the general style of the I/O automata and probabilistic I/O automata frameworks used for modeling distributed algorithms, that is, they consist of abstract state machines that can be composed and that can describe systems at different levels of abstraction. However, the new framework also allows expression of computational issues that are important in the analysis of security protocols.

Basic Theory of Task-PIOAs

The formal foundation for the framework is the task-PIOA framework, which is a variant of Segala's well-known PIOA framework. The key addition in the task-PIOA framework is a less powerful mechanism for resolving nondeterministic 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.
  • The most up-to-date version of this work is our new journal submission: pdf (2007). This version includes minor corrections to the WODES version, such as changing the definition of simulation relation so that it applies to executions rather than to execution fragments.
  • A slightly earlier version appears as the MIT CSAIL Technical Report MIT-CSAIL-TR-2006-060 (September 2006).
  • A still earlier version appeared in the proceedings of the 8th International Workshop on Discrete Event Systems (WODES'06), Ann Arbor, Michigan, July 2006: pdf.
  • A preliminary version of the WODES paper 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. In fact, this case study formed the initial motivation for the development of the framework. The papers with titles beginning with "Using Probabilistic Automata..." represent our first version of the case study. They use rather strong restrictions on the branching capabilities of the environment model, and are based on a preliminary version of the task-PIOA model, which includes an equivalence relation on states as well as one on actions. These papers include analysis for four kinds of adversaries. The later papers, with titles referring to "Task-Structured" automata, allow environments with more powerful branching capabilities, and are based on the newer task-PIOA model, without the equivalence relation on states. However, these later papers include analysis of just one kind of adversary---a corrupted receiver.
• Analyzing Security Protocols Using Time-Bounded Task-PIOAs.
  Ran Canetti, Ling Cheung, Dilsun Kaynar, Moses Liskov, Nancy Lynch, Olivier Pereira, and Roberto Segala.
  • A good summary of our work on this case study appears in the 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). This version improves on CSAIL-TR-2006-019 by making some minor corrections and changing the definition of a simulation relation to be on executions rather than execution fragments.
  • An earlier version appears as MIT-CSAIL-TR-2006-019 (March 2006). This version differs from CSAIL-TR-2006-046 in that it removes the state relation from the basic definition of a task-PIOA and does only one case of the proof, for one kind of adversary (receiver corrupted).
  • Cryptology ePrint Archive Report 2005/452: html. This report has four versions. The last two are for this paper, whereas the first two are for the "Using Probabilistic I/O Automata..." paper described below.
• 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 Analyze an Oblivious Transfer Protocol.
  Ran Canetti, Ling Cheung, Dilsun Kaynar, Moses Liskov, Nancy Lynch, Olivier Pereira, and Roberto Segala.
  • The last version of our case study, prior to generalizing the basic task-PIOA definition to remove the state relation, appears in MIT CSAIL Technical Report MIT-CSAIL-TR-2006-046 (June 2006), which represents a slight improvement over MIT-LCS-TR-1001a. This version includes the state relation for task-PIOAs and covers four cases, for four different kinds of adversaries. The CSAIL-TR-2006-046 and LCS-TR-1001a reports are the same as the second and first versions of the ePrint Archive Report 2005/452, described below.
  • An earlier version of the 2006-046 TR appears as MIT-CSAIL-TR-2005-055 (December 2005), also cited as MIT-LCS-TR-1001.
  • Cryptology ePrint Archive Report 2005/452: html. This report has four versions. The first two are for this paper, whereas the last two are for the "Using Task-Structured Probabilistic I/O Automata..." paper described above. The second eprint version is the same as CSAIL-TR-2006-046 above. The first is the same as LCS-TR-1001a.
• 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

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

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.
A stronger version of our long-term implementation relation, based on conditional probability, is proposed in the "Version 2" report.
• Modeling Computational Security in Long-Lived Systems.
  Ran Canetti, Ling Cheung, Dilsun Kaynar, Nancy Lynch, and Olivier Pereira.
  • Conference version in CONCUR 2008: 19th International Conference on Concurrency Theory, Toronto, Canada, August 2008. pdf
  • Full version in Cryptology ePrint Archive Report 2007/406. html
• Modeling Computational Security in Long-Lived Systems, Version 2.
  Ran Canetti, Ling Cheung, Dilsun Kaynar, Nancy Lynch, and Olivier Pereira.
  • Cryptology ePrint Archive Report 2008/584. html
  • This report is also available as MIT-CSAIL-TR-2008-068. html

Applications and Case Studies

Some other related work includes an application of the task-PIOA framework to a case study involving verifying statistical zero knowledge, and a preliminary study of automatic verification of simulatability properties of security protocols.
• 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 Fourth International Conference on Information Assurance and Security, Naples, Italy, September 2008.
  • 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