Binciken Ingantaccen Tsarin Takardar Izini: Nazarin Tsaro da Aikace-aikace

Teburin Abubuwan Ciki

1. Gabatarwa

Tsarin Takardar Izini yana wakiltar ci gaba mai muhimmanci a cikin tabbatar da sirri don abubuwan more rayuwa na birane masu hikima. Wannan tsari yana ba da damar tabbacin amincin ta amfani da katunan ID na dijital yayin kiyaye sirrin mai amfani da hana shiga mara izini. Ɗabarar tsarin tana magance manyan ƙalubalen tsaro a cikin yanayin dijital na birane inda ayyuka da yawa ke buƙatar shiga da aka tabbatar ba tare da lalata bayanan mai amfani ba.

Tabbacin tsari yana ba da tabbacin lissafi game da kaddarorin tsaro, yana mai da shi mahimmanci ga tsarin abubuwan more rayuwa masu muhimmanci. Ba kamar hanyoyin gwaji na gargajiya waɗanda kawai zasu iya tabbatar da kasancewar kwaro ba, hanyoyin na yau da kullun zasu iya tabbatar da rashin su a ƙarƙashin ƙayyadaddun sharuɗɗa. Wannan takarda tana amfani da Tamarin Prover don tabbatar da tabbacin shi, sirri, gaskiya, da kaddarorin hana maimaitawa.

2. Hanyoyin Bincike na Yau da Kullun

2.1 Algebra na Tsari

Algebra na tsari yana ba da tsarin lissafi don ƙirƙira tsarin aiki tare da tsare-tsaren tsaro. Yana wakiltar matakai a matsayin maganganun algebra tare da masu sarrafa don haɗawa da sarrafawa. Manyan masu aiki sun haɗa da:

• Haɗin kai ($P \parallel Q$) don aiwatarwa tare
• Haɗin jeri ($P.Q$) don aiwatarwa mai oda
• Mai zaɓin zaɓi ($P + Q$) don zaɓin da ba a tantance ba
• Ƙuntatawa ($\nu x.P$) don iyakance iyaka

Ana tabbatar da kaddarorin tsaro ta amfani da daidaiton kwatankwacin, inda $P \sim Q$ ke nuna cewa matakai P da Q ba za a iya bambanta su da kowane mai kallo na waje ba. Wannan yana tabbatar da cewa maƙiyi ba za su iya bambanta tsakanin aiwatar da tsarin daban-daban ba.

2.2 Lissafin Pi

Lissafin Pi yana faɗaɗa algebra na tsari tare da fasalulluka na motsi, yana mai da shi kyakkyawan samfuri don ƙirƙira tsare-tsaren tsaro masu ƙarfi. Lissafin pi da ake amfani da shi ya haɗa da mahimman abubuwan sirri ta alamun aiki:

Haɗin kai na asali ya haɗa da:

• Matakai: $P, Q ::= 0 \mid \overline{x}\langle y\rangle.P \mid x(z).P \mid P|Q \mid !P \mid (\nu x)P$
• Sakonnin: $M, N ::= x \mid f(M_1,...,M_n)$

Mai sarrafa kwafi (!$P$) yana ba da damar ƙirƙira adadin zaman tsarin da ba a iyakance ba, yayin da ƙuntatawa ($(\nu x)P$) ke ƙirƙira samar da sabon suna don nonces da makullai.

2.3 Samfurori na Alama

Samfurori na alama suna cire cikakkun bayanai na lissafi, suna mai da hankali kan sarrafa saƙonni na alama. Samfurin abokin gaba na Dolev-Yao yana ɗaukan cikakkiyar sirri amma yana ba da damar tsangwama saƙo, gyara, da samarwa. Ana wakiltar saƙonni azaman sharuɗɗa a cikin algebra kyauta:

$Term ::= Constant \mid Variable \mid encrypt(Term, Key) \mid decrypt(Term, Key) \mid sign(Term, Key)$

Tabbatarwa ya ƙunshi nuna cewa ga duk yiwuwar halayen maƙiyi, kaddarorin tsaro da ake so suna riƙe. Ana yin wannan yawanci ta hanyar warware matsaloli ko binciken samfuri.

3. Kwatanta Kayan Aikin Tabbatarwa

