9. Особенности мобильной связи. π-исчисление мобильных процессов. Синтаксис π-исчисления. Операционная семантика π-исчисления (1265180), страница 3
Текст из файла (страница 3)
X1 = {(b, K , r1 , N)}k1 .at(X2 ). abhX2 i. abh{m, N}K ikab[Y2 ].Y2 = (U, L). ab[Y3 ]. Y3 = {(M, r2 )}Lk(b, {a, r1 , r2 }k2 ) = (b, {a, R1 , R2 }k2 ).ν`. ath{(b, `, R1 , R2 )}k1 i. ath{(a, `)}k2 iÏðèìåðÂû÷èñëåíèå ïðîòîêîëà Yahalomat[X1 ].
X1 = {(b, K , r1 , N)}k1 .at(X2 ). abhX2 i. abh{m, N}K ikab[Y2 ].Y2 = (U, L). ab[Y3 ]. Y3 = {(M, r2 )}Lk{R1 /r1 , R2 /r2 }ν`. ath{(b, `, R1 , R2 )}k1 i. ath{(a, `)}k2 iÏðèìåðÂû÷èñëåíèå ïðîòîêîëà Yahalomat[X1 ]. X1 = {(b, K , r1 , N)}k1 .at(X2 ). abhX2 i. abh{m, N}K ikab[Y2 ].Y2 = (U, L). ab[Y3 ]. Y3 = {(M, r2 )}Lkν`. ath{(b, `, r1 , r2 )}k1 i. ath{(a, `)}k2 iÏðèìåðÂû÷èñëåíèå ïðîòîêîëà Yahalomat[X1 ]. X1 = {(b, K , r1 , N)}k1 .at(X2 ). abhX2 i.
abh{m, N}K ikab[Y2 ]. Y2 = (U, L). ab[Y3 ]. Y3 = {(M, r2 )}Lkν`. ath{(b, `, r1 , r2 )}k1 i. ath{(a, `)}k2 iÏðèìåðÂû÷èñëåíèå ïðîòîêîëà Yahalomat[X1 ]. X1 = {(b, K , r1 , N)}k1 .at(X2 ). abhX2 i. abh{m, N}K ikab[Y2 ]. Y2 = (U, L). ab[Y3 ]. Y3 = {(M, r2 )}Lkν`. ath{(b, k, r1 , r2 )}k1 i. ath{(a, `)}k2 i{`/k}ÏðèìåðÂû÷èñëåíèå ïðîòîêîëà YahalomX1 = {(b, K , r1 , N)}k1 .{X1 /{(b, k, r1 , r2 )}k1 }at(X2 ). abhX2 i. abh{m, N}K ikab[Y2 ].
Y2 = (U, L). ab[Y3 ]. Y3 = {(M, r2 )}Lkath{(a, k)}k2 iÏðèìåðÂû÷èñëåíèå ïðîòîêîëà Yahalom{(b, k, r1 , r2 )}k1 = {(b, K , r1 , N)}k1 .at(X2 ). abhX2 i. abh{m, N}K ikab[Y2 ]. Y2 = (U, L). ab[Y3 ]. Y3 = {(M, r2 )}Lkath{(a, k)}k2 iÏðèìåðÂû÷èñëåíèå ïðîòîêîëà Yahalom{K /k, N/r2 }at(X2 ). abhX2 i.
abh{m, N}K ikab[Y2 ]. Y2 = (U, L). ab[Y3 ]. Y3 = {(M, r2 )}Lkath{(a, k)}k2 iÏðèìåðÂû÷èñëåíèå ïðîòîêîëà Yahalomat(X2 ). abhX2 i. abh{m, r2 }k ikab[Y2 ]. Y2 = (U, L). ab[Y3 ]. Y3 = {(M, r2 )}Lkath{(a, k)}k2 iÏðèìåðÂû÷èñëåíèå ïðîòîêîëà Yahalomat(X2 ). abhX2 i. abh{m, r2 }k ikab[Y2 ]. Y2 = {(a, L)}k2 . ab[Y3 ]. Y3 = {(M, r2 )}Lkath{(a, k)}k2 iÏðèìåðÂû÷èñëåíèå ïðîòîêîëà Yahalomat(X2 ). abhX2 i. abh{m, r2 }k ikab[Y2 ]. Y2 = {(a, L)}k2 . ab[Y3 ]. Y3 = {(M, r2 )}Lkath{(a, k)}k2 iÏðèìåðÂû÷èñëåíèå ïðîòîêîëà YahalomabhX2 i. abh{m, r2 }k i{X2 /{(a, k)}k2 }kab[Y2 ].
Y2 = {(a, L)}k2 . ab[Y3 ]. Y3 = {(M, r2 )}LÏðèìåðÂû÷èñëåíèå ïðîòîêîëà Yahalomabh{(a, k)}k2 i. abh{m, r2 }k ikab[Y2 ]. Y2 = {(a, L)}k2 . ab[Y3 ]. Y3 = {(M, r2 )}LÏðèìåðÂû÷èñëåíèå ïðîòîêîëà Yahalomabh(a, k)}k2 i. abh{m, r2 }k ikab[Y2 ]. Y2 = {(a, L)}k2 . ab[Y3 ]. Y3 = {(M, r2 )}LÏðèìåðÂû÷èñëåíèå ïðîòîêîëà Yahalomabh{m, r2 }k ikY2 = {(a, L)}k2 . ab[Y3 ]. Y3 = {(M, r2 )}L {Y2 /{(a, k)}k2 }ÏðèìåðÂû÷èñëåíèå ïðîòîêîëà Yahalomabh{m, r2 }k ik{(a, k)}k2 = {(a, L)}k2 .
ab[Y3 ]. Y3 = {(M, r2 )}LÏðèìåðÂû÷èñëåíèå ïðîòîêîëà Yahalomabh{m, r2 }k ikab[Y3 ]. Y3 = {(M, r2 )}L{L/k}ÏðèìåðÂû÷èñëåíèå ïðîòîêîëà Yahalomabh{m, r2 }k ikab[Y3 ]. Y3 = {(M, r2 )}kÏðèìåðÂû÷èñëåíèå ïðîòîêîëà Yahalomabh{m, r2 }k ikab[Y3 ]. Y3 = {(M, r2 )}kÏðèìåðÂû÷èñëåíèå ïðîòîêîëà Yahalomabh{m, r2 }k ikab[Y3 ]. Y3 = {(M, r2 )}kÏðèìåðÂû÷èñëåíèå ïðîòîêîëà YahalomY3 = {(M, r2 )}k{Y3 /{(m, r2 )}k }ÏðèìåðÂû÷èñëåíèå ïðîòîêîëà Yahalom{(m, r2 )}k = {(M, r2 )}kÏðèìåðÂû÷èñëåíèå ïðîòîêîëà Yahalom{M/m}Ïðèìåíåíèå spi-èñ÷èñëåíèÿ âêðèïòîàíàëèçåÊ êðèïòîãðàôè÷åñêèì ïðîòîêîëàì îáû÷íî ïðåäúÿâëÿþòñÿ òðèãëàâíûõ òðåáîâàíèÿ áåçîïàñíîñòè.Êîíôèäåíöèàëüíîñòü äàííûõ.Îáåñïå÷åíèå òàêîé îðãàíèçàöèè õðàíåíèÿ èíôîðìàöèè è ååèñïîëüçîâàíèÿ â êðèïòîãðàôè÷åñêîì ïðîòîêîëå, ïðè êîòîðûõýòà èíôîðìàöèÿ îñòàåòñÿ íåäîñòóïíîé ïðîòèâíèêó.Öåëîñòíîñòü ñîîáùåíèé.Ãàðàíòèðóåìàÿ ïîëó÷àòåëþ âîçìîæíîñòü óäîñòîâåðèòüñÿ, ÷òîñîîáùåíèå ïîñòóïèëî îò äàííîãî îòïðàâèòåëÿ è âíåèñêàæåííîì âèäå.Íåîòñëåæèâàåìîñòü.Ãàðàíòèÿ òîãî, ÷òî ïðîòèâíèê íå òîëüêî íå ìîæåò óñòàíîâèòü,êòî èìåííî âûïîëíèë äàííîå êîíêðåòíîå äåéñòâèå, íî äàæåâûÿñíèòü, áûëè ëè äàííûå äâà èëè áîëåå äåéñòâèé âûïîëíåíûîäíèì è òåì æå ó÷àñòíèêîì.Ïðèìåíåíèå spi-èñ÷èñëåíèÿ âêðèïòîàíàëèçåÓêàçàííûå òðåáîâàíèÿ áåçîïàñíîñòè ñòðåìèòñÿ íàðóøèòüïðîòèâíèê, êîòîðûé ìîæåò âìåøèâàòüñÿ â ðàáîòó ïðîòîêîëà,ïðåñëåäóÿ íåêîòîðûå öåëè.Ñîâîêóïíîñòü ïðåäïîëîæåíèé î ïðîòèâíèêå, â ðàìêàõ êîòîðûõàíàëèçèðóåòñÿ ñòîéêîñòü êðèïòîãðàôè÷åñêîãî ïðîòîêîëà,íàçûâàåòñÿ àòàêîé .Àòàêà âêëþ÷àåò â ñåáÿ èíôîðìàöèþ, êîòîðóþ ïðîòèâíèê ìîæåòïîëó÷èòü â õîäå âûïîëíåíèÿ ïðîòîêîëà, è àêòèâíûå äåéñòâèÿïî âìåøàòåëüñòâó â ïðîöåññ âûïîëíåíèÿ ïðîòîêîëà, êîòîðûåïðîòèâíèê ìîæåò îñóùåñòâèòü.Ïðèìåíåíèå spi-èñ÷èñëåíèÿ âêðèïòîàíàëèçåÏðè àíàëèçå ìîäåëåé êðèïòîãðàôè÷åñêèõ ïðîòîêîëîâ,âûïîëíåííûõ â π-èñ÷èñëåíèè, ïðèäåðæèâàþòñÿ ñëåäóþùèõïðåäïîëîæåíèé î âîçìîæíîñòÿõ ïðîòèâíèêà.1.
âñå êðèïòîãðàôè÷åñêèå ïðèìèòèâû, ïðåäñòàâëåííûåòåðìàìè π-èñ÷èñëåíèÿ, ñ÷èòàþòñÿ àáñîëþòíî ñòîéêèìè;2. ïðîòèâíèêó íåèçâåñòåí ëèøü ñòðîãî îãðàíè÷åííûé íàáîðäàííûõ Private (èìåíà, êëþ÷è, ñîîáùåíèÿ è ïð.),êîòîðûìè îáëàäàþò ó÷àñòíèêè ïðîòîêîëà;3. ïðîòèâíèê îáëàäàåò ñïîñîáíîñòüþ ïîëó÷àòü è ïåðåäàâàòüñîîáùåíèÿ ïî òåì æå êàíàëàì ñâÿçè, êîòîðûåèñïîëüçóþòñÿ ó÷àñòíèêàìè ïðîòîêîëà.Òàêèì îáðàçîì, äëÿ ïðîòîêîëà, ïðåäñòàâëåííîãî â âèäåïðîöåññà π-èñ÷èñëåíèÿ, â êà÷åñòâå ìîäåëè ïðîòèâíèêàöåëåñîîáðàçíî òàêæå èñïîëüçîâàòü ïðîöåññ π-èñ÷èñëåíèÿ íàäìíîæåñòâîì èìåí Names \ Private .Ïðèìåíåíèå spi-èñ÷èñëåíèÿ âêðèïòîàíàëèçåÏðåäïîëîæèì, ÷òî Alice ñîáèðàåòñÿ ïîëó÷èòü îò Bob ñåêðåòíûåäàííûå ïî çàêðûòîìó êàíàëó ñâÿçè.Alice :Bob :Mallory :ν x.
chh(A, x)i. x[y ]. y = (B, M). nilkch[z]. z = (A, u). uh(B, secret)i. nilkch[z]. ν u. chh(A, u)i. u[v ]. nilÍî çëîóìûøëåííèê Mallory ìîæåò ïåðåõâàòûâàòü ñîîáùåíèÿ, ...Ïðèìåíåíèå spi-èñ÷èñëåíèÿ âêðèïòîàíàëèçåÏðåäïîëîæèì, ÷òî Alice ñîáèðàåòñÿ ïîëó÷èòü îò Bob ñåêðåòíûåäàííûå ïî çàêðûòîìó êàíàëó ñâÿçè.Alice :Bob :Mallory :ν x. chh(A, x)i. x[y ]. y = (B, M). nilkch[z]. z = (A, u). uh(B, secret)i. nilkch[z].
u = (A, u). uh(B, faked)i. nilèëè ïîäìåíÿòü ñîîáùåíèÿ.×òîáû èçáåæàòü ýòîãî, ó÷àñòíèêè ïðîòîêîëà äîëæíû èìåòüíåêîòîðûé ðàçäåëÿåìûé ñåêðåò, íåèçâåñòíûé ïðîòèâíèêó, ïðèïîìîùè êîòîðîãî ìîæíî çàùèòèòü ïåðåñûëàåìûå äàííûå.Ïðèìåíåíèå spi-èñ÷èñëåíèÿ âêðèïòîàíàëèçåÍàïðèìåð, òàê:System(secrete) :Alice :Bob :ν K.ν x. chh(A, x)i. x[y ]. y = ({B, M}K ). nilkch[z]. z = (A, u). uh({B, secret}K )i.
nil.nilkMallory :???À ñïîñîáåí ëè òåïåðü çëîóìûøëåííèê Mallory ÷òî-íèáóäüóçíàòü î ïåðåñûëàåìûõ äàííûõ?È êàê äîêàçàòü, ÷òî íèêàêîé çëîóìûøëåííèê íå ñìîæåòèçâëå÷ü íèêàêîé èíôîðìàöèè î ïåðåñûëàåìûõ äàííûõ?Ïðèìåíåíèå spi-èñ÷èñëåíèÿ âêðèïòîàíàëèçå 1982 ã. Sha Goldwasser è Silvio Micali âïåðâûå ïðåäëîæèëèñõåìó âåðîÿòíîñòíîãî øèôðîâàíèÿ ñ îòêðûòûì êëþ÷îì èñóìåëè äîêàçàòü åå ñòîéêîñòü.Äëÿ äîêàçàòåëüñòâà ñâîéñòâ êîíôèäåíöèàëüíîñòèêðèïòîñèñòåìû åå àâòîðû ââåëè øèðîêî èñïîëüçóåìîå ïîíÿòèåñåìàíòè÷åñêîé ñòîéêîñòè, ñóòü êîòîðîãî ìîæíî âûðàçèòü òàê:êðèïòîñèñòåìà ñ÷èòàòåòñÿ ñòîéêîé, åñëè íèêàêîé ïðîòèâíèê,îáëàäàþùèé ðàçóìíûì îáúåìîì âû÷èñëèòåëüíûõ ðåñóðñîâ, íèäëÿ êàêèõ äâóõ ðàçíûõ ñîîáùåíèé íå ìîæåò îòëè÷èòüøèôðòåêñòû îäíîãî ñîîáùåíèÿ îò øèôðòåêñòîâ äðóãîãî, èëè,åùå ïðîùå, íå ìîæåò îòëè÷èòü øèôðòåêñòû 0 îò øèôðòåêñòîâ1.Ïîïðîáóåì àäàïòèðîâàòü èäåþ ñåìàíòè÷åñêîé ñòîéêîñòèêðèïòîñèñòåì ïðèìåíèòåëüíî ê ìîäåëÿì êðèïòîãðàôè÷åñêèõïðîòîêîëîâ.Ïðèìåíåíèå spi-èñ÷èñëåíèÿ âêðèïòîàíàëèçåÐàññìîòðèì íåêîòîðîå îòíîøåíèå ýêâèâàëåíòíîñòè ∼= íàìíîæåñòâå ïðîöåññîâ spi-èñ÷èñëåíèÿ.
Òàêèì îòíîøåíèåìýêâèâàëåíòíîñòè ìîæåò áûòü îòíîøåíèå áèñèìóëÿöèè,âåòâÿùåéñÿ áèñèìóëÿöèè, îòíîøåíèå ðàâåíñòâà ìíîæåñòâàâû÷èñëåíèé è äð.Äâà ïðîöåññà p1 è p2 íàçîâåì ∼= -òåñòîâî ýêâèâàëåíòíûìè ,åñëè äëÿ ëþáîãî ïðîöåññà q ñïðàâåäëèâî ñîîòíîøåíèåp1 k q ∼= p2 k q .Ñîäåðæàòåëüíûé ñìûñë òåñòîâîé ýêâèâàëåíòíîñòè òàêîâ:íèêàêîé âíåøíèé ïðîöåññ (ïðîòèâíèê) q íå ìîæåò, âñòóïàÿ âîâçàèìîäåéñòâèå ñ ïðîöåññàìè p1 è p2 , âûÿâèòü ðàçëè÷èÿìåæäó íèìè.Ïðèìåíåíèå spi-èñ÷èñëåíèÿ âêðèïòîàíàëèçåÏðåäïîëîæèì, ÷òî èìååòñÿ ïðîöåññ spi-èñ÷èñëåíèÿ System(x) ,â êîòîðîì èìÿ x èñïîëüçóåòñÿ â êà÷åñòâå ïàðàìåòðà (íàïðèìåð,ýòî ñîîáùåíèå, êîòîðîå äîëæíî áûòü îòïðàâëåíî îò îäíîãîïîäïðîöåññà äðóãîìó).Òîãäà ïðîöåññ System(x) íàçîâåì ∼= -ñòîéêèì (îòíîñèòåëüíîïàðàìåòðà x ), åñëè äëÿ ëþáîé ïàðû èìåí m1, m2 ïðîöåññûSystem(m1 ) è System(m2 ) ÿâëÿþòñÿ ∼= -òåñòîâîýêâèâàëåíòíûìè.Ñòîéêîñòü òàêîãî ðîäà îçíà÷àåò, ÷òî íèêàêîé ïðîòèâíèê íåñìîæåò, âñòóïèâ âî âçàèìîäåéñòâèå ñ ïðîöåññîì System(m) ,èçâëå÷ü íèêàêîé ñåìàíòè÷åñêîé (ñîäåðæàòåëüíîé) èíôîðìàöèèî çíà÷åíèè ïàðàìåòðà m , ñ êîòîðûì ðàáîòàåò ïðîöåññ.Ïðèìåíåíèå spi-èñ÷èñëåíèÿ âêðèïòîàíàëèçåÍàïðèìåð, ñèñòåìà âçàèìîäåéñòâóþùèõ ïðîöåññîâWeak(X ) : chh{(A, X )}K i.
nil k ch[y ]. y = {(A, X )}K . nilíå ÿâëÿåòñÿ ∼ -ñòîéêîé, ïîñêîëüêó äëÿ ïàðû èìåí m1, m2ñóùåñòâóåò òàêîé ïðîöåññAdvers : ch[z]. Z = {(A, m1)}K . success. nil,äëÿ êîòîðîãî ïàðàëëåëüíûå êîìïîçèöèèAdvers k Weak(m1) è Advers k Weak(m2)áèñèìóëÿöèîííî ýêâèâàëåíòíûìè, ïîñêîëüêóAdvers k Weak(m1) èìååò âû÷èñëåíèå, îêàí÷èâàþùååñÿâûïîëíåíèåì âíóòðåííåãî äåéñòâèÿ success ,Advers k Weak(m2) íå èìååò íè îäíîãî âû÷èñëåíèÿ, â êîòîðîìâûïîëíÿåòñÿ äåéñòâèå success .íå ÿâëÿþòñÿÏðèìåíåíèå spi-èñ÷èñëåíèÿ âêðèïòîàíàëèçåÀ ñèñòåìà âçàèìîäåéñòâóþùèõ ïðîöåññîâStrong(X ) :νK . chh{(A, X )}K i. nil k ch[y ]. y = {(A, X )}K . nil .
nil-ñòîéêîé.Íî äîêàçàòü ýòî íåïðîñòî. Ôàêòè÷åñêè, äëÿ ýòîãî íóæíîïðîâåñòè òðîéíîé ïåðåáîð 1) ïî ïàðàì èìåí m1, m2 ,2) ïî âñå ïðîöåññàì-ïðîòèâíèêàì Advers ,3) ïî âñåì âû÷èñëåíèÿì âçàèìîäåéñòâóþùèõ ñèñòåìAdvers k Strong(m) .È ýòî íå ìåíåå ïðîñòàÿ çàäà÷à, ÷åì ïîëó÷åíèå íèæíèõ îöåíîêñëîæíîñòè çàäà÷.ÿâëÿåòñÿ∼Ïðèìåíåíèå spi-èñ÷èñëåíèÿ âêðèïòîàíàëèçåÏðåäëîæåííîå îïðåäåëåíèå ñòîéêîñòè ìîäåëåéêðèïòîãðàôè÷åñêèõ ïðîòîêîëîâ ïîñðåäñòâîìîòíîøåíèÿ òåñòîâîé ýêâèâàëåíòíîñòè ïðèçâàíîãàðàíòèðîâàòü òðåáîâàíèÿ êîíôèäåíöèàëüíîñòèäàííûõ â âû÷èñëåíèÿõ ýòèõ ïðîòîêîëîâ.Çàäà÷à.À êàê ïðè ïîìîùè îòíîøåíèÿ òåñòîâîéýêâèâàëåíòíîñòè ñôîðìóëèðîâàòü òðåáîâàíèÿöåëîñòíîñòè ñîîáùåíèé äëÿ ìîäåëåéêðèïòîãðàôè÷åñêèõ ïðîòîêîëîâ.ÊÎÍÅÖ ËÅÊÖÈÈ 9.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
