A Logic of Authentication Michael Burrows hhrtiu Abacli R.oger Needham Abstract Autllcnt.icntioii protocols a.re the basis of seciuity iii many clisti~il~utetl systems, mid it, is therefore esseiitial to eii- sure t,lia.t t,liese prot~ocols function correctly. Uufortuiia.tely, t,licir tlcsign 1~s beeii estremcIy error prone. hbst of the ~xotocols found iii the literature coutniii redundancies or security flaws. A siinple logic 1ia.s aHowed us to describe the beliefs of trustworthy parties involved iii a~utllentica.tioil proto- cols alit1 the evol11tioii of these beliefs as a consequence of conliiiunicat,ioii. We lia.ve been able to esplain a. va.riety of ~lut,lieiit,icatic.)ii protocols foriiially, to discover subtleties a,nd errors in tliein, and to suggest iiiiprovenieiits. Iii this p”l”rr we pleseut, the logic al~rl t,lleil give the results of 011r aimlysis of four l~~~l~lisl~etl 1xotocols, clxxxzii either lie- cilllsc of their pract.ica,l iinpc)rtance or Ixcn.use they serve t,o illust.rate 0111’ lllctllcKl. 1. Iiltroductioil .~lit~li(~iit ic’akil plotocols a.re t,lie hasis of securit,y iii ~iiaiiy In la.ter sections, we sl10w 110~ t,lle logic 11il.s eiia~&~l 11s to tlistrilxikd systems, ant1 it- is therefore esseubial to eiisllre answer these questions for a. iiuinl~er of pullislietl protocols. t11;1 t t.hcse p~t~ocols fuuctbu correctly ([NS]). Unfortu- It is worth iiotirig tlia,t we have iiot tried to auswcr soiiie Ila tcsly, their design has been estremel~~ error prone. Al- otller questions. Siuce we operate at au a.bstra.ct level, we t.l~oq$ ~~ut.lient,icat,ic.)il protocols t,ypically have few mes- tlo ilot, coiisitler errors iiitrotlucetl by concrete iiiilk.iueii- sagrs, t,lle coiulxxi bion of cn.cli message cn.ii be subtle, tatioiis of a. l~rotocol, fmws siicli a.s tlcatlloclis, or CV~IJ and the iilternst.ions I)etwecn the messages ca.u be tom- inapproprin.te 11se of cryptosystcnls (as in [VI<]). Furtllcr- plc,s. I&)rcovcr, protocol designers often iiiisuiitletstnii~l more, while we allow for t,lie possibility of hostile iiit~rliclcrs, t.lle arxilable teclliiiques, col>ying features from esistiilg there is 110 at tempt to deaJ wi tli tile a.utlimitica tioil of r7.i~ lxot.occ.~ls inal)l)lopliately. -4s a result, maiiy of the l)ro- untrustworthy principal, iior to detect weakiiesscs of eil- Permission to copy without fee all or part of this material is granted provided that the copies are not made or distributed for direct commercial advantage, the ACM copyright notice and the title of the publication and its date appear, and notice is given that copying is by permission of the Association for Computing Machinery. To copy otherwise, or to republish, requires a fee and/or specific permission. 0 1989 ACM 089791-338-3/89/0012/0001 $1.50 tocols found ii1 the litera.ture contain retlunda.iicies or se- curity flaws. To a.dcl to tl ie cotifusion, protocols use dif- fereut cryptosystems (e.g., ‘[DES], [R.SA]) a.ud ca.ter for a wide ra.uge of a.pplicakious; it is seldom c1ea.r liow these protocols couipa.re iii tlie guaraiitees they offer. The goa. of a.utllentication ca,u be stated rather sim- ply, thougll informally a.ncl imprec.isely. After autllcxtica- tioii, two yrinciyals (peollle, coiuputers, services) slio~ild lx etititletl to believe that tliey are comiiuuiica.tiiig with ea.cll other, ailcl not witli intruders. Iii t,liis ya.per we defiiie a logic of a.~lt,lieiitica.tion to express such beliefs precisely snd to captlue the reasoning tlmt lexls to them. These a.re examples of questions t1la.t we woi~ltl like t,o lx: able t,o a.iiswer wi tli the help of formal iiie tliods: Does this Ixotocol work? Ca.11 it be ma.& to work? Exactly w1la.t does this protocol achieve? Does this protocol ueed more assunlptiolls tha.11 ailotlier one? Does this protocol do aalythiug unnecessary? Michael Burrows and Martin Aba.di a.re with Digital Equip- ment Corpora.t,ion, Systems Research Center, 130 Lytton Av- enue, Palo Alto, Cabfornia 94301, USA. Roger Needham is with the Universit.y of Cambridge Computer Labora.tory, Corn Ex- change Street, Cambridge CD2 3QG, UK. The three al~thors conipleted part of this work at Digital Equipment Corpora.tion and pa.rt a.t the University of Cambridge.2. The Formalisnl Iii this section. n-e cl(5cril)r t.lir sy1h;i.s a.iitl sriimntics 0f 0111' logic. it S lulVS. illltl tllC t.~~~llSfO~lllil.t.iOll~ Ill~l.t, WC iIl>l)lJ to 1nx~tocols hfore tllcir fomial analysis. Basic llot,ationSimila.rly, for public keys, we poshla te: Logical postulates P believes t%Q P sees {.Y}lc-t P belie& Q said S For slmwl secrets, we postulat~e: I’ believes Q k’, P sees (LY)Lr) P believes Q said S That is, if P believes tllat the secret I” is shared wit.11 Q n.ntl sees (5),.. , tllen P believes that Q olicc mid X. This post&k is sound Ixca.use the rules for sees (,given Ixlowv) guarantee that (S),.. wn.s not just uttered by P l~iinself. l The no7~ce-oeri~cn.tio7t rule expresses he check that it. llleSSil,,$e is ITCCllt, EUlct IlellW tallilt the sender stiIl 1,elieves iii it: 17 believes fresh(X), P believes Q said S P believes Q believes X That is, if P Ideves tht X coultl hve hell ut t,erecl 0lllJ~ IWxllt~ly (ill the ~)rmxmt ) R.ll<l that Q oiicc sid .Y (eitlier in the past or iii the lxesmt), thn P lx- lievcs tlmt Q L&eves S. For the sa.1~ of simplicity, X must lx “clea.rtext ,” that is, it sliould llot include ally sl1l~foL.llllllil. of the fom { 1’) h’. l The juTidi~ti07~~ rule skates that if P lxlieves that Q lms jurisc1ic.tic.m over S tlleu I’ trusts Q on the hut11 of A-: P believes Q controls ;lr, P believes Q believes S P believes ,‘I’ 0 If a. lwincipl sees a. formula. then lie dso sees its coin- 1)tnlruts, 1m)vidwI lie l~iiows the iiccesmry lays: P sees (5, Y) P sees ,Y P sees (S),.. P sees ,I- P believes Q&P , P