Compositional analysis of contract-signing protocols
Identifieur interne : 005807 ( Main/Merge ); précédent : 005806; suivant : 005808Compositional analysis of contract-signing protocols
Auteurs : Michael Backes [Allemagne] ; Anupam Datta [États-Unis] ; Ante Derek [États-Unis] ; John C. Mitchell [États-Unis] ; Mathieu Turuani [France]Source :
- Theoretical computer science [ 0304-3975 ] ; 2006.
Descripteurs français
- Pascal (Inist)
English descriptors
- KwdEn :
Abstract
We develop a general method for proving properties of contract-signing protocols using a specialized protocol logic. The method is applied to the Asokan-Shoup-Waidner and the Garay-Jacobson-MacKenzie protocols. Our method offers certain advantages over previous analysis techniques. First, it is compositional: the security guarantees are proved by combining the independent proofs for the three subprotocols of each protocol. Second, the formal proofs are carried out in a "template" form, which gives us a reusable proof that may be instantiated for the two example protocols, as well as for other protocols with the same arrangement of messages. Third, the proofs follow the design intuition. In particular, in proving game-theoretic properties like fairness, we demonstrate success for the specific strategy that the protocol designer had in mind, instead of non-constructively proving that a strategy exists. Finally, our logical proofs demonstrate security when an unbounded number of sessions are executed in parallel.
Links toward previous steps (curation, corpus...)
- to stream PascalFrancis, to step Corpus: 000408
- to stream PascalFrancis, to step Curation: 000625
- to stream PascalFrancis, to step Checkpoint: 000402
Links to Exploration step
Pascal:07-0027112Le document en format XML
<record><TEI><teiHeader><fileDesc><titleStmt><title xml:lang="en" level="a">Compositional analysis of contract-signing protocols</title><author><name sortKey="Backes, Michael" sort="Backes, Michael" uniqKey="Backes M" first="Michael" last="Backes">Michael Backes</name><affiliation wicri:level="1"><inist:fA14 i1="01"><s1>Saarland University</s1><s3>DEU</s3><sZ>1 aut.</sZ></inist:fA14><country>Allemagne</country><wicri:noRegion>Saarland University</wicri:noRegion><wicri:noRegion>Saarland University</wicri:noRegion></affiliation></author><author><name sortKey="Datta, Anupam" sort="Datta, Anupam" uniqKey="Datta A" first="Anupam" last="Datta">Anupam Datta</name><affiliation wicri:level="1"><inist:fA14 i1="02"><s1>Stanford University</s1><s3>USA</s3><sZ>2 aut.</sZ><sZ>3 aut.</sZ><sZ>4 aut.</sZ></inist:fA14><country>États-Unis</country><wicri:noRegion>Stanford University</wicri:noRegion></affiliation></author><author><name sortKey="Derek, Ante" sort="Derek, Ante" uniqKey="Derek A" first="Ante" last="Derek">Ante Derek</name><affiliation wicri:level="1"><inist:fA14 i1="02"><s1>Stanford University</s1><s3>USA</s3><sZ>2 aut.</sZ><sZ>3 aut.</sZ><sZ>4 aut.</sZ></inist:fA14><country>États-Unis</country><wicri:noRegion>Stanford University</wicri:noRegion></affiliation></author><author><name sortKey="Mitchell, John C" sort="Mitchell, John C" uniqKey="Mitchell J" first="John C." last="Mitchell">John C. Mitchell</name><affiliation wicri:level="1"><inist:fA14 i1="02"><s1>Stanford University</s1><s3>USA</s3><sZ>2 aut.</sZ><sZ>3 aut.</sZ><sZ>4 aut.</sZ></inist:fA14><country>États-Unis</country><wicri:noRegion>Stanford University</wicri:noRegion></affiliation></author><author><name sortKey="Turuani, Mathieu" sort="Turuani, Mathieu" uniqKey="Turuani M" first="Mathieu" last="Turuani">Mathieu Turuani</name><affiliation wicri:level="1"><inist:fA14 i1="03"><s1>LORIA-INRIA Nancy</s1><s3>FRA</s3><sZ>5 aut.</sZ></inist:fA14><country>France</country><wicri:noRegion>LORIA-INRIA Nancy</wicri:noRegion><wicri:noRegion>LORIA-INRIA Nancy</wicri:noRegion></affiliation></author></titleStmt><publicationStmt><idno type="wicri:source">INIST</idno><idno type="inist">07-0027112</idno><date when="2006">2006</date><idno type="stanalyst">PASCAL 07-0027112 INIST</idno><idno type="RBID">Pascal:07-0027112</idno><idno type="wicri:Area/PascalFrancis/Corpus">000408</idno><idno type="wicri:Area/PascalFrancis/Curation">000625</idno><idno type="wicri:Area/PascalFrancis/Checkpoint">000402</idno><idno type="wicri:explorRef" wicri:stream="PascalFrancis" wicri:step="Checkpoint">000402</idno><idno type="wicri:doubleKey">0304-3975:2006:Backes M:compositional:analysis:of</idno><idno type="wicri:Area/Main/Merge">005807</idno></publicationStmt><sourceDesc><biblStruct><analytic><title xml:lang="en" level="a">Compositional analysis of contract-signing protocols</title><author><name sortKey="Backes, Michael" sort="Backes, Michael" uniqKey="Backes M" first="Michael" last="Backes">Michael Backes</name><affiliation wicri:level="1"><inist:fA14 i1="01"><s1>Saarland University</s1><s3>DEU</s3><sZ>1 aut.</sZ></inist:fA14><country>Allemagne</country><wicri:noRegion>Saarland University</wicri:noRegion><wicri:noRegion>Saarland University</wicri:noRegion></affiliation></author><author><name sortKey="Datta, Anupam" sort="Datta, Anupam" uniqKey="Datta A" first="Anupam" last="Datta">Anupam Datta</name><affiliation wicri:level="1"><inist:fA14 i1="02"><s1>Stanford University</s1><s3>USA</s3><sZ>2 aut.</sZ><sZ>3 aut.</sZ><sZ>4 aut.</sZ></inist:fA14><country>États-Unis</country><wicri:noRegion>Stanford University</wicri:noRegion></affiliation></author><author><name sortKey="Derek, Ante" sort="Derek, Ante" uniqKey="Derek A" first="Ante" last="Derek">Ante Derek</name><affiliation wicri:level="1"><inist:fA14 i1="02"><s1>Stanford University</s1><s3>USA</s3><sZ>2 aut.</sZ><sZ>3 aut.</sZ><sZ>4 aut.</sZ></inist:fA14><country>États-Unis</country><wicri:noRegion>Stanford University</wicri:noRegion></affiliation></author><author><name sortKey="Mitchell, John C" sort="Mitchell, John C" uniqKey="Mitchell J" first="John C." last="Mitchell">John C. Mitchell</name><affiliation wicri:level="1"><inist:fA14 i1="02"><s1>Stanford University</s1><s3>USA</s3><sZ>2 aut.</sZ><sZ>3 aut.</sZ><sZ>4 aut.</sZ></inist:fA14><country>États-Unis</country><wicri:noRegion>Stanford University</wicri:noRegion></affiliation></author><author><name sortKey="Turuani, Mathieu" sort="Turuani, Mathieu" uniqKey="Turuani M" first="Mathieu" last="Turuani">Mathieu Turuani</name><affiliation wicri:level="1"><inist:fA14 i1="03"><s1>LORIA-INRIA Nancy</s1><s3>FRA</s3><sZ>5 aut.</sZ></inist:fA14><country>France</country><wicri:noRegion>LORIA-INRIA Nancy</wicri:noRegion><wicri:noRegion>LORIA-INRIA Nancy</wicri:noRegion></affiliation></author></analytic><series><title level="j" type="main">Theoretical computer science</title><title level="j" type="abbreviated">Theor. comput. sci.</title><idno type="ISSN">0304-3975</idno><imprint><date when="2006">2006</date></imprint></series></biblStruct></sourceDesc><seriesStmt><title level="j" type="main">Theoretical computer science</title><title level="j" type="abbreviated">Theor. comput. sci.</title><idno type="ISSN">0304-3975</idno></seriesStmt></fileDesc><profileDesc><textClass><keywords scheme="KwdEn" xml:lang="en"><term>Computer theory</term><term>Contract signing</term><term>Logic</term><term>Security protocol</term><term>Signing</term><term>Strategy</term></keywords><keywords scheme="Pascal" xml:lang="fr"><term>Signature</term><term>Logique</term><term>Stratégie</term><term>Informatique théorique</term><term>Protocole sécurité</term><term>Signature contrat</term></keywords></textClass></profileDesc></teiHeader><front><div type="abstract" xml:lang="en">We develop a general method for proving properties of contract-signing protocols using a specialized protocol logic. The method is applied to the Asokan-Shoup-Waidner and the Garay-Jacobson-MacKenzie protocols. Our method offers certain advantages over previous analysis techniques. First, it is compositional: the security guarantees are proved by combining the independent proofs for the three subprotocols of each protocol. Second, the formal proofs are carried out in a "template" form, which gives us a reusable proof that may be instantiated for the two example protocols, as well as for other protocols with the same arrangement of messages. Third, the proofs follow the design intuition. In particular, in proving game-theoretic properties like fairness, we demonstrate success for the specific strategy that the protocol designer had in mind, instead of non-constructively proving that a strategy exists. Finally, our logical proofs demonstrate security when an unbounded number of sessions are executed in parallel.</div></front></TEI><affiliations><list><country><li>Allemagne</li><li>France</li><li>États-Unis</li></country></list><tree><country name="Allemagne"><noRegion><name sortKey="Backes, Michael" sort="Backes, Michael" uniqKey="Backes M" first="Michael" last="Backes">Michael Backes</name></noRegion></country><country name="États-Unis"><noRegion><name sortKey="Datta, Anupam" sort="Datta, Anupam" uniqKey="Datta A" first="Anupam" last="Datta">Anupam Datta</name></noRegion><name sortKey="Derek, Ante" sort="Derek, Ante" uniqKey="Derek A" first="Ante" last="Derek">Ante Derek</name><name sortKey="Mitchell, John C" sort="Mitchell, John C" uniqKey="Mitchell J" first="John C." last="Mitchell">John C. Mitchell</name></country><country name="France"><noRegion><name sortKey="Turuani, Mathieu" sort="Turuani, Mathieu" uniqKey="Turuani M" first="Mathieu" last="Turuani">Mathieu Turuani</name></noRegion></country></tree></affiliations></record>Pour manipuler ce document sous Unix (Dilib)
EXPLOR_STEP=$WICRI_ROOT/Wicri/Lorraine/explor/InforLorV4/Data/Main/Merge
HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 005807 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/Main/Merge/biblio.hfd -nk 005807 | SxmlIndent | more
Pour mettre un lien sur cette page dans le réseau Wicri
{{Explor lien
|wiki= Wicri/Lorraine
|area= InforLorV4
|flux= Main
|étape= Merge
|type= RBID
|clé= Pascal:07-0027112
|texte= Compositional analysis of contract-signing protocols
}}
| This area was generated with Dilib version V0.6.33. |  |