I n d on e s ian   Jou r n al   o f   E lec t r ica l   E n gin e e r in a n d   Com p u t e r   S c ience   Vo l .   24 ,   N o .   1 Oc to b e r   2021 ,   pp .   621 ~ 636   I S S N:  2502 - 4752,   DO I 10 . 11591/i j e e c s . v 24 .i 1 . pp621 - 636             621       Jou r n al  h o m e page ht tp: // ij e e c s . iaes c or e . c om   F or m al  se c u r ity  an al y si s of  l ig h t w e ig h t  au t h e n t ic at e d  k e y   agr e e m e n t  p r ot oc ol  f o r   IoT   in  c lo u d  c o m p u t in g       Ahm e d   H.   Al y 1 At e f   Gh al was h 2 M on a   M .   Nas r 3 ,   Ahm e d   A.   Abd   E l - Haf e z 4   1, 2, 3 Fac u l t y   o Co m p u t e S ci e n ce   a n d   A rt i f i c i a l   I n t e l l i g e n ce ,   H el w a n   U n i v e rs i t y ,   Ca i ro ,   E g y p t   4 N at i o n a l   T e l eco m ,   R eg u l at o r y   A u t h o ri t y   (N T RA ),   Cai r o ,   E g y p t       Ar t ic l e   I n f o     AB S T RA CT     A r ti c le  h is tor y :   R e c e i ve Ju n   24 2021   R e vi s e A ug   29 2021   A c c e pt e A ug   30 2021       T h e   i n t e rn e t   o f   t h i n g s   (I o T )   an d   c l o u d   c o m p u t i n g   are   e v o l v i n g   t e c h n o l o g i e s   i n   t h e   i n fo rm a t i o n   t e c h n o l o g y   fi e l d .   Me rg i n g   t h e   p e rv a s i v I o T   t e c h n o l o g y   w i t h   c l o u d   c o m p u t i n g   i s   an   i n n o v a t i v e   s o l u t i o n   fo r   b e t t e r   an al y t i c s   an d   d e c i s i o n - m ak i n g .   D e p l o y e d   I o T   d e v i c e s   o f fl o ad   d i f fe re n t   t y p e s   o f   d a t a   t o   t h e   c l o u d ,   w h i l e   c l o u d   c o m p u t i n g   c o n v e rg e s   t h e   i n f ra s t ru c t u re ,   l i n k s   u p   t h e   s e rv e r s ,   a n al y ze s   i n fo rm a t i o n   o b t ai n e d   f ro m   t h e   I o T   d e v i c e s ,   re i n fo rc e s   p ro c e s s i n g   p o w e r,   an d   o f fe r s   h u g e   s t o r ag e   c a p ac i t y .   H o w e v e r,   t h i s   m e rg i n g   i s   p ro n e   t o   v ari o u s   c y b e r   t h re a t s   t h a t   af fe c t   t h e   I o T - Cl o u d   e n v i ro n m e n t .   Mu t u al   a u t h e n t i c a t i o n   i s   c o n s i d e re d   a s   t h e   fo re f ro n t   m ec h an i s m   fo c y b e r - a t t ac k s   a s   t h e   I o T - Cl o u d   p a r t i c i p an t s   h av e   t o   e n s u re   t h e   au t h e n t i c i t y   o f   e ac h   o t h e r   an d   g e n e ra t e   a   s e s s i o n   k e y   fo r   s e c u ri n g   t h e   e x c h an g e d   t ra ff i c .   W h i l e   d e s i g n i n g   t h e s e   m e c h an i s m s ,   t h e   c o n s t r ai n e d   n a t u re   o f   t h e   I o T   d e v i c e s   m u s t   b e   t ak e n   i n t o   c o n s i d e ra t i o n .   W e   p ro p o s e d   a   n o v e l   l i g h t w e i g h t   p ro t o c o l   ( L i g h t - A H A K A )   fo a u t h e n t i c a t i n g   I o T - Cl o u d   e l e m e n t s   an d   e s t a b l i s h i n g   k e y   ag re e m e n t   fo e n c ry p t i n g   t h e   e x c h an g e d   s e n s i t i v e   d a t a   w a s   p r o p o s e d .   I n   t h i s   p a p e r,   t h e   fo rm al   v e ri fi c a t i o n   o f   (L i g h t - A H A K A w a s   p re s e n t e d   t o   p r o v e   an d   v e ri fy   t h c o r re c t n e s s   o f   o u r   p ro p o s e d   p ro t o c o l   t o   e n s u re   t h a t   t h e   p r o t o c o l   i s   f re e   fro m   d e s i g n   fl aw s   b e fo re   t h e   d e p l o y m e n t   p h a s e .   T h e   v e ri fi c a t i o n   i s   p e r fo rm e d   b a s e o n   t w o   d i ffe re n t   a p p ro ac h e s ,   t h e   s t r an d   s p ac e   m o d e l   an d   t h e   au t o m a t e d   v al i d a t i o n   o i n t e rn e t   s e c u ri t y   p ro t o c o l s   an d   a p p l i c a t i o n s   (A V I SPA t o o l .   K e y w o r ds :   A VI S P A   F o r m a l   v e r i f i c a t i o n   I n t e r n e t   s e c ur i t y   pr oto c o l   I n t e r n e t   o f   t hi n gs   L i g h t we i g h t   a u t h e n t i c a t i o n   S tr a n s pa c e   m o de l   T his   is   an  ope ac c e s s   ar ti c le  unde r   the  CC  B Y - SA   l ice ns e .     C or r e s pon din A u th or :   Ahm e Ha s s a n   Aly   F a c u l t y   o f   C o m put e r   S c i e n c e   a n A r t i f i c i a l   I n t e l li g e n c e   He l wa n   U ni ve r s i t y ,   C a i r o ,   E gy pt   E m a i l a hm e d71. a ly @g m a il . c o m       Nom e n c l at u r e s   C   B undl e  i s tr a nd s pa c e  m o d e l   E  ( . )   S y mm e t r i c   li ght w e ig ht  e n c r y pt i o n   F   D o bb e r ta in   f un c ti o n   ID I o T   I oT   id e nt it y   ID S   A ut he nt i c a ti o s e r ve r   id e nt it y   ID U   U s e r   id e n ti t y   H  ( .   )   li ght w e i ght   c o ll is i o n - f r e e   o n e - w a y  ha s f unc ti o n   PW I o T , P W U   T h e  pa s s w o r of  t he   I oT  d e v i c e us e r   r e s p e c ti v e l y   P SK I o T   T h e  p r e - s ha r e d k e y  be twe e n t h e  us e r  a nd t he  I oT  d e v ic e   P SK U   T h e  p r e - s ha r e d k e y  be twe e n t h e  us e r  a nd t he  s e r ve r   R S , R U , R I o T   R a ndo m num be r s  of   s e r ve r , us e r , I oT  de vi c e  r e s p e c ti ve l y   T S , T U , T I o T   T im e - s ta mps   of   se r ve r ,   us e r , I oT  d e v i c e  r e s pe c ti ve l y   Δ  T   T im e   r a nge  a ll o w e f or  de la y     i   I nde x  s e le c t e f r o m R U     e x i=  d e c im a v a lu e   of   i th   by t e   of   R U   j   I nde x  s e le c t e f r o m R I o T     e x j=  d e c im a v a lu e   of   j th   by t e   of   R I o T   Evaluation Warning : The document was created with Spire.PDF for Python.
                                I S S N :   2502 - 4752   I n do n e s i a n   J   E l e c   E n &   C o m S c i ,   Vo l .   24 ,   N o .   1 Oc to b e r   2021 621   -   636   622   ||   C o nc a t e na ti o n     X o R  O pe r a ti o n     Abb r e viat ion s   H M A C   H a s me s s a ge  a ut he nt ic a ti o n   c o d e   L F S R   L in e a r   f e e d -   ba c k s hi f r e gi s t e r   N F S R   N o n - li n e a r   f e e d - ba c k s hi f r e gi s t e r   SK   S e s s io k e y       1.   I NT RODU C T I ON     T h e   i n t e r n e o f   t h i n gs   ( I o T )   h a s   b e c o m e   a n   e m e r g i n t e c hn o l o g y   i n   r e c e n t   y e a r s ,   t h e   n u m be r   o f   c o n n e c t e de vi c e s   i s   a n t i c i pa t e to   r e a c h   75  bil li o n   de vi c e s   by   t h e   e n d   o f   2025   [1 ] .   I o T   t e c hn o l o gy   c o ve r s   d i f f e r e n t   a pp l i c a t i o ns ,   s m a r t   c i t i e s ,   he a l t h c a r e ,   a nd  s m a r t   t r a f f i c .   B a s e o n   t h e   a pp li c a t i o n   u s e d,   I oT   de vi c e s   s e n a   p l e t h o r a   o f   da t a ,   r e a l - t i m e   vi d e o s ,   a n ph o to s   to   t h e   s e r v e r s .   T h e   t r a di t i o n a l   p l a t f o r m s   s t or a ge   s y s t e m s   a n d   c o m put i n g   p l a t f o r m s   c a n o t   e f f e c t i v e ly   h a n d le  t h e   m a s s i ve   da t a   ge ne r a t e by   de p l o y e I o T   de vi c e s .   A s   a   r e s u l t ,   i m pe r a t i v e   a t t e n t i o n   i s   r e qu i r e d   to   f i nd   s u it a bl e   m e c h a ni s m s   t h a t   r e l y   o l a r ge   r e s o ur c e   po o l s   s uc h   a s   c l o ud  c o m put i n t o   h a n d l e   t h e   o f f l o a d e da t a .   I n   m a ny   u s e   c a s e s ,   a ut h o r i z e u s e r s   ne e t o   a c c e s s   r e a l - t i m e   da t a   di r e c t l y   f r o m   t h e   I o T   de vi c e s   f o r   i ns t a n t   a n c r i t i c a l   de c i s i o n s   ( i . e . ,   He a l t h c a r e F i r e   i g ni t i o n ,   a n d   T r a f f i c   C o n ge s t i o n )   [ 3] .   I n   t hi s   us e   c a s e ,   c l o ud  s e r ve r s   a r e   r e s po n s i b l e   f o r   t h e   m ut ua l   a ut h e n t i c a t i o o f   t h e   us e r   a n d   t h e   i n t e n d e I o T   de vi c e   b e f o r e   gr a n t i n a ut h o r i z e us e r s   t he   r i g h t   to   a c c e s s   t h e   r e a l - t i m e   da t a .   Due   to   t h e   c o n s t r a i n e d   n a t ur e   o f   I o T   de vi c e s ,   t h e s e   de vi c e s   a r e   s u s c e pt i bl e   t o   di f f e r e n t   v u l ne r a bil i t i e s   a n d   s e c ur i t y   b r e a c h e s   [4 ] [ 5] .   M e a n w hil e ,   h a c k e r s   a r e   de v e lo pi n ne m e t h o ds   to   e x p l o i t   p oo r   s e c ur i t y   m e c h a ni s m s   im p l e m e n t e i I o T   de vi c e s .   r o b us t   a ut h e n t i c a t i o n   pr o to c o l   i s   s u b s t a n t i a l   t o   pr e v e n t   una ut h o r i z e a c c e s s ,   pr ot e c s e n s i t i ve   da t a ,   a n m a i n t a i n   u s e r   pr i v a c y .     I n   t hi s   c o n t e x t ,   we   pr o p o s e a   n e li g h t we i g h t   a ut h e n t i c a t i o a n ke y   a gr e e m e n t   pr oto c o l   ( L i g h t - A H AK A )   [ 6] .   Our   pr o p o s e pr oto c o l   i s   b a s e o n   t h e   c h a ll e n ge - r e s po n s e   m e c h a ni s m   t o   a c hi e ve   m ut ua l   a ut h e n t i c a t i o n ,   t a k i n i n t o   c o n s i de r a t i o n   t h e   c o ns t r a i n e n a t ur e   o f   I o T   de vi c e s .   T h e   c r y pt o gr a phi c   f un c t i o n s   us e a r e   s ymm e t r i c - ke y   c r y pt o g r a phy ,   h a s h   f u n c t i o n ,   a n h a s m e s s a ge   a ut h e n t i c a t i o c o de   ( HM A C )   [ 7] E v e r y   s e s s i o n ,   t h e   pr oto c o l   ge n e r a t e s   a   n e ke y   f o r   e n c r y pt i n t h e   t r a f f i c .   A   d i f f e r e n t   s e s s i o n   ke y   f o r   e a c h   s e s s i o a ll o ws   a   l im i t e n u m be r   o f   m e s s a ge s   t o   b e   e nc r y pt e w i t o n e   s e s s i o n   k e y ,   m a k i ng  i t   v e r y   d i f f i c u l t   f o r   a tt a c ke r s   to   f i nd  t h e   ge n e r a t e s e s s i o n   ke y s .   M o r e o v e r ,   i f   t h e   a t t a c ke r   s uc c e e ds   i f i nd i ng  t h e   s e s s i o n   k e y   by   a ny   m e a n s ,   t hi s   k e y   i s   r e l a t e to   a   s pe c i f i c   s e s s i o n   a n ha s   n o t hi n t o   d o   wi t h   t he   upc o m i ng  s e s s io n s .   F o r   e nh a nc i n g   t h e   r e s i li e nc y   o f   t h e   I o T - C l o ud  n e t wo r k ,   t h e   ( L i g h t - A H AK A )   upd a t e s   t h e   pr e - s h a r e ke y s ,   pa s s wo r ds ,   a n d   pa r t i c i p a n t   i de n t i t i e s .   All   t h e   pr e vio us   pa r a m e t e r s   a r e   v a li o nly   f o r   o n e   s e s s i o n ,   m a k i n t h e   b r e a kt h r o ugh   to  o ur   p r oto c o l   v e r y   d i f f i c u l t .     T h e   d e s i gn   a n d   f or m a l   a n a l y s i s   of   s e c u r i t y   p r o t oc ol s   i s   a   c h a l l e n gi n g   p r ob l e m .   S e r i ou s   s e c u r i t y   f l a w s   i p r o t oc ol s   w e r e   di s c ov e r e d   i n   s e v e r a l   c a s e s ,   m a n y   y e a r s   a f te r   th e y   w e r e   f i r s p u b l i s h e d   or   d e p l o y e d .   A tt a c k s   on   th e s e   p r o t oc ol s   g e n e r a l l y   a v o i d   ta r g e ti n g   th e   m a th e m a ti c a l   c r y p tog r a p h i c   p r i m i t i v e s ,   b u r a th e r   f oc u s   on   e x pl o i t i n th e   p r o t oc ol ' s   d e s i gn   f l a w s .   F or m a l   v e r i f i c a t i on   pr ov i d e s   r i g or ou s   a n d   th or ou g h   m e th od s   of   e v a l ua ti n g   th e   c or r e c tn e s s   o f   th e   s e c u r i t y   p r o t oc ol s   to  d i s c ov e r   s ub tl e   f l a w s .   R e s e a r c h e r s   h a v e   de v e l op e d   n um e r ou s   a p p r oa c h e s   a n d   f or m a l   m e th od s   th a c ou l d   b e   u t i l i z e d   f or   th e   v e r i f i c a t i on   of   s e c u r i t y   p r o t oc ol s .   I n   th i s   c on te x t,   w e   p r e s e n th e   f or m a l   v e r i f i c a t i on   of   ( L i gh t - A HA K A )   to  v e r i f y   th e   c or r e c tn e s s   of   ou r   p r op os e d   p r o t oc ol .   T h e   f or m a l   v e r i f i c a t i on   i s   c on d u c te d   b a s e d   on   tw o   d i f f e r e n a p p r oa c h e s ,   th e   s tr a n d   s p a c e   m od e l   a n d   A V I S P A .   T h e   upc o m i ng   s e c t i o ns   o f   t h e   pa pe r   a r e   s t r uc t ur e i t h e   f o l l o w i ng  wa y .   S e c t i o n   2   o f   t h e   pa p e r   r e vi e ws   t h e   ( L i g h t - A H AK A )   pr oto c o l .   T h e   f o r m a l   a n a ly s i s   o f   ( L i g h t - A H AK A )   i s   i n t r o duc e t h or oughly   in  s e c t i o n   3   b a s e o n   t w o   di f f e r e n t   a ppr o a c h e s .   S e c t i o n   4 ,   di s c u s s e s   t h e   r e s u l t s   o f   t h e   f o r m a l   a na l y s is   o f   t h e   ( L i g h t - A H AK A ) .   F i na l ly ,   s e c t i o n   5   c o n c l ud e s   t h e   pa pe r .       2.   RE VI E OF   ( L I GH T - AHAK A)   T h e   ( L i gh t - A HA K A )   i s   a   l i gh tw e i gh a u th e n t i c a t i on   p r o t oc ol   b a s e d   on   l i gh tw e i gh s y m m e tr i c   ke y   c r y p tog r a p h y ,   l i gh tw e i gh h a s h   f un c t i on ,   l i gh tw e i gh h a s h - b a s e d   m e s s a g e   a u th e n t i c a t i on   c od e   ( H M A C )   [ 8 ] a n e x c l us i v e - or   op e r a ti on .   A   r e v i e w   of   th e   ( L i gh t - A HA K A )   wi l l   b e   i l l u s tr a te d   i n   th e   u p c om i n g   s te p s .   T h e   I oT - C l o ud  n e t wo r k   wi ll   b e   i ni t i a li z e a c c o r d i n to   t h e   f o l l o w in g:     T h e   n e t wo r a dm i ni s t r a t or   ( NA )   a s s i g ns   a   uni que   i de n t i t y   ( ID Ui ) ,   pa s s wo r d   ( PW Ui ) ,   a n a   pr e - s h a r e d   ke y   ( P SK Ui )   f o r   e a c h   us e r   ( U i )   s to r e d   s a f e ly   i t h e   c l i e nt  a ppl i c a t i o n .     T h e   ( NA )   l o a ds   ( ID Io T i ) ,   ( PW Io T i ) ,   a n pr e - s h a r e d   ke y   ( P SK Io T i )   i n   a   t a m pe r - pr oo f   m e m o r y   f o r   e a c I oT   de vi c e .     T h e   ( L i g h t - A H AK A )   pr o c e dur e   F i gur e   wi ll   b e   r e vi e we i n   t h e   f o l l o w i ng  s t e ps :   Evaluation Warning : The document was created with Spire.PDF for Python.
