Я написал код Promela для проверки протокола Needham-Schroeder с использованием SPIN. После запуска случайного моделирования кода я получаю этот вывод:
0: proc - (:root:) creates proc 0 (:init:)
Starting PIni with pid 1
1: proc 0 (:init:) creates proc 1 (PIni)
0 :init ini run PIni(A,I,N
Starting PRes with pid 2
3: proc 0 (:init:) creates proc 2 (PRes)
0 :init ini run PRes(B,Nb)
Starting PI with pid 3
4: proc 0 (:init:) creates proc 3 (PI)
0 :init ini run PI()
1 PIni 62 else
1 PIni 63 1
1 PIni 64 ca!self,nonce,
3 PI 128 ca?,x1,x2,x3
1 PIni 64 values: 1!A,Na
3 PI 128 values: 1?0,Na
Process Statement PI(3):kNa PI(3):x1 PI(3):x2 PI(3):x3
3 PI 135 x3 = 0 1 0 0 I
3 PI 101 ca!B,gD,A,B 1 0 0 0
2 PRes 79 ca?eval(self), 1 0 0 0
3 PI 101 values: 1!B,gD 1 0 0 0
2 PRes 79 values: 1?B,gD 1 0 0 0
Process Statement PI(3):kNa PI(3):x1 PI(3):x2 PI(3):x3 PRes(2):g2 PRes(2):g3
2 PRes 80 g3==A)&&(self= 1 0 0 0 gD A
2 PRes 80 ResRunningAB = 1 0 0 0 gD A
Process Statement PI(3):kNa PI(3):x1 PI(3):x2 PI(3):x3 PRes(2):g2 PRes(2):g3 ResRunning
2 PRes 82 ca!self,g2,non 1 0 0 0 gD A 1
3 PI 128 ca?,x1,x2,x3 1 0 0 0 gD A 1
2 PRes 82 values: 1!B,gD 1 0 0 0 gD A 1
3 PI 128 values: 1?0,gD 1 0 0 0 gD A 1
3 PI 135 x3 = 0 1 0 0 A gD A 1
3 PI 113 ca!( (kNa) -> 1 0 0 0 gD A 1
1 PIni 68 ca?eval(self), 1 0 0 0 gD A 1
3 PI 113 values: 1!A,Na 1 0 0 0 gD A 1
1 PIni 68 values: 1?A,Na 1 0 0 0 gD A 1
Process Statement PI(3):kNa PI(3):x1 PI(3):x2 PI(3):x3 PIni(1):g1 PRes(2):g2 PRes(2):g3 ResRunning
1 PIni 69 else 1 0 0 0 Na gD A 1
1 PIni 69 1 1 0 0 0 Na gD A 1
1 PIni 71 cb!self,g1,par 1 0 0 0 Na gD A 1
3 PI 139 cb?,x1,x2 1 0 0 0 Na gD A 1
1 PIni 71 values: 2!A,Na 1 0 0 0 Na gD A 1
3 PI 139 values: 2?0,Na 1 0 0 0 Na gD A 1
3 PI 145 x2 = 0 1 0 I 0 Na gD A 1
timeout
#processes: 4
34: proc 3 (PI) needhamNew.pml:100 (state 81)
34: proc 2 (PRes) needhamNew.pml:86 (state 10)
34: proc 1 (PIni) needhamNew.pml:73 (state 18)
34: proc 0 (:init:) needhamNew.pml:58 (state 8)
4 processes created
Я вижу, что созданные процессы предназначены для Инициатора, Ответчика и Злоумышленника. Мне трудно понять, как именно это доказывает, что протокол Нидхема-Шредера может быть взломан, хотя я понимаю его теорию.
Может ли кто-нибудь понять этот вывод и, возможно, направить меня туда, где я должен искать? Если вы хотите просмотреть мой код Promela, сообщите мне об этом! Любые отзывы приветствуются!
