Modified-Wide-Mouthed-Frog-Protocol

ModifiedWide-Mouthed-FrogProtocolThesecondexampleillustratesthe`gap'thatexistsbetweenan`idealized'versionofaprotocolanditsactualimplementation.Table4-bshowsamodifiedversionofthe`wide-mouthed-frogprotocol'(table4-a;seealso[1]).Theroleofthetwotimestampsintheoriginalprotocolisnowplayedbyanonce,thusremovingtheneedforsynchronizedclocks.However,anextra(first)messagehastobesent.Table4:Thewide-mouthed-frogprotocolWhenthisprotocolisanalysedthroughtheBAN-logic,themessageshavetobeidealizedandtheinitialassumptionshavetobelisted.Thefirstmessageisomitted,sinceitdoesnotcontributetothelogicalpropertiesoftheprotocol.Table5:Thewide-mouthed-frogprotocolSinceBtrustsS,whichsaysthatAconveyed,BtrustsA'sjurisdictionoverthegenerationofsuchkeys,andBknowsthatthelastmessageis`fresh'(itcontains),Bcanbelieve.IntheBAN-logic,theparticipantsshouldbeabletorecognizeandignoreitsownmessages.Therearetwopossibilities:eithereveryparticipantstoreseverymessagesentinadatabaseandcheckseverymessagereceivedwhetherornotitisincludedinthatdatabase,or,everyparticipantmakessurethathecanrecognizethatareceivedmessagecouldnotpossiblyoriginatefromhim.Inthenon-idealizedprotocoldescription,itisclearthatthesecondpossibilityistrue.Sneversendsmessagesoftheformwhere.However,messagesreceivedalwayshavethatformat!IfaprogrammermodifiedthemessagesentbySinto,becausehecouldreuseaprocedureusedbyparticipantA,thentheimplicitassumptionthateveryparticipantcanrecognizeitsownmessagesisnolongertrue.Hence,theformalproofisnotvalidanymore.