Reduction-based Analysis of Real-World Cryptographic Protocols
HGI » UbiCrypt » Projects

Re­duc­tion-ba­sed Ana­ly­sis of Re­al-World Cryp­to­gra­phic Pro­to­cols

1st ad­vi­sor: Schwenk, 2nd ad­vi­sor: Kiltz

In 1993, Bel­la­re and Ro­ga­way pu­blis­hed the first re­duc­tion-ba­sed se­cu­ri­ty model for cryp­to­gra­phic pro­to­cols. Since then, many pa­pers have been pu­blis­hed to ex­tend these ideas, and many new pro­to­cols have been de­si­gned.

La­te­ly, the focus in the re­se­arch com­mu­ni­ty shif­ted from the de­sign of new pro­to­cols (which are not used in prac­tice) to the ana­ly­sis of exis­ting pro­to­cols (e.g. TLS, SSH). Here ad­di­tio­nal pro­blems arise in se­cu­ri­ty pro­ofs:

  • The pro­to­cols can­not be chan­ged, thus in­tro­du­cing new se­cu­ri­ty me­cha­nis­ms to enable a se­cu­ri­ty proof is aout of scope.
  • Im­ple­men­ta­ti­on de­tails have to be con­s­i­de­red, e.g. si­de­chan­nels in ser­ver-si­de TLS im­ple­men­ta­ti­ons.
  • Func­tio­na­li­ty may be di­stri­bu­ted to dif­fe­rent pro­to­cols on dif­fe­rent com­mu­ni­ca­ti­on lay­ers. (The most pro­mi­nent ex­amp­le is pass­word-ba­sed au­then­ti­ca­ti­on on top of TLS, which has noc­t­hin in com­mon with pass­word-ba­sed va­ri­ants of TLS.)

 

At the chair for net­work and data se­cu­ri­ty, we com­bi­ne prac­tical know­ledge about im­ple­men­ta­ti­ons of pro­to­cols, with re­se­arch in for­mal mo­dels.

 

A buil­ding block for the PhD the­sis is our paper on au­then­ti­ca­ted se­cu­re TLS chan­nels which is avail­able on ePrint (...), and will most pro­bab­ly be pre­sen­ted at CRYP­TO 2012. Pos­si­ble PhD to­pics are:

  • Com­bi­ning TLS with au­then­ti­ca­ti­on pro­to­cols on top of TLS. Ty­pi­cal­ly TLS only pro­vi­des ser­ver au­then­ti­ca­ti­on, and cli­ent au­then­ti­ca­ti­on is added by sup­p­ly­ing a pass­word through the TLS chan­nel. Stron­ger cli­ent au­then­ti­ca­ti­on me­cha­nis­ms are e.g. smart card based au­then­ti­ca­ti­on pro­to­cols pro­vi­ded by Eu­ropean ci­ti­zen cards, or Mas­ter­Card CAP. The the­sis should de­vi­se me­thods how to com­bi­ne TLS with ar­bi­tra­ry au­then­ti­ca­ti­on prot­cols to form a se­cu­re, mu­tual­ly au­then­ti­ca­ted key es­ta­blish­ment (AKE) pro­to­col. This ex­tends our paper at ASI­A­CRYPT 2010.
  • For­mal se­cu­ri­ty pro­ofs for TLS-ba­sed Sin­gle-Sign-On (SSO) pro­to­cols. Many SSO pro­to­cols used today (Open­ID, SAML) use a com­mu­ni­ca­ti­on struc­tu­re si­mi­lar to Ker­be­ros, but apply TLS in­s­tead of Ker­be­ros en­cryp­ti­on. First for­mal mo­dels for SSO have been de­ve­lo­ped, but need re­fi­ne­ment and ad­ap­ti­on to the TLS case.
Prof. Jörg Schwenk

Prof. Jörg Schwenk