I n do n e s i a n   J   E l e c   E n &   C o m S c i     I S S N:  2502 - 4752       F or mal  s e c u r it y   analys is   of   li ghtw e ight   authentica ted  k e y   agr e e me nt  pr o tocol  f or   I o T   ( A hme H.   A ly )   623       F i gur e   1 .   L i g h t - A H AK A   pr o c e dur e       1)   T h e   us e r   s e n d s   a n   a c c e s s   r e que s t   to   t h e   authenticat ion  s e r v e r :   o   ( I D | | ( P W U )   | |T U1 )   | |   ( HM A C U1 ) .   2)   T h e   authentication  s e r v e r   w i ll   do   t h e   f o l l o w i ng:     C he c ks   i f   ( T U1   <   Δ   T ) ,   c a l c u l a t e s   ( HM A C U1 ),   a n c o m pa r e s   i t   w i t h   t h e   r e c e i v e o n e .     S e a r c h e s   i n   t h e   da t a b a s e   f o r   ( ID U )   a n t h e   h a s h   o f   th e   pa s s wo r d.     Ge n e r a t e s   a   r a n do m   n u m be r   ( R S1 ).     S e n ds   t h e   f o l l o w i ng  m e s s a ge   e n c r y pt e w i t h   t h e   pr e - s h a r e ke y   ( P SK U )   a s   a   c h a ll e n ge   f o r   t h e   us e r :   o   E P S K U   ( ID S   | | R S1 )   | | T S1   | |   ( HM A C S1 ) .   3)   T h e   us e r   r e c e i ve s   t h e   m e s s a ge   a n w i ll   do   t h e   f o l lo wi n g:     C he c ks   i f   ( T S1   <   Δ   T )   a n v e r i f i e s   ( HM A C S1 ).     De c r y pt s   t h e   m e s s a ge   a n c he c ks   ID S   ( r e c e i v e d)   = ID S   ( s to r e d) .     E x t r a c t s   ( R S1 ).     F r o m   t h e   pr e vi o u s   s t e ps ,   t h e   u s e r   a ut h e n t i c a t e s   t h e   s e r v e r .     T h e   u s e r   wi l l   ge n e r a te   a   r a n d o m   n um b e r   ( R U )   a n d   s e n d   th e   f o l l owi n g   m e s s a g e   a s   a   r e s p on s e   t th e   s e r v e r :   o   E P S K U   ( R S1 | | R U | | I D I o T )   | | T U2   | |   ( HM A C U2 ) .   4)   T h e   authentication  s e r v e r   r e c e i v e s   t h e   m e s s a ge   a nd  w i l l   do   t h e   f o l l o w i ng:     C he c ks   i f   ( T U2   <   Δ   T )   a n v e r if i e s   ( HM A C U2 ).     De c r y pt s   t h e   m e s s a ge   a n c he c ks   i f   R S 1   ( s e n t )   =   R S 1   ( r e c e i v e d) .     F r o m   t h e   pr e vi o u s   s t e p,   t h e   s e r v e r   a ut h e n t i c a t e s   t h e   us e r .     S tor e s   R U   a n s e a r c he s   f o r   t h e   ( ID I o T ) .       T h e   s e r v e r   s e n d s   t h e   us e r   a c k n o w l e dg m e n t   m e s s a ge   a n t h e   HM A C   o f   t h e   a c k n o w l e dg m e n t   us i ng   (R U )   a s   a   ke y   f o r   t h e   HM A C   a s   a   r e s po n s e   f o r   t h e   us e r :   o   A C K   | |   H M A C S2     T h e   us e r   r e c e i ve s   t h e   m e s s a ge s   a n c a l c u l a t e s   t h e   HM A C   us i n (R U )   a s   a   ke y   a n c o m pa r e s   t h e   r e s u l t   w i t h   t h e   r e c e i v e o n e .   Evaluation Warning : The document was created with Spire.PDF for Python.
                                I S S N :   2502 - 4752   I n do n e s i a n   J   E l e c   E n &   C o m S c i ,   Vo l .   24 ,   N o .   1 Oc to b e r   2021 621   -   636   624   5)   T h e   s e r v e r   w il l   s t a r t   t h e   m ut ua l   a ut h e n t i c a t i o n   w i t h   t h e   i n t e n de I oT   de vi c e :     T h e   s e r v e r   g e n e r a te s   a   r a n d om   n um b e r   (R S2 )   a n d   s e n d s   a   c h a l l e n g e   m e s s a g e   t th e   i n ten d e d   I o T   d e v i c e :   o   E P S K Io T   ( I D S   | | I D I o T   | | R S2   )   | | T S1 | | HM A C S3     T h e   I oT   r e c e i ve s   t h e   m e s s a ge ,   c h e c ks   if   ( T S1   <   Δ   T ) ,   a n v e r i f i e s   ( HM A C S3 ).     De c r y pt s   t h e   m e s s a ge   a n c he c ks   i f   ID S   ( r e c e i v e d)   =   ID S   ( S to r e d) .     F r o m   t h e   pr e vi o u s   s t e ps ,   t h e   I o T   de vi c e   a ut h e n t i c a t e s   t h e   s e r v e r .     T h e   I oT   de vi c e   c a l c u l a t e s   t h e   r e s po n s e   m e s s a ge   f o r   t h e   c h a ll e n ge   o f   t h e   s e r v e r :   o   HM A C Io T 1   (T I o T 1   R S2   PW Io T ) .     C a l c u l a t e s   t h e   n o n c e   R Io T   a s   f o l l o w s :   o   R Io T   =   Has ( R S2     ID S     ID I o T )   6)   T h e   I oT   de vi c e   s e n ds   t h e   f o l l o w i ng  r e s po n s e   m e s s a ge   to  t h e   s e r v e r :   o     ( HM A C Io T 1   | |   T Io T 1   ) .     T h e   s e r v e r   r e c e i ve s   t h e   m e s s a ge ,   c h e c ks   i f   ( T Io T 1   <   Δ   T ) ,   a n v e r i f i e s   ( HM A C Io T1 ).     C a l c u l a t e s   R I o T   a s   f o l l o ws :   o   R Io T   =   Has ( R S2     ID S     ID I o T )     F r o m   t h e   pr e vi o u s   s t e ps ,   t h e   s e r v e r   a ut h e n t i c a t e s   th e   I oT   de vi c e .   7)   T h e   s e r v e r   s e n ds   t h e   I oT   de vi c e   a c k n o w l e dg m e n t   m e s s a ge   a n t h e   HM A C   o f   t h e   a c kn o w l e dg m e n t   us i ng  (R Io T )   a s   a   ke y   f o r   t h e   HM A C   a s   a   r e s po n s e   f o r   t h e   I oT   de vi c e :   o   A C K   | |   H M A C S4   8)   Af t e r   t h e   authentication  s e r v e r   h a s   f i n i s he a ut h e n t i c a t i n t h e   u s e r   a n t h e   I oT   de vi c e ,   t h e   s e r v e r   s e n ds   t h e   us e r   a n t h e   I oT   de vi c e   t e m po r a r y   pa r a m e t e r s   to   e s t a bl i s h   a   t e m po r a r y   ke y .   T h e   us e r   w il l   m a ke   us e   o f   t hi s   ke y   to   a c c e s s   t h e   I oT   de vi c e .   I n   t h e   i n i t i a l   s t a ge s   o f   de s i g ni ng  ( L i g h t - A H AK A ) ,   i t   wa s   de s i g n e to   m a k e   t h e   a ut h e n t i c a t i o n   s e r v e r   s e n K Io T   to   th e   us e r ,   b ut   a f t e r   s t udy i ng  t he   S t r a n S pa c e   M o de l   pr e s e n t e i n   s e c t i o n   4. 1 ,   we   f o un t h a t   to   a c hi e v e   m a xim u m   s e c ur i t y ,   i t   i s   n o r e c o m m e n de to   tr a n s mi t   pr e - s h a r e ke y s .     9)   T h e   s e r v e r   s e n d s   to   t h e   us e r   t h e   f o l l o w i ng  da t a :     R T e m p 1   =   ( R I o T     ID S )       I oT   de vi c e   pa s s wo r ( PW Io T ) ,   a n R T e m p 1   o   E P S K U   (R T e m p 1   | |   P W Io T )   | | T S1 | | HM A C S5     T h e   us e r   r e c e i ve s   t h e   m e s s a ge ,   c h e c ks   i f   ( T S1   <   Δ   T ) ,   a n v e r if y   HM A C S5 .     C a l c u l a t e s   R I o T =   R T e m p 1     ID S .     C a l c u l a t e s   K T e m p 1   =   R I o T     R U .   10)   T h e   s e r v e r   s e n d s   to   t h e   I oT   de vi c e   t h e   f o l l o w i ng  d a t a :     R T e m p 2 =R U     ID S .     R T e m p 2   a n us e r   I e n c r y pt e w i t h   I oT   pr e - s h a r e ke y   ( P SK Io T )   a s   f o l l o w s :   o     E P S K Io T   (R T e m p 2   | |   I D U )   | | T S2 | | HM A C S6     T h e   I oT   de vi c e   r e c e i v e s   t h e   m e s s a ge ,   c h e c ks   i f   ( T S2   <   Δ   T ) ,   a n v e r i f i e s   HM A C S6 .     C a l c u l a t e s   R U =R T e m p 2     ID S     S tor e s   ( R U )   a n ( ID U ).     C a l c u l a t e s   K T e m p 1   =   R I o T     R U .   11)   T h e   us e r   s e n d s   a n   a c c e s s   r e que s t   to   t h e   I oT   de vi c e   a s   f o l l o ws :   o   E K Te m p 1   ( P W Io T )   | | I D | | T U1 | |   M A C U3     T h e   I oT   de vi c e   r e c e i v e s   t h e   m e s s a ge ,   c h e c ks   i f   ( T U1   <   Δ   T ) ,   a n Ve r i f i e s   HM A C U3 .     C he c ks   i f   ID U   ( r e c e i v e d)   =   ID U   ( s to r e d ) .     De c r y pt s   t h e   m e s s a ge   us i ng  ( K T e m p 1 ).     E x t r a c t s   t h e   pa s s wo r a n c h e c ks   t h a t   i t   i s   a   v a li pa s s wo r d.     S e n ds   a c k n o w l e dg m e n t   to  t h e   us e r .   12)   T h e   ( L i g h t - A H AK A )   pa r t i c i pa n t s   ( s e r v e r -   I oT   d e vi c e   - u s e r )   s t o r e   t w o   s hi f t   r e g i s t e r s T h e   f i r s t   s hif r e g i s t e r   i s   a   l i ne a r   f e e d b a c s hif t   r e g i s t e r   ( L1 )   c onn e c t e to   a   pr i mi t i ve   po l y n o mi a l   t pr o duc e   a   w e l l - b a l a n c e s e que n c e   o f   s t r e a m s .   T h e   s e c o n d   i s   a   no n - l i ne a r   f e e d b a c k   s hif t   r e g i s t e r   ( L2 )   c o n n e c t e t o   a   n o n - l i ne a r   B o o l e a n   f u n c t i o n   t i n c r e a s e   t h e   n o n - l in e a r i t y   o f   t h e   o ut pu s e que n c e .   T h e   o ut pu o f   t h e   two  r e g i s t e r s   i s   c o nn e c t e to  a   v e c to r i a l   d o bbe r t a i n   f un c t i o n   ( F )   a s   a   c o m b i ne r   f u n c t i o n   [ 9] ,   whi c h   i s   a a l m o s t   pe r f e c t   n o n - l i ne a r   f u n c t i o n   c ha r a c t e r i z e by  hi g h   r e s i s t a n c e   to   l i ne a r   a n d i f f e r e n t i a l   a tt a c ks .     13)   T h e   I oT   de vi c e   a n t h e   us e r   w i ll   do   t h e   f o l l o w i ng  f o r   ge n e r a t i n t h e   s e s s i o n   ke y       IV 1 = Ha s h   ( R Io T ) .         IV 2 = Ha s h   ( R U ) .     Evaluation Warning : The document was created with Spire.PDF for Python.
