DOC

Mechanical Proofs about BW Multi-Party Contract Signing Protocol

By Gordon Warren,2014-01-21 20:53
7 views 0
Mechanical Proofs about BW Multi-Party Contract Signing Protocol

Mechanical Proofs about BW Multi-Party

    Contract Signing Protocol WWuhanUniversityJournalofNaturalSciences

    ArticleID:10071202(2006)O61516O5

    VoI.11No.6200615161520

    MechanicalProofsaboutBWMulti-Party

    ContractSigningProtocol

    ZHANGNingrong,ZHANGXingyuan,

    WANGYuanyuan

    InstituteofCommandAutonmtion,PIAUniversityof ScienceandTechnology,Nanjing210007,Jiangsu,China Abstract:Wereportontheverificationofanmltiparty

    contractsigningprotocoldescribedbyBaum-Waidnerand Waidner(BW).BasedonPaulson'sinductiveapproach,we givetheprotocolmodelthatincludesinfinitelymanysignalo riesandcontracttextssigningsimultaneously.Weconsider compositeattacksofthedishonestsignatoryandtheexternal intruder,formalizecryptographicprimitivesandprotocol arithmeticincludingattackmodel,showformaldescriptionof keydistribution,andprovesignaturekeysecrecytheorems andfairnesspropertytheoremsoftheBWprotocolusingthe interactivetheoremproverIsabelle/HOI.

    Keywords:formalverification;nmltipartycontractsig

    ningprotocol;inductiveapproach;model

    CLCnumber:TP393.04

    Receiveddate:20060520

    FoundatioRitom:SupportedbytheNafiona1Nalura1ieneeFoun-

dationofChina(60373068)

    Biographv:ZHANGNingrong(1972),female,Ph.D.candidate, researchdirection:informationsecurityandelectroniccomalerce. E-mailningron~zhang@163.coal

    tTowhomcorrespondenceshouktbeaddressed.Email:wangyy@ pubhc1.ppt.Js.cn

    1516

    0IntrOdUCtiOn

    Multi

    partycontractsigningnatoriestosignacontractprotocols[']allowssigtextevenifuptor/lof

    themaredishonest.Suchprotocolsgenerallyconsistinamain protocolandoneorseveralsubprotocols.Themainprotocolis executedinordertoexchangesignaturesonthecontract.The subprotocolsareusedtocontacttheTTPinordertoforcea successfuloutcomeortoaborttheprotoco1.Atsomemoment intheprotoco1.thesignerhavetochoosetocontinuethemain protocolortolaunchasubprotocolbycontactingthetrusted thirdparty(TTP).Subprotocolsmaybeexcutedatamoment notforeseenbytheprotocolandlcadtosubtleflaws.There

    fore,optimisticcontractsigningprotocolsarenotping-pong protocols,butarebranching.Itisdifficulttoanalysesuch protocolssincenopredefinedorderisgiventotheseactions whenspecifyingtheprotoco1.

    Moreover,wegenerallyrequirethatacontractsigning protocolrespectsseveralpropertiesoffairness,completeness andabuse-freenessE.Hence,theuseofformalmethodsto analysesuchprotocolsisveryimportantandnecessary.Shma

    tikovandMitchellE,]usedthefinitestatetoolMurq0toexam

    inetwo-partycontractsigningprotocols.Chadhaetalused

themultisetrewritingformalismcombinedtoinductivemeth

    odstoanalysetwo-partyabuse-freecontractsigning.Chadha etalE]usedmodelcheckerM()CHAtoanalysemultiparty contractsigningprotocols.Butsincethehighnumberofmes

    sageswouldcreateaseriousstateexplosion,theyjustverified BWprotoco1withtwoanduptofivesignersfocusingona contracttext.Specially,theyjustmodeleddishonestpartici

    pantswithoutanexternalintruder.Andtheydidnotexplicitly modelanycryptographicprimitives,butonlythefactthat t豫皤蝴l蝻麟W舢垛lof瞄麟糯薯醢1,'惠一答|

    ?

    j

    ?