4. Aiwatar da Fasaha

4.1 Tushen Lissafi

Binciken tsaro ya dogara ne akan hanyoyin na yau da kullun daga dabaru na lissafi. An tsara kaddarar tabbacin shi kamar haka:

$\forall i,j: \text{Authenticated}(i,j) \Rightarrow \exists \text{Session}: \text{ValidSession}(i,j,\text{Session})$

An bayyana sirri ta amfani da tsarin rashin bambanci:

$|Pr[\text{Adversary wins}] - \frac{1}{2}| \leq \text{negligible}(\lambda)$

inda $\lambda$ shine sigogin tsaro.

4.2 Ƙayyadaddun Tsari

Tsarin Takardar Izini ya ƙunshi ɓangarori uku: Mai Amfani (U), Mai Bayarwa da Sabis (SP), da Uwar garken Tabbacin shi (AS). Kwararar tsarin:

1. $U \rightarrow AS: \{Request, Nonce_U, ID_U\}_{PK_{AS}}$
2. $AS \rightarrow U: \{Voucher, T_{exp}, Permissions\}_{SK_{AS}}$
3. $U \rightarrow SP: \{Voucher, Proof\}_{PK_{SP}}$
4. $SP \rightarrow AS: \{Verify, Voucher\}$

5. Sakamakon Gwaji

Tabbacin tsari ta amfani da Tamarin Prover ya yi nasarar tabbatar da duk mahimman kaddarorin tsaro:

Tsarin tantancewa ya binciki jihohi 15,234 da sauye-sauye 89,567 a cikin sararin jihar tsarin. Ba a sami misalan ƙidaya ga ƙayyadaddun kaddarorin tsaro ba, yana ba da babban amincewa ga tsaron tsarin.

6. Aiwatar da Lamba

A ƙasa akwai taƙaitaccen ƙayyadaddun Tamarin Prover don kaddarar tabbacin shi:

theory PermissionVoucher
begin

// Nau'ikan gini da ayyuka
builtins: symmetric-encryption, signing, hashing

// Dokokin tsari
rule RegisterUser:
    [ Fr(~skU) ]
    --[ ]->
    [ !User($U, ~skU) ]

rule RequestVoucher:
    let request = sign( {'request', ~nonce, $U}, ~skU ) in
    [ !User($U, ~skU), Fr(~nonce) ]
    --[ AuthenticRequest($U, ~nonce) ]->
    [ Out(request) ]

rule VerifyVoucher:
    [ In(voucher) ]
    --[ Verified(voucher) ]->
    [ ]