I n do n e s i a n   J   E l e c   E n &   C o m S c i     I S S N:  2502 - 4752       F or mal  s e c u r it y   analys is   of   li ghtw e ight   authentica ted  k e y   agr e e me nt  pr o tocol  f or   I o T   ( A hme H.   A ly )   625     I V a n I V w i ll   be   us e to   f i ll   ( L1 )   a n ( L2 ) ,   r e s pe c t i v e ly .     T h e   s e s s i o n   ke y   ( SK )   w il l   b e   c a l c u l a t e us i ng  t h e   ke y   a gr e e m e n t   a n pa r a m e t e r s   upda t e   m o du l e   a s   s h o w n   i n   F i gur e   2 .   o     SK =   F   [ Sh i f ( L 1( i) ) ,   Shi f t   ( L 2( j) ) ]       As   a n   e x a m p l e ,   l e t 's   a s s u m e   t h a t   i s   pr e de t e r m i ne a s   t h e   20 th   by t e   o f   RU ,   a n t h e   d e c im a l   v a l ue   o f   i s   ( 126) ,   s t h e   L wi ll   b e   s hif t e ( 126)   s hi f t s .     14)   T h e   pa s s wo r ds   a n t h e   i de n t i t i e s   o f   ( Us e r -   I oT )   w i ll   be   upda t e e v e r y   s e s s i o n   b a s e upo n   t h e   m e t h o d   il l us t r a t e d   i n   s t e ( 13) .   M or e   de t a i l s   a b o ut   ( L i g h t - A H AK A )   a r e   pr o vi de i n   [ 1] .           F i gur e   1 .   K e y   a gr e e m e n t   a n pa r a m e t e r s   upda t e   m o dul e       3.   F ORM AL   S E CU RI T AN AL YS I S   OF   ( L I GH T - AHAK A)   I n   t hi s   s e c t i o n ,   we   r e vi e t h e   s e c ur i t y   a na l y s i s   o f   ( L i g h t - A H AK A ) ,   w hi c h   i s   s u mm a r i z e i T a bl e   1 W e   a l s o   pr e s e n t   t h e   f o r m a l   a na l y s i s   o f   t h e   pr otoco l   b a s e o n   t wo   di f f e r e n t   a ppr o a c h e s ,   t h e   S t r a n S pa c e   M o de l   a n A VI S P A .   T a bl e   2   pr e s e n t s   t h e   a dv e r s a r y   c a pa bil i t i e s   w hi c h   a r e   b a s e o n   t h e   Do l e v - Ya o     m o de l   [ 10]   a n t h e   C a n e t t i - K r a wc z y t h r e a t   m o de l   [ 11] .       T a b le   1 .   S e c ur i t y   a n a ly s i s   o f   l i g h t - A H AK A   S e c ur it y  a tt a c k   C o unt e r m e a s ur e s   I mpe r s o na ti o n a tt a c ks   U pda ti ng t he   f o ll o w in g pa r a m e t e r s  e ve r y  s e s s io n:   1 -   ( U s e r - I oT  d e v i c e )  pa s s w o r ds .   2 -   ( U s e r - I oT )  I d e nt it i e s .   3 -   P r e - s ha r e K e y s .   4 -   R a ndo m Numb e r s   P r i v il e ge in s id e r  a tt a c ks   1 -   S t o r in g t h e  pa s s w o r H a s he d   2 -   S e ndi ng  th e  ha s of  t h e  pa s s w o r d   M a n i n t he  mi ddl e  a tt a c ks   ( M I T M )   1 -   E n c r y pt in g a ll   c ha ll e nge s  a nd r e s po ns e s   2 -   F r e s h R a ndo m Numb e r s   3 -   U s in g T i me s ta mps   D O S  A tt a c ks   U pda ti ng t he   f o ll o w in g pa r a m e t e r s  e ve r y  s e s s io n :   1 -   ( U s e r - I oT  d e v i c e )  pa s s w o r ds   2 -   ( U s e r - I oT )  I d e nt it i e s   3 -   P r e - s ha r e K e y s   R e pl a y  A tt a c ks   1 -   F r e s h R a ndo m Numb e r s   2 -   U s in g T i me s ta mps   O f f li n e  gue s s in g a tt a c ks   1 -   S e ndi ng  th e  pa s s w o r d ha s he d   2 -   U pda ti ng t he  pa s s w o r e ve r y  s e s s i o n   D a ta  i nt e gr it y  a tt a c ks   1 -   U s in g H M A C  f un c ti o n   2 -   U s in g f r e s h r a nd o m num b e r s   P a r a ll e s e s s i o n a tt a c k   1 -   U s in g t he  ha s h f un c ti o n   2 -   U s in g t he   H M A C  f un c ti o n   S e s s io n k e y  di s c l o s e r  a tt a c k   U s in g t he   f o ll o w in g:   1 -   F r e s h R a ndo m Numb e r s  ( R U   -   R I oT )   2 -   C o ll is i o n - f r e e  ha s f un c ti o n   3 -   T h e  P r im i ti v e   P o l y n o mi a l   4 -   T h e  N o n li ne a r   B oo l e a n F un c ti o n   5 -   T h e  s hi f ti ng  v a lu e s   of  t h e  t w o   L S F R   U s e r  a no n y m it y  a nd  unt r a c e a bi li t y   U pda ti ng t he   f o ll o w in e ve r y  s e s s i o n:   1 -   ( U s e r -   I oT )  I d e nt it i e s   2 -   F r e s h R a ndo m Numb e r s       T a bl e   2 .   A dve r s a r y   c a p a bi li t i e s   C a pa bi li ti e s   D e f in it i o n   C a pa bi li t y  1    T h e  a d ve r s a r y  c a n i nt e r c e pt , r e pl a y  a nd m o di f y  a n y  m e s s a ge  e xc ha nge d i n t h e  n e tw o r k .   C a pa bi li t y  2   T h e  a d ve r s a r y  i s  a  l e gi ti ma t e  pa r ti c ip a nt  i n t h e  n e tw o r k, s /h e  c a n i ni ti a te  a  s e s s io n w i th  a n y   o th e r  pa r ti c ip a nt .   C a pa bi li t y  3   T h e  a d ve r s a r y  c a n s e nd /r e c e i ve  m e s s a ge s .   C a pa bi li t y  4   T h e  a d ve r s a r y  c a n p e r f or m a  ma n i n t h e  mi ddl e , i mp e r s o na ti o n,  r e pl a y  a tt a c ks   o n a n y  r un  of   th e  p r o t o c ol .   C a pa bi li t y  5   T h e  a d ve r s a r y  c a o bt a in  a e x pi r e d s e s s io n k e y .   C a pa bi li t y  6   T h e  a d v e r s a r y  c a o bt a in  t h e  pr e - s ha r e d k e y s   of   th e  n e tw o r k pa r ti c ip a nt s .   C a pa bi li t y  7   in it ia te  a n unli mi t e d numb e r   of  pa r a ll e pr o t oc o r uns  w it n e tw o r k pa r ti c ip a nt s   Evaluation Warning : The document was created with Spire.PDF for Python.
                                I S S N :   2502 - 4752   I n do n e s i a n   J   E l e c   E n &   C o m S c i ,   Vo l .   24 ,   N o .   1 Oc to b e r   2021 621   -   636   626   3 . 1.       S t r an d   s p ac e   m od e l   T h e   s t r a n s pa c e   m o de l   [ 12 ] - [ 15]   i s   a   f o r m a l   a na lys i s   m e t h o v a s t l y   us e to   pr o v e   t h e   c o r r e c t n e s s   o f   a ut h e n t i c a t i o n   pr o to c o l s .   W e   h a v e   s e l e c t e t h e   s t r a n s pa c e   m o de l   t o   pr o v e   t h e   c or r e c t n e s s   o f   ( L i g h t - A H AK A )   a s   t h e   a ut h e n t i c a t i o n   t e s t   i de a   i s   w e l l - s u i t e to   a u t h e n t i c a t i o n   pr o to c o l s   b a s e o n   t h e   c h a ll e n ge - r e s po n s e   m e c h a ni s m .   T h e   a ut h e n t i c a t i o n   t e s t s   [ 14 ] [ 16] - [ 18]   p r o vi de   r i go r o us   p oo f   f o r   e a c h   c ha l l e n ge   a n d   r e s po n s e   u s e d   i ( L i g h t - A H KA )   a n d   e ns ur e   t h a t   e a c h   r e s po ns e   f o l l o w s   t h e   c o n s t r a i n t s   o f   t h e   a ut h e n t i c a t i o t e s t s .   B e f o r e   pr o vi n t h e   c o r r e c t n e s s   o f   ( L i g h t - AH AK A )   u s i n g   t h e   s t r a n s p a c e   m o de l ,   we   w il l   d is c us s   t h e   b a s i c   n o t i o n s   o f   s t r a n s pa c e   a n t h e   a ut h e n t i c a t i o n   t e s i d e a .       3 . 1. 1.   B as ic  n ot ion s   of   t h e   s t r an d   s p ac e   m od e l   T h e   b a s i c   n o t i o ns   o f   t h e   S tr a n S pa c e   M o de l   a r e   a s   f o l l o ws :     Σ i s   t h e   s e t   o f   s t r a n s pa c e   c o m pr i s i ng  a ll   s t r a n d s   o f   t h e   pr oto c o l   pa r t i c i p a n t   i n   a dd i t i o n   to   t h e   pe n e t r a to r   s tr a n ds .       A T h e   s e t   o f   a l l   e l e m e n t s   t h a t   a r e   e x c ha n ge be t we e n   t h e   pr oto c o l   pa r t i c i pa n t s .         t a r e   t h e   e l e m e n t s   o f   s e t   A.     +   t / - t :   T h e   po s i t i v e   s i g n   m e a n s   t h e   t e r m   i s   s e n t   whil e   t h e   m i nus   s i g n   m e a n s   r e c e i ve d.     n 1 n 2 De n ot e s   t h a t   t h e   m e s s a g e   i s   s e n t   f r o m   n o de   n 1   a n r e c e i v e i n   n 2 .     n 1 n 2 De n ot e s   t h a t   n 1   a n n 2   b e l o n to   t h e   s a m e   s t r a n a n n 1   p r e c e de s   n 2   o n   t h e   gr a ph .     S S e t   o f   a l l   e dge s   i n   t h e   g r a p h .     S     n De n ot e s   t h a t   t h e   pa t h   f r o m   to   n   c o n t a i ns   o n e   or   m o r e   e dge s   i n   S.     S   n De n ot e s   t h a t   pa t h   f r o m   to   n   c o n t a i ns   z e r o r   m o r e   e dge s   i n   S.     T De n ot e s   t h e   s e t   o f   a to m i c   m e s s a ge s   e xc h a n ge i n   t h e   pr oto c o l .     K De n o t e s   t h e   s e t   o f   c r y pt o g r a ph i c   ke y s   o f   r e gu l a r   s t r a n ds .     {m} K De n o t e s   t h a t   t h e   pa r t i c i pa n t   us e t h e   c r y pt o g r a phi c   ke y   K   i n   e n c r y pt i n t h e   m e s s a g e   m .     3 . 1. 2.   P e n e t r at or   s t r an d s   I n   t hi s   s e c t i o n ,   t h e   c a pa bil i t i e s   o f   t h e   pe n e t r a tor   a r e   pr e s e n t e d,   whi c h   de p e n o n   t wo   f a c to r s .   T h e   f i r s t   o n e   i s   t h e   s e t   o f   ke y s   K P   o wn e by   t he   pe n e t r a to r ,   t h e   s e c o n i s   t h e   a bil i t y   o f   t h e   pe n e t r a tor   to   ge n e r a t e   a   n e m e s s a g e   f r o m   t h e   i n t e r c e pt e m e s s a g e s .   T he   s t r a n ds   o f   t h e   pe n e t r a to r   a r e   i ll us t r a t e i n   t h e   f o l l o w i ng   po i n t s :     T e x t   m e s s a g e   ( M ) T h e   pe n e t r a to r   c a n   s e n a   m e s s a ge   < + m>     F l us hi ng  ( F ) T h e   pe ne t r a to r   r e c e i v e s   a   m e s s a ge   f r o m   a   l e g i t im a t e   pa r t i c i pa n t   < - m>     T e e   ( T ) T h e   pe n e t r a to r   r e c e i v e s   t h e   m e s s a ge   a nd  s e n d s   i t .       C o n c a t e n a t i o n   ( C ) T h e   pe ne t r a to r   r e c e i v e s   t h e   mes s a ge s   m   a n t ,   t h e   pe n e t r a to r   j o i n s   t h e m   t o   ge t   ( mt ) ,   t h e n   s e n d s   ( mt ) .       C o m po n e n t   s e pa r a t i o n   ( S ) T h e   pe ne t r a to r   r e c e i v e s   t h e   m e s s a ge   ( mt)   a n c a n   s e p a r a t e   t h e   c o m po n e n t s   ( m)   a n ( t)   a n s e n ds   t h e m .       K e y   ( K ) T h e   pe n e t r a tor   s e n ds   a   ke y   <   +   K p>   whi c h   i s   f r o m   t h e   l i s t   o f   t h e   pe ne t r a to r   ke y s .       E n c r y pt i o n   ( E ):   T h e   pe n e t r a tor   r e c e i v e s   a   l e g i t im a t e   ke y   K   a n a   m e s s a ge   m ,   t h e e n c r y pt s   m   us i ng   K t h e n   s e n d s   {m} K       De c r y pt i o n   ( D ) T h e   pe n e t r a to r   r e c e i v e s   a   pr i va te  ke y   K −1   a n d   a   c i p h e r t e x t   {m} K ,   t h e de c r y pt s   {m} K   us i n K - 1 ,   a n e x t r a c t s   t h e   m e s s a ge   m ,   t h e n   s e n ds   it .       Ha s h   m e s s a ge   a ut h e n t i c a t i o n   c o de   ( HA M C ) T h e   pe n e t r a to r   r e c e i v e s   K   a n a   m e s s a ge   m ,   a n o b t a i ns   t h e   HM A C   f u n c t i o n .   T h e   pe ne t r a to r   c a l c u l a t e s   t he   HM A C   va l u e   o f   K | | m ,   t h e n   s e n ds   HM A C   {K   | | M }   ( a dd i t i o n a l   pe n e t r a to r   s tr a n d) .     3 . 1. 3.   Aut h e n t ic at io n   t e s t   id e a   B a s e o n   t h e   s t r a n s pa c e ,   T ha y e r   a n Gut tm a n   [ 14 ] [ 16 ] - [ 18]   pr o p o s e t h e   c o n c e pt   o f   a ut h e n t i c a t i o t e s t s .   I t   f o r m a l i z e s   t h e   c ha l l e n g e - r e s po n s e   m e t h o us e i s t r uc t ur i n m a ny   a ut h e n t i c a t i o pr oto c o l s .   I n   t h e   a ut h e n t i c a t i o n   t e s t s ,   a   pr oto c o l   pa r t i c i pa n t   t r a n s m i t s   a   t e s t   c o m po ne n t   ( e . g.   N o n c e ) ,   a n d   l a t e r   r e c e i v e s   b a c k   t h e   t e s t   c o m po n e n t   i a n o t h e r   t r a ns f o r m e f o r m ,   t h e o nly   a   r e gu l a r   p a r t i c i pa nt,   n o t   a   pe n e t r a to r ,   pe r f o r m e t hi s   t r a ns f o r m a t i o n .   A c c o r d i ng ly ,   m ut ua l   a ut h e n t i c a t i o n   c a n   be   a c hi e v e b a s e o n   t h e   i de a   o f   a ut h e n t i c a t i o n   t e s t s .   F o r   pr o vi n a   s e c u r i t y   pr oto c o l   c o r r e c t n e s s ,   o n e   o r   m o r e   o f   t h e   f o l l o w i ng  a ut h e n t i c a t i o n   t e s t s   m us t   b e   e x a mi ne d:   Evaluation Warning : The document was created with Spire.PDF for Python.
