9. Особенности мобильной связи. π-исчисление мобильных процессов. Синтаксис π-исчисления. Операционная семантика π-исчисления (1265180), страница 2
Текст из файла (страница 2)
nil k UhV i. nil↓R νU [S]. nil k UhV i. nilUhV i ↓ RCZeronil k nil ≡ nilπ -èñ÷èñëåíèåïðîöåññîâ: ñåìàíòèêàÒàê æå, êàê â àëãåáðå ïðîöåññîâ, äëÿ êàæäîãî ïðîöåññà pπ -èñ÷èñëåíèÿ ìîæíî îïðåäåëèòü äåðåâî âû÷èñëåíèé Γ(p) .Èñïîëüçóÿ äåðåâüÿ âû÷èñëåíèé, íà ìíîæåñòâå ïðîöåññîâ Procππ -èñ÷èñëåíèÿ ìîæíî îïðåäåëèòü îòíîøåíèå áèñèìóëÿöèè ∼ èðåøàòü ñ ïîìîùüþ ýòîãî îòíîøåíèÿ çàäà÷è ñèíòåçà è àíàëèçàìîáèëüíûõ ðàñïðåäåëåííûõ ñèñòåì.Îäíàêî π-èñ÷èñëåíèå îòêðûâàåò èíòåðåñíóþ âîçìîæíîñòüïðèìåíåíèÿ àëãåáðû ïðîöåññîâ äëÿ îïèñàíèÿ è èññëåäîâàíèÿêðèïòîãðàôè÷åñêèõ ïðîòîêîëîâ.Ðàññìîòðèì îäèí èç êðèïòîãðàôè÷åñêèõ ïðîòîêîëîâ, ÷òîáûîöåíèòü, êàê íóæíî ðàñøèðèòü âûðàæåíèÿ π-èñ÷èñëåíèÿ,÷òîáû àäåêâàòíî âûðàçèòü òå äåéñòâèÿ, êîòîðûå âûïîëÿíþòó÷àñòíèêè ïðîòîêîëà.Êðèïòîãðàôè÷åñêèå ïðîòîêîëûÑèììåòðè÷íûé ïðîòîêîë ðàñïðåäåëåíèÿ êëþ÷åéYahalom (àëìàç).MAlice?BobÊðèïòîãðàôè÷åñêèå ïðîòîêîëûÑèììåòðè÷íûé ïðîòîêîë ðàñïðåäåëåíèÿ êëþ÷åéYahalom (àëìàç).M KATAliceKAT , KBTTrentBobKBTÊðèïòîãðàôè÷åñêèå ïðîòîêîëûÑèììåòðè÷íûé ïðîòîêîë ðàñïðåäåëåíèÿ êëþ÷åéYahalom (àëìàç).M KATAliceRA(A, RA )Trent?BobKBTKAT , KBTÊðèïòîãðàôè÷åñêèå ïðîòîêîëûÑèììåòðè÷íûé ïðîòîêîë ðàñïðåäåëåíèÿ êëþ÷åéYahalom (àëìàç).M KATRAAliceKAT , KBTTrentBobKBT RAÊðèïòîãðàôè÷åñêèå ïðîòîêîëûÑèììåòðè÷íûé ïðîòîêîë ðàñïðåäåëåíèÿ êëþ÷åéYahalom (àëìàç).M KATAliceRAKAT , KBTTrent* Bob (B, EKBT (A, RA , RB ))KBT RA RBÊðèïòîãðàôè÷åñêèå ïðîòîêîëûÑèììåòðè÷íûé ïðîòîêîë ðàñïðåäåëåíèÿ êëþ÷åéYahalom (àëìàç).M KATAliceRAKAT , KBTTrentBobKBT RA RBA,BRA , RBÊðèïòîãðàôè÷åñêèå ïðîòîêîëûÑèììåòðè÷íûé ïðîòîêîë ðàñïðåäåëåíèÿ êëþ÷åéYahalom (àëìàç).M KATAliceRAHYHHHHEKAT (B, K, RA , RB )HHHHKAT , KBTHHTrentBobKBT RA RBÊðèïòîãðàôè÷åñêèå ïðîòîêîëûÑèììåòðè÷íûé ïðîòîêîë ðàñïðåäåëåíèÿ êëþ÷åéYahalom (àëìàç).M KAT RA RB , KAliceKAT , KBTTrentBobKBT RA RBÊðèïòîãðàôè÷åñêèå ïðîòîêîëûÑèììåòðè÷íûé ïðîòîêîë ðàñïðåäåëåíèÿ êëþ÷åéYahalom (àëìàç).M KAT RA RB , KAliceHYHHHHEKBT (A, K)HHHHHHKAT , KBTTrentBobKBT RA RBÊðèïòîãðàôè÷åñêèå ïðîòîêîëûÑèììåòðè÷íûé ïðîòîêîë ðàñïðåäåëåíèÿ êëþ÷åéYahalom (àëìàç).M KAT RA RB , KAliceEKBT (A, K)Trent?BobKAT , KBTKBT RA RBÊðèïòîãðàôè÷åñêèå ïðîòîêîëûÑèììåòðè÷íûé ïðîòîêîë ðàñïðåäåëåíèÿ êëþ÷åéYahalom (àëìàç).M KAT RA RB , KAliceKAT , KBTTrentBobKBT RA RBKÊðèïòîãðàôè÷åñêèå ïðîòîêîëûÑèììåòðè÷íûé ïðîòîêîë ðàñïðåäåëåíèÿ êëþ÷åéYahalom (àëìàç).M KAT RA RB , KAliceEK (RB , M)Trent?BobKAT , KBTKBT RA RBKÊðèïòîãðàôè÷åñêèå ïðîòîêîëûÑèììåòðè÷íûé ïðîòîêîë ðàñïðåäåëåíèÿ êëþ÷åéYahalom (àëìàç).M KAT RA RB , KAliceKAT , KBTTrentBobKBT RA RBKMÊðèïòîãðàôè÷åñêèå ïðîòîêîëûÈç îïèñàíèÿ ïðîòîêîëà âèäíî, ÷òî äëÿ ìîäåëèðîâàíèÿ åãîïîâåäåíèÿ ïðè ïîìîùè âûðàæåíèé π-èñ÷èñëåíèÿ íóæíî èìåòüâîçìîæíîñòüI îïåðèðîâàòü íå òîëüêî ñ èìåíàìè, íî è ñî ñëîæíûìèòåðìàìè, ïðåäñòàâëÿþùèìè ðåçóëüòàò âûïîëíåíèÿêðèïòîãðàôè÷åñêèõ ïðîöåäóð (øèôðîâàíèÿ, ýëåêòðîííîéïîäïèñè, õåøèðîâàíèÿ è äð.);I ïåðåñûëàòü ïî êàíàëàì ñâÿçè íå òîëüêî îòäåëüíûå èìåíà,íî òàêæå è ñïèñêè èìåí è òåðìîâ;I êîððåêòíî âûïîëíÿòü âçàèìíî-îáðàòíûå äåéñòâèÿ(íàïðèìåð, øèôðîâàíèå è ðàñøèôðîâàíèå ñîîáùåíèé);I ñðàâíèâàòü äðóã ñ äðóãîì èìåíà è òåðìû.spi-èñ÷èñëåíèå: ñèíòàêñèñ è ñåìàíòèêàÄëÿ òîãî, ÷òîáû ïðèäàòü π-èñ÷èñëåíèþ áîëüøóþâûðàçèòåëüíóþ ñèëó, íàðÿäó ñ èìåíàìè â îáîðîò ââîäÿòñÿ èñëîæíûå òåðìû ñëåäóþùåãî âèäà:1.
(t1, t2) òåðì-ïàðà; ïðè ïîìîùè ýòîãî âèäà òåðìîâ ìîæíîñòðîèòü ñïèñêè;2. 0 êîíñòàíòà 0;3. succ(t) òåðì âû÷èñëåíèÿ íàòóðàëüíîãî ÷èñëà,ñëåäóþùåãî ïî ïîðÿäêó çà òåðìîì t ;4. {t1}t òåðì øèôðîâàíèÿ òåðìà t1 íà ñåêðåòíîìêëþ÷å-òåðìå t2 ;Ìîæíî òàæå ââîäèòü è äðóãèå êðèïòîãðàôè÷åñêèå ïðèìèòèâû øèôðîâàíèÿ íà îòêðûòîì êëþ÷å, ýëåêòðîííîé ïîäïèñè,õåøèðîâàíÿè, è äð.Ìíîæåñòâî âñåõ òåðìîâ îáîçíà÷èì çàïèñüþ Term .2spi-èñ÷èñëåíèå: ñèíòàêñèñ è ñåìàíòèêàÊ ìíîæåñòâó äåéñòâèé Act äîáàâëåí íîâûé âèääåéñòâèé:t1 = t2 óíèôèöèðîâàòü òåðìû t1 è t2 ;Ñåìàíòèêà ýòîãî âèäà äåéñòâèé îïðåäåëÿåòñÿñëåäóþùèì ïðàâèëîì âû÷èñëåíèé(t1 , t2 )R = : tθ1 ∈= tÍÎÓïðè óñëîâèè, ÷òî θ 2 .
p −→ pθïðàâèëüíàÿ ïîäñòàíîâêàäëÿ ïðîöåññà pÏðèìåðÏðîòîêîë ðàñïðåäåëåíèÿ êëþ÷åé YahalomÏðîöåññ Alice(a, m, ab, at, kAT ) :νr . abh(a, r )i. at[X1 ]. X1 = {(b, K , r , N)}kAT . at(X2 ). abhX2 i. abh{m, N}K iÏðîöåññ Bob(a, ab, bt, kBT ) :ab[Y1 ].Y1 = (U, V ). νs. bth(b, {(U, V , s)}kBT )i. ab[Y2 ].Y2 = (U, L). ab[Y3 ]. Y3 = {(M, s)}LÏðîöåññ Trent(a, b, ab, bt, kAT , kBT ) :bt[Z1 ]. Z1 = (b, {a, R1 , R2 }kBT ). ν`. ath{(b, `, R1 , R2 )}kAT i. ath{(a, `)}kBT iÏðîöåññ System(a, b, ab, bt, m) : :νk1 .
νk2 . Alice(a, m, ab, at, k1 ) k Bob(ab, bt, k2 ) k Trent(bt, at, k1 , k2 )ÏðèìåðÂû÷èñëåíèå ïðîòîêîëà Yahalomνx. νy .νr . abh(a, r )i. at[X1 ]. X1 = {(b, K , r , N)}x .at(X2 ). abhX2 i. abh{m, N}K ikab[Y1 ].Y1 = (U, V ). νs. bth(b, {(U, V , s)}y )i. ab[Y2 ].Y2 = (U, L). ab[Y3 ]. Y3 = {(M, s)}Lkbt[Z1 ]. Z1 = (b, {a, R1 , R2 }y ).ν`. ath{(b, `, R1 , R2 )}x i. ath{(a, `)}y iÏðèìåðÂû÷èñëåíèå ïðîòîêîëà Yahalomνx.
νy .νr . abh(a, r )i. at[X1 ]. X1 = {(b, K , r , N)}x .at(X2 ). abhX2 i. abh{m, N}K ikab[Y1 ].Y1 = (U, V ). νs. bth(b, {(U, V , s)}y )i. ab[Y2 ].Y2 = (U, L). ab[Y3 ]. Y3 = {(M, s)}Lkbt[Z1 ]. Z1 = (b, {a, R1 , R2 }y ).ν`. ath{(b, `, R1 , R2 )}x i. ath{(a, `)}y iÏðèìåðÂû÷èñëåíèå ïðîòîêîëà Yahalomνr . abh(a, r )i. at[X1 ]. X1 = {(b, K , r , N)}x .{x/k1 , y /k2 }at(X2 ). abhX2 i. abh{m, N}K ikab[Y1 ].Y1 = (U, V ).
νs. bth(b, {(U, V , s)}y )i. ab[Y2 ].Y2 = (U, L). ab[Y3 ]. Y3 = {(M, s)}L{x/k1 , y /k2 }kbt[Z1 ]. Z1 = (b, {a, R1 , R2 }y ).{x/k1 , y /k2 }ν`. ath{(b, `, R1 , R2 )}x i. ath{(a, `)}y iÏðèìåðÂû÷èñëåíèå ïðîòîêîëà Yahalomνr . abh(a, r )i. at[X1 ]. X1 = {(b, K , r , N)}k1 .at(X2 ). abhX2 i. abh{m, N}K ikab[Y1 ].Y1 = (U, V ). νs.
bth{(U, V , s)}k2 i. ab[Y2 ].Y2 = (U, L). ab[Y3 ]. Y3 = {(M, s)}Lkbt[Z1 ]. Z1 = (b, {a, R1 , R2 }k2 ).ν`. ath{(b, `, R1 , R2 )}k1 i. ath{(a, `)}k2 iÏðèìåðÂû÷èñëåíèå ïðîòîêîëà Yahalomνr . abh(a, r )i. at[X1 ]. X1 = {(b, K , r , N)}k1 .at(X2 ). abhX2 i. abh{m, N}K ikab[Y1 ].Y1 = (U, V ). νs. bth{(U, V , s)}k2 i. ab[Y2 ].Y2 = (U, L). ab[Y3 ]. Y3 = {(M, s)}Lkbt[Z1 ]. Z1 = (b, {a, R1 , R2 }k2 ).ν`.
ath{(b, `, R1 , R2 )}k1 i. ath{(a, `)}k2 iÏðèìåðÂû÷èñëåíèå ïðîòîêîëà Yahalomabh(a, r )i. at[X1 ]. X1 = {(b, K , r , N)}k1 .{r /r1 }at(X2 ). abhX2 i. abh{m, N}K ikab[Y1 ].Y1 = (U, V ). νs. bth{(U, V , s)}k2 i. ab[Y2 ].Y2 = (U, L). ab[Y3 ]. Y3 = {(M, s)}Lkbt[Z1 ]. Z1 = (b, {a, R1 , R2 }k2 ).ν`.
ath{(b, `, R1 , R2 )}k1 i. ath{(a, `)}k2 iÏðèìåðÂû÷èñëåíèå ïðîòîêîëà Yahalomabh(a, r1 )i. at[X1 ]. X1 = {(b, K , r1 , N)}k1 .at(X2 ). abhX2 i. abh{m, N}K ikab[Y1 ].Y1 = (U, V ). νs. bth{(U, V , s)}k2 i. ab[Y2 ].Y2 = (U, L). ab[Y3 ]. Y3 = {(M, s)}Lkbt[Z1 ]. Z1 = (b, {a, R1 , R2 }k2 ).ν`. ath{(b, `, R1 , R2 )}k1 i. ath{(a, `)}k2 iÏðèìåðÂû÷èñëåíèå ïðîòîêîëà Yahalomabh(a, r1 )i. at[X1 ]. X1 = {(b, K , r1 , N)}k1 .at(X2 ).
abhX2 i. abh{m, N}K ikab[Y1 ]. Y1 = (U, V ). νs. bth(b, {(U, V , s)}k2 )i. ab[Y2 ].Y2 = (U, L). ab[Y3 ]. Y3 = {(M, s)}Lkbt[Z1 ]. Z1 = (b, {a, R1 , R2 }k2 ).ν`. ath{(b, `, R1 , R2 )}k1 i. ath{(a, `)}k2 iÏðèìåðÂû÷èñëåíèå ïðîòîêîëà Yahalomabh(a, r1 )i. at[X1 ]. X1 = {(b, K , r1 , N)}k1 .at(X2 ).
abhX2 i. abh{m, N}K ikab[Y1 ]. Y1 = (U, V ). νs. bth(b, {(U, V , s)}k2 )i. ab[Y2 ].Y2 = (U, L). ab[Y3 ]. Y3 = {(M, s)}Lkbt[Z1 ]. Z1 = (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 ikY1 = (U, V ). νs. bth(b, {(U, V , s)}k2 )i. ab[Y2 ].Y2 = (U, L).
ab[Y3 ]. Y3 = {(M, s)}L{Y1 /(a, r1 )}kbt[Z1 ]. Z1 = (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 ik(a, r1 ) = (U, V ). νs. bth(b, {(U, V , s)}k2 )i.
ab[Y2 ].Y2 = (U, L). ab[Y3 ]. Y3 = {(M, s)}Lkbt[Z1 ]. Z1 = (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 ik(a, r1 ) = (U, V ). νs. bth(b, {(U, V , s)}k2 )i. ab[Y2 ].Y2 = (U, L). ab[Y3 ]. Y3 = {(M, s)}Lkbt[Z1 ].
Z1 = (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 ikνs. bth(b, {(U, V , s)}k2 )i. ab[Y2 ].Y2 = (U, L). ab[Y3 ]. Y3 = {(M, s)}L{U/a, V /r1 }kbt[Z1 ]. Z1 = (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 ikνs. bth{(a, r1 , s)}k2 i. ab[Y2 ].Y2 = (U, L). ab[Y3 ]. Y3 = {(M, s)}Lkbt[Z1 ]. Z1 = (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 ikνs. bth(b, {(a, r1 , s)}k2 )i. ab[Y2 ].Y2 = (U, L). ab[Y3 ]. Y3 = {(M, s)}Lkbt[Z1 ]. Z1 = (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 ikνs. bth{(a, r1 , s)}k2 i. ab[Y2 ].Y2 = (U, L). ab[Y3 ]. Y3 = {(M, s)}L{s/r2 }kbt[Z1 ]. Z1 = (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 )}LkZ1 = (b, {a, R1 , R2 }k2 ).{Z1 /(b, {a, r1 , r2 }k2 )}ν`. ath{(b, `, R1 , R2 )}k1 i. ath{(a, `)}k2 iÏðèìåðÂû÷èñëåíèå ïðîòîêîëà Yahalomat[X1 ].