-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathproof200.mod
115 lines (106 loc) · 2.2 KB
/
proof200.mod
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
-- I) Base case
open INV
ops m221 m222 : -> Message2 .
op m30 : -> Message3 .
red inv200(init,m221,m222,m3) .
close
-- sdm1
open ISTEP
ops m221 m222 : -> Message2 .
op m30 : -> Message3 .
--
ops p10 q10 : -> Principal .
op d10 : -> Dompar .
op r10 : -> Random .
eq s' = sdm1(s,p10,q10,r10,d10) .
red istep200(m221,m222,m30) .
close
-- sdm2
open ISTEP
ops m221 m222 : -> Message2 .
op m30 : -> Message3 .
--
op m10 : -> Message1 .
ops p10 q10 : -> Principal .
op r10 : -> Random .
op d10 : -> Dompar .
eq s' = sdm2(s,p10,q10,r10,m10) .
red istep200(m221,m222,m30) .
close
-- sdm3
open ISTEP
ops m221 m222 : -> Message2 .
op m30 : -> Message3 .
--
op m10 : -> Message1 .
ops m2001 m2002 : -> Message2 .
ops p10 q10 : -> Principal .
eq s' = sdm3(s,p10,q10,m10,m2001,m2002) .
red istep200(m221,m222,m30) .
close
-- fkm11
open ISTEP
ops m221 m222 : -> Message2 .
op m30 : -> Message3 .
--
op c10 : -> Cipher1 .
ops p10 q10 : -> Principal .
eq s' = fkm11(s,p10,q10,c10) .
red istep200(m221,m222,m30) .
close
-- fkm12
open ISTEP
ops m221 m222 : -> Message2 .
op m30 : -> Message3 .
--
ops p10 q10 : -> Principal .
op r10 : -> Random .
op d10 : -> Dompar .
eq s' = fkm12(s,p10,q10,r10,d10) .
red istep200(m221,m222,m30) .
close
-- fkm21
open ISTEP
ops m221 m222 : -> Message2 .
op m30 : -> Message3 .
--
ops p10 q10 : -> Principal .
op e200 : -> Expo .
eq s' = fkm21(s,p10,q10,e200) .
red istep200(m221,m222,m30) .
close
-- fkm22
open ISTEP
ops m221 m222 : -> Message2 .
op m30 : -> Message3 .
--
ops p10 q10 : -> Principal .
ops r11 r12 : -> Random .
op d10 : -> Dompar .
eq s' = fkm22(s,p10,q10,r11,r12,d10) .
red istep200(m221,m222,m30) .
close
-- fkm31
open ISTEP
ops m221 m222 : -> Message2 .
op m30 : -> Message3 .
--
ops p10 q10 : -> Principal .
ops r11 r12 : -> Random .
op d10 : -> Dompar .
op c300 : -> Cipher3 .
eq s' = fkm31(s,p10,q10,c300) .
red istep200(m221,m222,m30) .
close
-- fkm32
open ISTEP
ops m221 m222 : -> Message2 .
op m30 : -> Message3 .
--
ops p10 q10 : -> Principal .
ops r11 : -> Random .
ops e10 e11 : -> Expo .
op d10 : -> Dompar .
eq s' = fkm32(s,p10,q10,r11,e10,e11,d10) .
red istep200(m221,m222,m30) .
close