I n do n e s i a n   J   E l e c   E n &   C o m S c i     I S S N:  2502 - 4752       F or mal  s e c u r it y   analys is   of   li ghtw e ight   authentica ted  k e y   agr e e me nt  pr o tocol  f or   I o T   ( A hme H.   A ly )   627   a)   Out g o i n T e s t :   a   c ha l l e nge   ( n o nc e )   i s   s e n t   i n   a n   e n c r y pt e f o r m   by   a   pr o to c o l   pa r t i c i pa n t .   T h e   r e c e i v e r ,   a s   a   r e gu l a r   pa r t i c i p a n t ,   i s   c h a ll e n ge t o   de c r y pt   i t   a n e x t r a c t   t h e   n o n c e   a n d   s e n i t   b a c t o   t h e   s e nde r   i n   a n ot h e r   e n c r y pt e f o r m .   i . e .   t h e   e n c r y pt e f o r m   i s   go i n o u t   o f   t h e   e dge .     b)   I n c o m i ng  T e s t :   a   ch a l l e n g e   ( n o n c e )   i s   s e n t   by   a   pr oto c o l   pa r t i c i pa n t .   T h e   r e c e i v e r   i s   c h a ll e n ge d   to  e n c r y pt   t h e   n o n c e   a n s e n i t   b a c to   t h e   s e n de r   to   p r o v e   i t s   l e g i t im a c y .   i . e .   t h e   e n c r y pt e f o r m   i s   i nc o m i ng  to   t h e   e dge .     c)   Uns o l i c i t e T e s t :   a   pa r t i c i pa n t   r e c e i v e s   a   m e s s a ge   w i t h o ut   a   p r i o r   r e que s t .   I f   t h e   m e s s a ge   f o r m   s h o ws   t h a t   i t   c a n   o nly   b e   pr o duc e by   a   l e g i t i m a t e   pa r t i c i pa n t ,   we   c a de duc e   t ha t   t h e   r e gu l a r   n o de   th a t   o r i g i na t e t h e   m e s s a ge   i s   pr e c e d i ng  t h e   r e c e i v i n n o de .   I t   i s   f r e qu e n t l y   u s e i n   t h e   c a s e   o f   a   s e r v e r   r e qu e s t i n a   c l i e n t   to  s e n i t s   a ut h e n t i c a t i o n   pa r a m e t e r s .   T h e   s e c ur i t y   a n a ly s i s   o f   ( L i g h t - A H AK )   i s   b a s e o n   t h e   o ut g o i n t e s t   a n t he   u n s o l i c i t e d   t e s t ,   whi c a r e   c o n s i de r e a s   t h e   f i r s t   a n t hi r a ut h e n t i c a t i o n   t e s t s   r e s pe c t i ve l y .   T h e   t h e o r e m s   f o r   t h e s e   t wo  t e s t s   a r e   f o r m a li z e a s   f o l l o ws   T h e o r e m   1 L e t   n   a n n'     C ,   i f     + n'   i s   a n   o ut g oi ng  t e s f o r   a   i n   t   t h e n :   1)   T h e   n o de s   m,   m'      C   e xi t .   2)   i s   a   c o m po n e n t   o f   m.   3)     + m'     i s   t r a n s f o r m i ng  e dge   f o r   a.   A dd i t i o n a ll y ,   i f   :   1)   a   o c c ur s   o nl y   i n   t 1 .   2)   t1  s ub t e r m   o f   m' .   3)   K - 1     P .   T h e n   t h e r e   e xi s t s   a   r e gul a r   n e ga t i v e   n o de   t h a t   r e c e i v e s   t 1   a s   a   c o m po n e n t   whi c h   i s   n' .   T h e o r e m   2 F o r   a   t e s t   c o m po n e n t   t= {h} K n   i s   c o n s i d e r e a n   u n s o l i c i t e d   t e s t   f o r   t ,   i f   t h e r e   e xi s t s   a   po s i t i ve   r e gu l a r   n o de   m t   i s   a   c o m po n e n t   o f   and  i s   pr e c e d i n g   s uc h   t h a t   C   n.   T h e   s t r a n s pa c e   i n t r o duc e t e s t s   f o r   t e s t i n t h e   e n c r y pt e c o m po n e n t s ,   b ut   o t h e r   c r y pt o gr a ph i c   f un c t i o n s   l i ke   t h e   HM A C   a r e   n o t   r e pr e s e n t e d.   W h e n   t h e   HM A C   c r y pt o gr a ph i c   f un c t i o n   i s   us e i n   a ut h e n t i c a t i o n   pr o t o c o l s ,   t h e   f o r m a l   a n a l y s i s   b e c o m e s   m o r e   s o ph i s t i c a t e d.   T o   r e i n f o r c e   t h e   f o r m a l   a n a l y s i s   o f   t h e   a ut h e n t i c a t i o n   pr o t o c o l s ,   t h e   t e s t   t h e o r e m   o f   HM A C   i s   pr o po s e i n   [ 19]   a s   f o l l o ws :   T h e o r e m   3 L e t   t=   ( h) H M A C_ K   ter ( n) ,   i s   a   n e c o m po n e n t   o f   n   a n d   n   i s   a   n e ga t i v e   n o de ,   a s s um i n i s   s a f e .   T h e n ,   t h e r e   m us t   b e   a   r e gul a r   n o de   m   pr e c e di n n,   C   n ,   a n t   a n h   a r e   un i que l y   o r i gi n a t i n a t   m     3 . 1. 4.   L igh t - AHA K f or m a l   an a l ys is   F i gur e   s h o ws   L i g h t - A H AK A   e x e c ut i v e   b u n d le,   whi c h   c o n t a i n s   s e t s authentication  s e r v e r   s t r a n ds ,   us e r   s t r a n ds ,   I oT   s t r a n ds .   T h e   tr a c e   o f   s t r a n ds   i n   t h e   L i g h t - A H AK A   i s   pr e s e n t e i n   T a bl e   3 .           F i gur e   3 .   L i g h t - A H AK A   b u n d l e     Evaluation Warning : The document was created with Spire.PDF for Python.
                                I S S N :   2502 - 4752   I n do n e s i a n   J   E l e c   E n &   C o m S c i ,   Vo l .   24 ,   N o .   1 Oc to b e r   2021 621   -   636   628   T a bl e   3 .   S e t   o f   s t r a n ds   P r in c ip a l   S e of   S tr a nds   T r a c e   A ut he nt i c a ti o n S e r ve r  ( A S )   A S  [ H ( P W U ) , I D U I D S , I D I o T   R S1 , R S2 , R U , R T e m p 1 , R T e m p 2 , P W I o T   H M A C U1 - 3 H M A C S1 - 6 H M A C I o T 1 ]   -   ID U H ( P W U ) H M A C U1     +   {R S1 , I D S } K US   H M A C S 1       -   {R S1 , R U I D s , I D I o T }   K US   ,   H M A C U 2     A C K , H M A C S2   +   { I D S , I D I o T , R S2 }   K Io T     H M A C S3   -   H M A C I o T 1   +   A C K , H M A C S4   {R T e m p 1 , P W I o T }   K U S   ,   H M A C S5   {R T e m p 2 , I D U }   K I o T   ,   H M A C S6   >   U s e r ( U )   U [ H ( P W ) , I D U , I D S , I D I o T ,   R S1 , R U , R T e m p 1 , P W I o T   H M A C U1 - 3 H M A C S 1 , 2 , 5 ]     -   ID U H ( P W U ) H M A C U1     -   {R S1 , I D S K US   H M A C S 1       +   {R S1 , R U , I D S , I D I o T }   K US    ,   H M A C U2     -   A C K H M A C S2   -   {R T e m p 1 , P W I o T }   K U S   ,   H M A C S5   +   {PW I o T }   K T e m p   , I D U ,   H M A C U3   >   I oT ( D )         D  [ I D I o T , I D U , I D S , P W I o T ,   R S2 , R T e m p 2 , R U H M A C I o T 1 H M A C S 3 , 4 , 6 ,   H M A C U3 ]   -   { I D S , I D I o T , R S2 }   K I o T     ,   H M A C S 3     +   H M A C I o T 1   -   A C K H M A C S4   -   {R T e m p 2 , I D U }   K I o T   H M A C S6   -   {PW I o T }   K T e m p   , I D U   ,   H M A C U3   >           4. 1. 5.   S t r an d   s p ac e   p r oo f   I n   t hi s   s e c t i o n ,   t h e   c o r r e c t n e s s   o f   ( L i g h t - A H AK A )   w il l   be   pr o v e by   pr o p o s i n e i g h t   l e mm a s   f o r   b u n d l e   C   w hi c h   i s   i n   Σ   s pa c e .     A c c o r d i n to   F i gur e   a n T a bl e :     T h e   authentication  s e r v e r   s t r a n S AS     AS   i s   i n   b u nd l e   C   a n i t s   h e i g h t   i s   9     K US   a n K Io T     P     T h e   r a n do m   n u m be r s   R S1 ,   R S2 ,   and  R U   a r e   f r e s h   v a lues   a n u ni que ly   o r i g i na t i n i n   Σ .     T h e r e   i s   us e r   s t r a n S U     U   i n   b u n d l e   C   a n i t s   h e igh t   i s   a l e a s t .       T h e r e   i s   I oT   s t r a n S D     i n   b u n d l e   C   a n i t s   h e i g h t   i s   a l e a s t .   L e mm a   1:   I f     P ,   t h e n   n o de   n=   < S,   1>   i s   a n   u n s o l i c i t e d   t e s t   f o r   =   {P W } H   wh e r e   t h e   o r i g i na t i ng  e dge   i s   m= < U, 1>   a n a   PW .   P r oof :   A c c o r d i n to   T h e o r e m   2,   = < U, 1>   i s   t he   o nl y   po s i t i v e   r e gu l a r   n o de   whe r e   t     m   n   f o r   a l l   n   s uc h   t h a t   C   n .   L e mm a   2 :   I f   K US     P R S1   i s   uni qu e l y   o r i g i na t i n i < S,   2>   t h e n   t h e   e dge   < S,   2>   +   < S,   3>   i s   a n   o u t g o i n g   t e s t   f o r   R S 1 t =   { R S1 ,   I D S }   K US   i s   t h e   t e s c o m po n e n t   a n a=   R S1 .   P r oof :   A c c o r di n to   T h e or e m   1 pr o v i n t h e   l e m ma  i s   a c hi e v e by   f i nd i ng  t w o   r e gul a r   n o de s   ( m m′   )   i n   b u n d l e   C   a n +   m'   i s   t r a n s f o r m i ng  e dge   f o r   R S1 .   I n   F i gur e = < U , 2>   i n   us e r   s t r a n S U ,   a n m′  = < U, 3>   i n   S U .   L e mm a   3 I f   K US     P R U   i s   u ni que ly   o r i g i na t i n in   < U,   3> t h e n   t h e   e dge   < U,   3>   +   < U,   4>   i s   a n   o u t g o i n g   t e s t   f o r   R U t=   { R S1 ,   R U ,   I D s ,   I D I o T }   K US   i s   t h e   t e s t   c o m po n e n t   a n a=   R U   a n t h e   r e s po n s e   i s   i HM A C S2   us i n g   R U     P   a s   t h e   ke y   f o r   t h e   HM A C S2 .   P r oof :     1)   A c c or di n g   to  T h e or e m   1 ,   p r ov i n th e   l e m m a   i s   a c h i e v e b y   f i n di n g   tw r e g u l a r   n od e s   ( m m′ )   i n   b un dl e   C   a n d   +   m '   i s   tr a n s f or m i n g   e d g e   f or   R U .   I n   F i g u r e m   = < S , 3 >   i n   s e r v e r   s tr a n d   S AS ,   a n d   m = < S , 4 >   of   S AS .   2)   A c c o r di n t o   T h e o r e m   3   a n F i gur e n= < U,   4>   i s   t h e   o n l y   n e ga t i v e   n o de   o f   us e r   s t r a n S U ,   a n t h e   t e s t   c o m po n e n t     t=   HM A C S3   is   s ub - t e r m   o f   t h e   n o de   n   a n a   n e c o m po n e n t   o f   t h i s   n o de ,   wh i l e   R U     P T h e n   t h e   po s i t i v e   n o de   m= < S,   4>   s uc h   t h a t   C   n ,   wh e r e   i s   un i que l y   o r i gi n a t i n a t   m .   Evaluation Warning : The document was created with Spire.PDF for Python.