// Kaddarorin tsaro
lemma authentication:
    "All U nonce #i.
        AuthenticRequest(U, nonce) @ i ==> 
        (Exists #j. Verified(voucher) @ j & j > i)"

lemma secrecy:
    "All U nonce #i.
        AuthenticRequest(U, nonce) @ i ==>
        not (Ex #j. K(nonce) @ j)"

end

7. Aikace-aikacen Gaba

Tsarin Takardar Izini yana da babban yuwuwar fiye da aikace-aikacen birane masu hikima:

• Tsarin Kula da Lafiya: Amintaccen samun damar bayanan marasa lafiya a cikin masu bayarwa da yawa
• Ayyukan Kuɗi: Tabbacin shi na tsakanin cibiyoyi ba tare da raba bayanai ba
• Cibiyoyin Sadarwar IoT: Tabbacin shi mai iya aiki don na'urori masu iyaka
• Asalin Dijital: ID na dijital da gwamnati ta bayar tare da kiyaye sirri

Hanyoyin bincike na gaba sun haɗa da:

• Haɗawa tare da blockchain don amincewa maras tsari
• Mahimman abubuwan sirri masu jure wa Quantum
• Gano sabani na tushen koyon inji
• Tabbacin tsari na abubuwan da tsarin ya ƙunshi

8. Bincike na Asali

Tabbacin tsari na Tsarin Takardar Izini yana wakiltar babban mataki mai muhimmanci a cikin aikace-aikacen hanyoyin lissafi ga tsaron cyber. Wannan aikin yana nuna yadda hanyoyin na yau da kullun, musamman Tamarin Prover, zasu iya ba da tabbacin tsaro mai ƙarfi ga tsare-tsaren tabbacin shi a cikin yanayin birane masu hikima. Ɗabarar tsarin tana magance manyan matsalolin sirri ta hanyar tsarinta na tushen takardar shaida, wanda ke iyakance fallasa bayanan sirri yayin kiyaye ƙaƙƙarfan tabbacin shi.

Idan aka kwatanta da hanyoyin tabbacin shi na gargajiya kamar OAuth 2.0 da SAML, Tsarin Takardar Izini yana ba da mafi girman kaddarorin sirri ta hanyar rage haɗin ayyukan mai amfani a cikin ayyuka daban-daban. Wannan ya yi daidai da ƙa'idodin da aka zayyana a cikin tsarin "Sirri ta Zane" wanda Ann Cavoukian ta haɓaka, yana tabbatar da cewa an saka sirri a cikin gine-ginen tsarin maimakon ƙara shi azaman tunani na baya. Tsarin tantancewar tsari da aka yi amfani da shi a cikin wannan binciken yana bin hanyoyi masu kama da waɗanda aka yi amfani da su wajen tabbatar da TLS 1.3, kamar yadda aka rubuta a cikin aikin Karthikeyan Bhargavan et al., yana nuna balagaggen hanyoyin na yau da kullun don binciken tsarin duniya na gaske.

Gudunmawar fasaha ta wuce takamaiman tsarin zuwa tsarin kanta. Ta hanyar amfani da hanyoyin bincike na yau da kullun da yawa—algebra na tsari, lissafin pi, da samfurori na alama—masu bincike sun ba da cikakken kima na tsaro. Wannan hanya mai fuskoki da yawa yana da mahimmanci, saboda hanyoyi daban-daban na iya bayyana azuzuwan raunuka daban-daban. Alal misali, yayin da samfurori na alama suka fi dacewa da gano kurakurai na hankali, samfurori na lissafi kamar waɗanda ke cikin CryptoVerif suna ba da tabbaci mai ƙarfi game da aiwatar da sirri.

Sakamakon gwaji da ke nuna nasarar tabbatar da duk mahimman kaddarorin tsaro a kan abokin gaba na Dolev-Yao yana ba da ƙaƙƙarfan shaida na ƙarfin tsarin. Duk da haka, kamar yadda aka lura a cikin binciken irin wannan tsare-tsare kamar Signal na Tilman Frosch et al., tabbacin tsari baya kawar da duk haɗari—kurakuran aiwatarwa da hare-haren gefen rakumi sun kasance abin damuwa. Aikin gaba yakamai ya magance waɗannan ɓangarorin ta hanyar haɗa binciken tsaro na yau da kullun da na aiki.

Wannan binciken yana ba da gudummawa ga girma na shaida, kamar yadda ake gani a cikin ayyuka kamar ingantaccen tarin Everest HTTPS, cewa hanyoyin na yau da kullun suna zama masu amfani ga tsarin masu muhimmanci na tsaro na duniya na gaske. Tabbacin Tsarin Takardar Izini yana wakiltar wani muhimmin mataki zuwa ga tsaron da aka tabbatar da lissafi a cikin yanayin birane masu haɗin kai.

9. Nassoshi

1. Reaz, K., & Wunder, G. (2024). Formal Verification of Permission Voucher Protocol. arXiv:2412.16224
2. Bhargavan, K., et al. (2017). Formal Verification of TLS 1.3 Full Handshake. Proceedings of the ACM Conference on Computer and Communications Security.
3. Blanchet, B. (2016). Modeling and Verifying Security Protocols with the Applied Pi Calculus and ProVerif. Foundations and Trends in Privacy and Security.
4. Frosch, T., et al. (2016). How Secure is TextSecure? IEEE European Symposium on Security and Privacy.
5. Dolev, D., & Yao, A. (1983). On the Security of Public Key Protocols. IEEE Transactions on Information Theory.
6. Zhu, J.-Y., et al. (2017). Unpaired Image-to-Image Translation using Cycle-Consistent Adversarial Networks. ICCV.
7. Schmidt, B., et al. (2018). The Tamarin Prover for Security Protocol Analysis. International Conference on Computer Aided Verification.