protocolmessagescanbesentoutoforde~.

    BasedonPaulson'sinductiveapproach[,wegive formalmodelofBWmultipartycontractsigningprotocol

    includinginfinitelymanysignatoriesandcontracttexts signingsimultaneously.Ourattackmodelincludesnot onlydishonestparticipants.butalsoexternalintruder. Weshowformaldescriptionofkeydistribution,formalize -'??'?'1

    cryptographlcprimitives,provesignaturekeysecrecy theoremsfromtheinductivereasoningabouttheknowl

    edgeofagentwhomayparticipatetheprotoco1.Andwe provetheprotocolgoalsoffairnessusinginteractivetheo

    remprovingtoolIsabelle/HOL(higher-orderlogic)L.

    1ProtocoIModeIandDefinition

    ThedetaileddescriptionoftheBWprotocolisgiven

    inpaper[.Wegivenolimittothenumberofagents whomayparticipate.anddefinefourkindsofagents. ThefollowingdeclarationspecifiestypeagenttoIsabelle. Thetypeofnaturalnumbersisnat.

    datatypeagent=SignernatlTTPlIntruderlVeri

    tier

    ThetypeeventinIsabelledescribesalleventsthat mayhappeninBW.Itisdefinedas;

    typedeclContr

    typedeclTid

    datatypeevent==Saysagentagentmsg

    lGetsagentmsg

    lNew_

    contr"natlist""natlist"TidContr

    Forexample,saysABXdenotesthatagentA

    sendsamessageXtoagentB,GetsAXdenotesthat agentAreceivesX.New

    contrh1dhltidcontrdenotes

    manysignersbegintosignacontract,inwhichhlisthe honestsignerlist,dhlisthedishonestsignerlist,eontr isthesigningcontracttext.tidisaidentifieruniquefor allsimultaneousinstancesoftheBWprotoco1. Datatypemsgintroducesthemessageforms(agent name,roundintheprotocolexecution,contracttext, identifieruniqueofeachprotocolinstance,signaturekey, ,compoundmessage,encryption,resolverequest,TTP' aborteddecision,TTP'signeddecision),definedas: typesround==nat

    datatypemsgAgentagentlRoundroundlCon

    trcontrlTidtidlKeykeylMPairmsgmsglCryptkey

msglResolveroundtidlAbortedagentroundtidlRecov

    eredtid

    BasedonPaulson'sinductiveapproach[.system beha~ourisformalizedasasetoftracesofaboveevents. Accordingtothedefinitionofconcurrentsystem~...the systemforverifyingBWprotocoliswrittenasbwandthe typeofthesystemis(eventlistXevent)set.Theex- pression(r,e)?bwmeansthattheeventeis1egitimate

    tohappenundertrace(event1ist)r,accordingtobw.0f course.theprotocolmodeldoesnotforceeventstohap

    pen,becausemessagesmaybesentbutmaynotbere

    ceived,andagentsmayabandonaprotocolexecution. Theforma1protocolmode1sa(event1istXevent) set.Itisdefinedinductivelyandisunboundedbecauseso areIsabellelists.AUrulesformalizetheinductivesteps. Eachofthemstateshowtoextendagiventraceoftheset wherebytheprotoeoladdsaneweventunderthetrace. 2ModelingBWProtocolwithIntruder

    andDishonestSignatories

    Whenmodelingthehonestbehaviorofaparticipant, weensurethatagivenmessageissentoutonlywhen specifiedbytheprotoco1.Therealwaysexistsomehonest signers.MoreovertheTrPismodeledtobealwayshon

    est.

    However.thedishonestsignersandexternalintrud

    ercansendmessagesOUt0forderandbuildmessages otherthanthoseprescribedbytheBWprotoco1.Weal

    lowthemtotakethecompositeattacksofthefollowing actions:

?impersonateotherroletoparticipatetheproto

    col;

    ?Overhearandinterceptnetworkmessages;

    ?Storeandreplaypartsofoverheardmessagesout oforder;

    ?Decryptencryptedmessagesifhehasthekey, generatemessagesusinganycombinationofhisinitial knowledge,partsofoverheardmessages,knownkeys, etC.

    Givenatracerdenotingthenetworkhistory,we modeltheknowledgethatagentAacquiresasknowsA r.Thisisthesetofmessagesincludinginitialmessages aboutkeydistributionandsomemessagesestablishedby inspectingThespecialsetsynth(analz(knowsAr)) containsallmessagesthatagentAcansynthesizeusing thecomponentsobtainedfromtheanalysisofthetraffic, evenwiththehelpofcorruptagents'privatekeys. AgentAmaybeadishonestsignerortheintruder.When modelingthedishonestbehavioroftheparticipantA,we 1517

    allowthathesendanymessagederivedfromtheset synth(anah(knowsA)).

    Forlackofspace,weshowpartialinductivedefini

    tionoftheBWprotocoIinFig.1.TheBrulemodels howtwoormorethantwosignatoriesbeginanewin

    stanceoftheBWprotocolusingfunctiontid

    is

    diff.tid

    isuniqueidentifierforeachinstance.Theprotocolmodel

    allowsthatasignerisinpluralinstancesoftheBWpro toed.Maybeheisanhonestparticipantinoneinstance, alsoisadishonestparticipantinanotherinstance.For eachinstanceweusetwolists("hi"and"dhl")torecord honestanddishonestsignatories,andavoidrepeatrecord usingfunctiondistinct.TheB2rulemodelsthateach GetseventmustfollowamatchingSaysevent.TheB3 andBrulesmodelhowhonestsignatorieswouldperform theBWprotocolsteps[.TheB1zandB13rulesmodel compositeattacksofthedishonestsignatoryandoutside intruder,usingthefunctionssynthandanah. Constsbw::"(eventlist×event)"set

    indt,clivebw

    intros

    B1:"[tid_isdiff(r,tid)distinct(hl@dh1);2?lengthdh1]

    (r,Newcontrh1dh1tideontr)Ebw"

    ;=}:"?B;SaysABXEsetr_j(r,GetsBX)Ebw"

    B3:"[Mew_contrhldhltidcontrEsetr,imenhl; JmemhlJmerndhl;iT/-j;

    r<lengthh1+lengthdhl+;1raised_exception(r,itid)] (r,Says(Signer)(SignerJ)(Crypt(spriKitid){Tidtid, Round(Sucr)}))Ebw"

    B"[New_contrhldhltidcontrEsetr;(J::nat)?rj

    r~lengthhl+lengthdhl+J:

    memh1;qraised_exception(r,itid);

    sendall

    in_

    rrihldhlftid;7recall

    inrrihldhlrtia]

    (r,Says(Signer)TTP(Crypt(spriKitid)

    {Resolverrid,multi_msg(reed(hl@dh1)irtid)tid}))E bw"

    :

    BI2:"[New_eontrhldhltidcontrEsetrTinlenlhl; X?synth(ana1z(knows(Signer)f));

    Vrid.tid?tid+tid?contain_ridX;

    SigneriEbad~'-Key(p"K(Signer))?containmsgx;

    Signerbad~a.,Key(pfiKirid)?contain_msgX]

    (r,Says(Signeri)BX)?bw"

    B13:"X?synth(analz(knowsIntruderr))

    (r,SaysIntruderBX)Ebw"

    Fig.1InductiveDefinitionoftheBWPmt~l

    3SignatureKeySecrecyTheorems

    3.1Formal

    Thekey

    acteristicsof

    1518

    DescriptionofKeyDistribution

    distributioniSrelatedtothebehaviorchar

    eachagentwhoparticipatestheprotoco1.

    WelucubratetheBWprotocol?clarifythedefinitionof dishonestsignatoriesandcorruptsignatories.Weassume thedishonestsignatoriesdonothavetofollowtheproto

    col,asspokeninSection2.Ontheotherhand,weas sumethatcorruptsignatoriessharetheirprivatekeyeach other,andwithexternalintruder.Adishonestsignatory maybeacorruptsignatory,ornot.

    badsetinIsabe11econtainsa11corruDtsignatories' andexternalintruder.TTPandVerifieraremodeledto bealwaysabsentfrombadset.j