I n do n e s i a n   J   E l e c   E n &   C o m S c i     I S S N:  2502 - 4752       F or mal  s e c u r it y   analys is   of   li ghtw e ight   authentica ted  k e y   agr e e me nt  pr o tocol  f or   I o T   ( A hme H.   A ly )   629   F r o m   t h e   pr oo f   o f   t h e   t h r e e   a f o r e m e n t i o ne l e mm a s ,   we   pr o v e   t h e   c or r e c t n e s s   o f   t h e   m ut ua l   a ut h e n t i c a t i o n   be t we e n   t h e   a ut he n t i c a t i o s e r v e r   S   a n t h e   us e r   U ;   m o r e o v e r ,   t h e   r a n do m   n u m be r s   ( R S1   &   R U a r e   f r e s hly   ge n e r a t e f r o m   r e gu l a r   s t r a n ds .   L e mm a   4 I f   K Io T     P R S2   i s   u ni que ly   o r i g i na t i n i n   < S,   5>   t h e n   t h e   e dge   < S,   5>   +   < S ,   6>   i s   a n   o u t g o i n g   t e s t   f o r   R S2 t=   { I D S ,   I D Io T ,   R S2 }   K Io T   i s   t h e   t e s t   c o m p o n e n t   a n a=   R S2 ,   a n t h e   r e s po n s e   i s   i n   HM A C S2   us i n R U     P   a s   t h e   ke y   f o r   t h e   HM A C S2 .   P r oof :     1)   A c c o r d i n t T h e o r e m   1,   pr o vi n t h e   l e mm a   i s   a c hi e v e by   f i nd i ng  t wo  r e gul a r   n o de s   (   m m′ )   i n   b u n d l e   C   a n +   m'   i s   t r a n s f o r m i ng   e dge   f o r   R S2 .   I n   F i gur e   3 ,   m= < D, 1>   i n   D   s t r a n S D,   a n m′= < D, 2>   o f   S D .   2)   A c c o r di n t o   T h e o r e m   3   a n F i gur e   3 n= < S,   6>   i s   t h e   o n l y   n e ga t i v e   s e r v e r   s t r a n S AS ,   a n t h e   t e s t   c o m po n e n t   t=   HM A C Io T 1   i s   s ub - t e r m   o f   t h e   n o de     a n a   n e c o m po n e n t   t h i s   n o de ,   wh i l e   K ds     P T h e n   t h e   po s i t i v e   n o de   m= < D,   2>   s uc h   t h a t   C   n ,   wh e r e   i s   un i que l y   o r i gi n a t i n a t   m .   F r o m   t h e   pr o o f   o f   t h e   pr e vi o u s   l e m m a ,   we   pr o v e   t h e   c o r r e c t n e s s   o f   t h e   m ut ua l   a ut h e n t i c a t i o b e t we e n   t h e   a ut h e n t i c a t i o n   s e r v e r   S   a n t h e   I oT   d e vi c e .   F ur t h e r m o r e ,   t h e   r a n do m   n u m be r s   ( R S2   )   a r e   f r e s hl y   ge n e r a t e f r o m   a   r e gu l a r   s t r a n d.   L e m m a   5 :   I f   R Io T     P HM A C S4   i s   un i que l y   o r i gi n a t i n i n   m= < D,   3>   t h e n   t h e   n o de   n=   < S,   7>     i s   a   t e s t   f o r     t=   HM A C S4   wi t h   R Io T   a s   a   ke y ,   a n t h e   t e s t   c o m po n e n t   i s   a=   A C K .   P r oof :   A c c o r di n t o   T h e o r e m   a n F i gur e   3 n   i s   t h e   o n l y   n e ga t i v e   n o de   o f   b un dl e   C ,   a n t=   HM A C S4     ter ( n)   i s   a   n e c o m po n e n t   o f   n   wi t h     P .   T h e n   t h e   po s i t i v e   n o de   m= < S,   7>   s uc h   t h a t   C   n ,   wh e r e   i s   un i que l y   o r i gi n a t i n a t   m .   L e mm a   6 I f   K US     P ,   t h e n   n o de   n=   < U,   5>   i s   a n   un s o l i c i t e t e s t   f o r   =   {R T e m p 1 ,   P w Io T } K US   wh e r e   m = < S,   8 >   a n a   R T e m p 1 .   P r oof :   A c c o r d i n t o   T h e o r e m   a n F i gur e   3 m= < S, 8>   i s   t h e   o nly   po s i t i v e   n o de   i n   s e r v e r   s t r a n S AS   wh e r e   t     m   n   f o r   a l l   n   s u c h   t h a t   C   n .   L e mm a   7 I f   K Io T     P ,   t h e n   n o de   n=   < D,   4>   i s   a un s o l i c i t e t e s t   f o r   =   {R T e m p 2 ,   I D U } K Io T   wh e r e   m= < S,   9 >   a n a   R T e m p 2 .   P r oof :   A c c o r d i n t o   T h e o r e m   a n F i gur e   3 m= < S, 9>   i s   t h e   o nly   po s i t i v e   n o de   i n   s e r v e r   s t r a n d   S AS   wh e r e   t     m   n   f o r   a l l   n   s u c h   t h a t   C   n .   L e mm a   8 :   I f   K T e m p     P ,   t h e n o de   n=   < D,   5>   i s   a n   u ns o l i c i t e t e s t   f o r   =   {P w } K T e m p   wh e r e   m= < U,   6>   a n d   a   Pw .   P r oof :   A c c o r di n t o   T h e o r e m   a n F i gur e   3 m= < U, 6>   i s   t h e   o nly   po s i t i ve   n o de   i n   us e r   s t r a n S U   wh e r e   t     m   n   f o r   a l l   n   s uc h   t h a t   C   n .     4. 2.       S im u l at ion   f or   f o r m a l   s e c u r it ve r if i c at ion   u s in AV I S P t ool   T o   e n s ur e   t h e   c o r r e c t n e s s   o f   ( L i g h t - A H AK A ) ,   w e   us e d   a ut o m a t e v a li da t i o n   o f   i n t e r n e t   s e c ur i t y   pr oto c o l s   a n a pp l i c a t i o ns   ( A VI S P A )   a s   a   too l   f o r   s i m u l a t i n ( L i g h t - A H AK A ) .       4. 2. 1.     AV I S P A   A VI S P A   i s   a n   a ut o m a t e too l   us e f o r   v a li da t i n s e c ur i t y   pr oto c o l s   a n c r y pt o gr a phi c     a pp l i c a t i o ns   [ 20 ] - [ 22] .   A VI S P A   i s   us e d   f o r   a n a ly z i ng  t h e   s e c ur i t y   pr o pe r t i e s   o f   t h e   i nve s t i ga t e pr oto c o l s   b y   s e a r c hi ng  f o r   po s s i bl e   a t t a c ks   i n   d i f f e r e n t   s c e na r i o s .   W e   s p e c i f i e ( L i g h t - A H AK A )   i hi g h - l e v e l   pr oto c o l   s pe c i f i c a t i o n   l a n gua ge   ( HL P S L ) ,   whi c h   i s   a   r o l e - ba s e l a n gu a ge   de v e l o pe f o r   A VI S P A .     T h e   HL P S L   l a n gua ge   s p e c i f i e s   t h e   d i f f e r e n t   r o l e s   i n   t h e   a ut h e n t i c a t i o n   pr oto c o l s .   E a c h   r o l e   r e pr e s e n t s   a   pr oto c o l   pa r t i c i p a n t ,   a n t h e n   a l l   t h e   r o l e s   a r e   c o m po s e to   r e pr e s e n t   t h e   i n t e r a c t i n b e ha vi o r   o f   t h e   pa r t i c i p a n t s .   E a c h   r o l e   s pe c i f i e i n   H L P S L   i s   i n de pe n d e n t   o f   t h e   ot h e r   r o l e s ,   s e t t i n t h e   i ni t i a l   k no wl e dg e   o f   e a c h   r o l e   a n c o m m u ni c a t i n w i t h   t h e   o t h e r   r o l e s   vi a   da t a   t r a n s f e r   c ha nn e l s .   HL P S L   i s   a   r o l e - b a s e d   l a n gua ge ,   i s uc a   w a y   t h a t   t h e   s e qu e n c e   o f   a c t i o n s   o f   e a c pr oto c o l   pa r t i c i pa n t   i s   s pe c i f i e d   i a   s e pa r a t e   m o du l e ,   w hi c h   i s   c a ll e a   ba s i c   r o l e .   Af t e r   c o m p l e t i n t h e   s t e o f   s pe c i f yi ng  a ll   t h e   r o l e s   o f   t h e   pr oto c o l   pa r t i c i pa n t s ,   t h e s e   r o l e s   w il l   b e   i ns t a n t i a t e by   o n e   or   m o r e   a ge n t s   p l a y i ng  t h e   g i ve n   r o l e   a n de s c r i b i ng  h o t h e   pa r t i c i pa n t s   i n t e r a c t   wi t h   e a c h   ot h e r   by   c o n c a t e n a t i n a l l   t h e   b a s i c   r o l e s   to ge t h e r   i n t o n e   c o m po s e r o l e .   A VI S P A   us e s   t h e   H L P S L 2I F   t oo l   f o r   t r a n s f o r m i n a   s pe c if i c a t i o n   wr i t t e n   i t h e   H L P S L   l a n gua g e   i n t o   a   l o w - l e v e l   s pe c i f i c a t i o n   i t h e   I F   l a n gua ge .   T hi s   t oo l   c o m p i l e s   t h e   s pe c if i c a t i o n   o f   a   pr oto c o l   g i v e n   a s   a   pa r a m e t e r   i n   a   f il e   w i t h   t h e   e x t e n s i o n   ( . hl ps l ) ,   a n e i t h e r   l i s t s   t h e   e r r or s   f o un i n   t h e   s pe c if i c a t i o n   o r   ge n e r a t e s   a   f il e   w i t h   t h e   s a m e   n a m e   b ut   wi t h   a   n e e x t e n s i o n   ( . i f )   c o n t a i ni ng  t h e   s pe c if i c a t i o n   t h a t   wi ll   be   a n a ly z e d   l a t e r   o n .   I n   t h e   f i e l o f   de s i g ni ng  li g h t we i g h t   a uth e n t i c a t i o n   pr o to c o l s   f o r   I o T - C l o ud  c o m put i n g,   nu m e r o us   r e s e a r c h e r s   [ 23 ] - [ 28]   r e l i e o n   t h e   A VI S P A   t oo l   f o r   s i m u l a t i n t h e i r   pr o p o s a l s   a n v e r i f yi ng  t h e   c o r r e c t n e s s   o f   t h e   pr o p o s e l i g h t we i g h t   pr oto c o l s ,   a s   A VI S P A   pr e s e n t s   f o ur   pr oto c o l   a n a ly z e r   too l s on - t h e - f ly   m o de l - Evaluation Warning : The document was created with Spire.PDF for Python.
                                I S S N :   2502 - 4752   I n do n e s i a n   J   E l e c   E n &   C o m S c i ,   Vo l .   24 ,   N o .   1 Oc to b e r   2021 621   -   636   630   c h e c ke r   ( OFM C [ 29] S A T - b a s e d   m o de l - c h e c k e r   ( S A T M C [ 30] c o n s t r a i n t   l o g i c - b a s e d   a t t a c k   s e a r c h e r   ( CL - A t S e [ 31] a n tr e e   a u to m a t a   b a s e o n   a utom a t i c   a ppr o xi m a t i o ns   f o r   t h e   a n a ly s i s   o f   s e c ur i t y   pr oto c o l s   ( T A 4S P [ 32 ]   A VI S P A   im p l e m e n t a t i o n   c o n s i s t s   o f   t h e   us e r s '   r o l e s ,   s e s s i o r o l e ,   e nvi r o nm e n t   r o l e ,   a n d   f i na l ly   t h e   s e c ur i t y   go a l s .   T h e   us e r   r o l e s   c o m p r i s e   a ll   a ge n t s   i n   t h e   pr o to c o l ,   t h e   s y mm e t r i c   ke y s ,   a n f in a ll y   t h e   s e n d/r e c e i ve   c h a nn e l s .   Al l   t h e   m e s s a ge s   e xc h a n ge vi a   t h e   c h a nne l s   a r e   s u bj e c t e to  t h e   c o n t r o l   o f   t h e   Do l e v - Ya o   ( dy )   i n t r ude r   m o de l .   A c c o r d i n t o   t h i s   m o d e l ,   i t   i s   a s s u m e t h a t   t h e   i n t r u de r   h a s   f u ll   po we r   o v e r   t h e   c o m m u ni c a t i o n   ne t wor k,   s uc h   t h a t   a l l   m e s s a ge s   e x c h a n g e by   t h e   a ge n t s   a r e   i n t e r c e pt e by   t h e   i n t r ude r .   I n   a dd i t i o n ,   t h e   i n t r ude r   h a s   t h e   po we r   to   a n a l y z e ,   m o d i f y ,   a n c o m po s e   n e m e s s a g e s   t o   ot h e r   pr oto c o l   pa r t i c i pa n t s ,   pr e t e n d i n t h a t   t h e s e   m e s s a g e s   we r e   ini t i a t e by   a   l e g i t im a t e   a ge n t .   T h e   l o c a l   s e c t i o n   de f i ne s   a l l   t h e   l o c a l   v a r i a bl e s   us e by   e a c h   r o l e .       4. 2. 1.   Us e r   r o l e   F i gur e   s h o ws   t h e   r o l e   o f   t h e   us e r   ( U) ,   w hi c h   i s   c o n s i de r e a s   t h e   i ni t i a t o r   o f   t h e   pr oto c o l ,   p l a y e d   by   U .   T h e   k n o w l e dge   o f   U   c o m pr i s e s   a ll   a ge n t s   i t h e   pr oto c o l   ( U ,   a ut h e n t i c a t i o n   s e r v e r   ( S) ,   I o T   de vi c e   ( D) ,   a n t h e   s ymm e t r i c   pr e - s h a r e ke y   (k us )   b e t we e n   U   a n S   "R c v ( s tar t) "   i s   s e n t   to   U   a s   a   t r i gge r   s i g n a l   t o   i ni t iat e   t h e   pr oto c o l   r un U   s t a r t s   t h e   r e gi s t r a t i o n   p h a s e   w i t h   t h e   a ut h e n t i c a t i o n   s e r v e r   S   ( s t e 1)   a n a f t e r   s uc c e s s f u l   r e g i s t r a t i o n ,   U   s t a r t s   t h e   m ut ua l   a ut h e n t i c a t i o pr o c e s s   w i t h   S   ( s t e ps   &   3) .   F i na ll y ,   U   r e c e i ve s   a n   a c k n o w l e dg m e n t   ( A C K )   f r o m   t h e   s e r v e r   ( s t e 4) .   I n   s t e ( 5) ,   r e c e i v e s   t h e   c r e de n t i a l s   o f   f r o m   t h e   s e r v e r   a n s e n ds   a n   a c c e s s   r e que s t   to   ( s t e p   6) .           F i gur e   2 .   Us e r   r o l e       4. 2. 2.   S e r ve r   r o l e   F i gur e   5   s h o ws   t h e   r o l e   o f   t h e   s e r ve r   ( S) .   S   r e c e iv e s   a   r e g i s t r a t i o n   r e que s t   f r o m   U   ( s t e 1) .   T h e n   S   s t a r t s   t h e   m ut ua l   a ut h e n t i c a t i o n   pr o c e s s   w i t h   U   ( s t e ps   &   3)   a n d   a f t e r   pa s s i ng  t h e   m ut ua l   a ut he n t i c a t i o n ,   S   w i ll   s e n U   t h e   A C K   m e s s a ge   ( s t e 4) .   T h e n ,   S   w i ll   s t a r t   a u t h e n t i c a t i n t h e   i n t e n de d   I o T   de vi c e   D   ( s t e ps   a n d   6) .   Af t e r   s uc c e s s f u l   a ut h e n t i c a t i o n ,   S   s e n ds   D   a A C K   m e s s a ge   ( s t e 7) .   F i n a ll y ,   S   s e n ds   t h e   c r e de n t i a l s   o f   D   to  ( s t e p   8) ,   a n t h e   i de n t i t y   o f   U   to   D   ( s t e 9) .     4. 2. 3.   De vice   r ol e   F i gur e   s h o ws   t h e   r o l e   o f   t h e   d e vi c e   ( D) D   r e c e i v e s   t h e   c h a ll e n ge   f r o m   t h e   s e r v e r   t o   s t a r t   t h e   m ut ua l   a ut h e n t i c a t i o n   pr o c e s s   ( s t e 1) .   r e s po n ds   w i t h   t h e   HM A C   o f   S   c h a ll e n ge   c o nc a t e n a t e w i t h   i t s   pa s s wo r ( s t e 2) .   S   v e r i f i e s   t h e   HM A C   o f   D ,   t h e S   r e p l i e s   w i t h   t h e   a c k n o w l e dg m e n t   A C K   ( s t e 3) .   I n   ( s t e 4) ,   S   s e n ds   D   t h e   i d e n t i t y   o f   U   t h a t   i s   r e que s t i n a c c e s s   t o   t h e   da t a   f r o m   t h e   I oT   de vi c e .   F i na ll y ,   i ( s t e 5)   r e c e i v e s   t h e   a c c e s s   r e que s t   f r o m   U .   Evaluation Warning : The document was created with Spire.PDF for Python.