-
Notifications
You must be signed in to change notification settings - Fork 3
/
Copy pathchangelog
100 lines (77 loc) · 4.08 KB
/
changelog
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
This file summarizes the most important changes between versions
of DeepSec.
Version 2.0.2 (23/07/2020)
- Fix several bugs (See Github Issue #67 to #71)
Version 2.0.1 (03/05/2020)
- For session equivalence queries, if the two processes are both strongly
determinate, deepsec execute the verification procedure for determinate pro-
cesses as session equivalence and trace equivalence coincide in this case.
Version 2.0.0 (01/05/2020)
- Official release
- Creation of opam package
Version 2.0.0 beta8 (26/04/2020)
- Add a display of the attack trace in the terminal when DeepSec is executed
with the option --trace
- Fix a bug when reconstructing the attack trace on equivalence between deter-
minate processes.
Version 2.0.0 beta7 (19/04/2020)
- Fix a bug in the constraint solving when working on deduction formula.
Version 2.0.0 beta6 (18/04/2020)
- Fix a bug in the constraint solving when a rewrite rule can be allow a deduction
fact to be removed from the incremental knowledge.
Version 2.0.0 beta5 (06/04/2020)
- Fix a bug in session equivalence when dealing with improper block. Would raise
an internal error.
- Fix a bug in determinate equivalence which would not display the proper attack
trace when the processes contain only trivial else branches.
Version 2.0.0 beta4 (24/02/2020)
- Fix a bug in the representation of formula on recipe.
Version 2.0.0 beta2 (29/01/2020)
- Fix a bug in session equivalence that prevented the function authorised block
to be applied correctly.
- Fix a bug when distributed computation is deactivated: The worker could send
progression status without an acknowledgement which would cause issue when
calling Unix.select in the local manager.
Version 2.0.0 beta1 (22/01/2020)
- Fix a bug in the Makefile for detecting the number of physical CPU
- Fix a bug that would raise an internal error when using !^1 in the input file
Version 2.0.0 beta (21/01/2020)
- The memory consumption of DeepSec has been reduced (up to 4 times less memory).
- Better integration with DeepSec UI Alpha RC3
- Fix many bugs
Version 2.0.0 alpha rc2 (14/01/2020)
- Does not return an internal error when an incorrect path of file is given
as argument. Returns a user error instead.
- Improved Makefile to handle the cases where Git Commit, Git Hash and detection
of physical core are not possible.
- [API] Improved parsing of recipe.
- [API] Allow deepsec_api to keep running even if its stdin and stdout are
destroyed.
- [API] List of privates names in process and frames are sent when receiving
commands for the simulators and display of traces.
- [API] Send a specific error message when there is a '%' in a recipe given by
a user.
Version 2.0.0 alpha rc (14/01/2020)
DeepSec 2.0.0 is a major rework of DeepSec. It is still a command-line tool
but it can also be used with the new user interface DeepSec UI. See
https://github.com/DeepSec-prover/deepsec_ui to download and install DeepSec UI 1.0.x.
Amongst the new features of both DeepSec and DeepSec UI:
- Improved efficiency when verifying queries.
- Support for "Eavesdrop", "Classic" and "Private" semantics (POST'17) for verifying
trace equivalence.
- Integration and improvements of session equivalence (CCS'19).
- Recording of the result of your runs that can be displayed in DeepSec UI.
- DeepSec UI supports all of DeepSec's abilities does but with a nice interface.
- Interactive display of attacks for violated queries.
- Attack and equivalence simulators in DeepSec UI for trace equivalence:
when a trace equivalence query holds, you can select a trace on any of
the two processes and request an equivalent trace; when violated there
is an attack trace on one of the processes, and you can select any trace
on the other process to see why they are not equivalent. Note that these
simulators only work with trace equivalence and not session equivalence.
Version 1.02 (16/08/2019)
- Introduction of equivalence by session
Version 1.01 (06/05/2019)
- Fixing a bug in Constraint_system.ml
Version 1.0 (19/12/2018)
- Initial release of DeepSeec