Using Task-Structured Probabilistic I/O Automata to Analyze Cryptographic Protocols

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

inria-00080681, version 1

Using Task-Structured Probabilistic I/O Automata to Analyze Cryptographic Protocols

Ran Canetti ^1, 2, Ling Cheung ³, Dilsun Kaynar ², Moses Liskov ⁴, Nancy Lynch ², Olivier Pereira ⁵, Roberto Segala ⁶

Workshop on Formal and Computational Cryptography (FCC 2006) (2006)

Abstract: The Probabilistic I/O Automata (PIOA) framework of Lynch, Segala and Vaandrager provides tools for precisely specifying protocols and reasoning about their correctness based on implementation relationships between multiple levels of abstraction. We enhance this framework to allow the analysis of protocols that use cryptographic primitives. For this purpose, we propose new techniques for handling nondeterministic behaviors, expressing computationally hardness assumptions, and for proving security in a composable setting.

1: IBM Watson Research Center
IBM
2: Computer Science and Artificial Intelligence Laboratory (CSAIL)
Massachussetts Institute of Technology (MIT)
3: nijmeegs instituut voor informatica en informatiekunde/informatics for technical applications (NIII)
Radboud university of Nijmegen
4: W&M Computer Science department
The College of William and Mary
5: UCL Crypto Group
Université Catholique de Louvain (UCL) - Belgique
6: Department of Computer Science / Dipartimento di Informatica [Verona]
University of Verona – Università degli studi di Verona

inria-00080681, version 1
http://hal.inria.fr/inria-00080681
oai:hal.inria.fr:inria-00080681
From: Véronique Cortier <>
Submitted on: Tuesday, 20 June 2006 15:00:27
Updated on: Tuesday, 20 June 2006 15:27:36

See detailed view

Associated documents

PDF :

Export

Bibtex EndNote TEI RefWorks

<?xml version="1.0" encoding="UTF-8"?>
<listBibl xmlns="http://www.tei-c.org/ns/1.0" xmlns:xlink="http://www.w3.org/1999/xlink" xmlns:mml="http://www.w3.org/1998/Math/MathML">
<listBibl type="inproceedings"><head>Peer-reviewed conferences/proceedings</head>
<biblStruct type="inproceedings" xml:id="inria-00080681"><analytic>
<author><persName><forename>Ran</forename><surname>Canetti</surname></persName>
<affiliation>
<orgName type="team">IBM Watson Research Center</orgName>
<country>US</country>
<orgName type="institution">IBM</orgName>
</affiliation>
<affiliation>
<orgName type="laboratory">CSAIL</orgName>
<orgName type="team">Computer Science and Artificial Intelligence Laboratory</orgName>
<country>US</country>
<orgName type="institution">Massachussetts Institute of Technology (MIT)</orgName>
</affiliation>
</author>
<author><persName><forename>Ling</forename><surname>Cheung</surname></persName>
<affiliation>
<orgName type="laboratory">NIII</orgName>
<orgName type="team">nijmeegs instituut voor informatica en informatiekunde/informatics for technical applications</orgName>
<country>NL</country>
<orgName type="institution">Radboud university of Nijmegen</orgName>
</affiliation>
</author>
<author><persName><forename>Dilsun</forename><surname>Kaynar</surname></persName>
<affiliation>
<orgName type="laboratory">CSAIL</orgName>
<orgName type="team">Computer Science and Artificial Intelligence Laboratory</orgName>
<country>US</country>
<orgName type="institution">Massachussetts Institute of Technology (MIT)</orgName>
</affiliation>
</author>
<author><persName><forename>Moses</forename><surname>Liskov</surname></persName>
<affiliation>
<orgName type="team">W&M Computer Science department</orgName>
<country>US</country>
<orgName type="institution">The College of William and Mary</orgName>
</affiliation>
</author>
<author><persName><forename>Nancy</forename><surname>Lynch</surname></persName>
<affiliation>
<orgName type="laboratory">CSAIL</orgName>
<orgName type="team">Computer Science and Artificial Intelligence Laboratory</orgName>
<country>US</country>
<orgName type="institution">Massachussetts Institute of Technology (MIT)</orgName>
</affiliation>
</author>
<author><persName><forename>Olivier</forename><surname>Pereira</surname></persName>
<affiliation>
<orgName type="team">UCL Crypto Group</orgName>
<country>BE</country>
<orgName type="institution">Université Catholique de Louvain (UCL) - Belgique</orgName>
</affiliation>
</author>
<author><persName><forename>Roberto</forename><surname>Segala</surname></persName>
<affiliation>
<orgName type="team">Department of Computer Science / Dipartimento di Informatica [Verona]</orgName>
<country>IT</country>
<orgName type="institution">University of Verona</orgName>
<orgName type="institution">Università degli studi di Verona</orgName>
</affiliation>
</author>
<title type="main" level="a">Using Task-Structured Probabilistic I/O Automata to Analyze Cryptographic Protocols</title></analytic><monogr><meeting>Workshop on Formal and Computational Cryptography (FCC 2006)</meeting><imprint><pubPlace><settlement>Venice</settlement><country>Italy</country></pubPlace><biblScope type="publicationDate">2006-07-09</biblScope></imprint></monogr><idno type="HALid">http://hal.inria.fr/inria-00080681</idno><idno type="HALFile">http://hal.inria.fr/inria-00080681/PDF/paper7.pdf</idno></biblStruct>
</listBibl>
</listBibl>