constsbad::"agentset''

    axiores

    Intruderin_bad:"IntruderEbad"

    TTP

    not

    in_bad:"TTPq:bad''

    Verifier_

    notinbad:"Verifier~bad''

    Forabusefreeness,BWprotocolleteachsignatory Pgenerateafreshpairofsecretandpublicsignature key,(sk,)shorttermkeystoobtainthepre-con

    tract,andthattheprotocoluseslongtermkeystocon vertthepre-contractintorea1contract.Theimageofa setunderafunctioniSamostusefulnotion.Ithastheob

    viousdefinitionintheinteractivetheoremproverlsabelle/ H0L:

    {y.EA.Y一向}(imagedef)

    WeusefunctioninitStatetoshowinitialdistribution ofsignaturekeysthatarelong-termkeysofeachsigner. Long_

    termpublickeysareopen,butlong

    termprivate

    keysisknownbyoneselforsharedinbadset. constdefsinitState::"agent=>msgset'' "initStateagt~-

    (ifagtbad

    then{Key(priKago)U(Key,rangepubK)

    else(Key,invKey,pubK,bad)

    U(Key,rangepubK))"

    declareinitState_def[simp]

OncetheeventNew_

    contrhldhJtidcontrhappens, westartthedisrtibutionofshorttermkeysthatrelateto

    agentandidentifiertid,shownasFig.2:.

    InIsabelle,wegivedistributionofshort-termsig

    naturekeysusingkeys

    distri,all

    spubK,bad

    signer

    ?

    list,bad

    spriKfunctions.

    constskeys_

    distri::

    "

    agent=>natlist->Tid->msgset"

    primrec"keys_

    distri(Signer)nltid

    (ifSignerEbad

    then(ifimemnlVbad_

    signer_

    listnl4-

    thenbadspriKnltidUallspubKnltid

AgentHTTP

    Intruder

    Verifier

    ?bad

    Ifheparticipatessigningfor tidorexistscorruptsigner

Report this document

For any questions or suggestions please email
cust-service@docsford.com