-
Notifications
You must be signed in to change notification settings - Fork 0
/
rlwrap_cryptoverif_completion_with_comments.conf
161 lines (158 loc) · 2.34 KB
/
rlwrap_cryptoverif_completion_with_comments.conf
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
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
# from the help command (source code in instruct.ml)
remove_assign useless
remove_assign binder
remove_assign all
move all
move noarrayref
move random
move random_noarrayref
move assign
move binder
move array
SArename
global_dep_anal
crypto
simplify
simplify coll_elim
all_simplify
insert_event
insert
replace
merge_arrays
merge_branches
success
show_game
show_game occ
show_state
show_facts
start_from_other_end
out_game
out_state
out_facts
auto
set
allowed_collisions
undo
restart
quit
help
?
# from manual.pdf
remove_assign findcond
crypto variables terms
## insert <occ> …
new
if then
event
let in
find orfind
<-R
suchthat then
## allowed_collisions
size
small
passive
noninteractive
password
large
collision
# all parameters
true false
diffConstants
constantsNotTuple
expandAssignXY
minimalSimplifications
mergeBranches
mergeArrays
uniqueBranch
uniqueBranchReorganize
autoSARename
autoRemoveAssignFindCond
autoRemoveIfFindCond
autoMove
optimizeVars
interactiveMode
autoAdvice
noAdviceCrypto
noAdviceGlobalDepAnal
backtrackOnCrypto
simplifyAfterSARename
detectIncompatibleDefined
ignoreSmallTimes
maxIterSimplif
maxIterRemoveUselessAssign
maxAdvicePossibilitiesBeginning
maxAdvicePossibilitiesEnd
useKnownEqualitiesInCryptoTransform
minAutoCollElim
elsefindFactsInReplace
elsefindFactsInSuccess
elsefindFactsInSimplify
improvedFactCollection
useEqualitiesInSimplifyingFacts
maxReplaceDepth
maxAddFactDepth
maxTryNoVarDepth
casesInCorresp
debugInstruct
debugFindUnique
debugCryptotransf
debugElsefindFacts
debugSimplify
debugSimplifAddFacts
debugCorresp
# predefinend equiv statements for the crypto command
move_array
ind_cpa enc
ind_cpa enc
int_ctxt enc
ind_cca2 enc
int_ptxt enc
ind_cca2 enc
ind_cca2_after_int_ptxt enc
int_ptxt enc
int_ptxt_after_ind_cca2 enc
sprp enc
prp enc
icm enc
uf_cma mac
uf_cma_corrupt mac
suf_cma mac
suf_cma_corrupt mac
ind_cca2 enc
uf_cma sign
uf_cma_corrupt sign
suf_cma sign
suf_cma_corrupt sign
rom hash
rom hash
rom hash
rom hash
group_to_exp_strict exp
group_to_exp exp
exp_to_group exp
exp'_to_group exp
cdh exp
group_to_exp_strict exp
group_to_exp exp
exp_to_group exp
exp'_to_group exp
ddh exp
group_to_exp_strict exp
group_to_exp exp
exp_to_group exp
exp'_to_group exp
gdh exp
group_to_exp_strict exp
group_to_exp exp
exp_to_group exp
exp'_to_group exp
gdh exp
remove_invf f
ow f
remove_invf f
ow_rsr f
remove_invf f
pd_ow f
prf f
remove_xor xor