UKano v0.5

UKano v0.5 packaged with Proverif v1.97 enhanced for handling extended diff-equivalence (see [HBD19]).

Improvements from UKano v0.4 (based on the new revision of [HBD19]):

• fix a bug that impacted sanity checks generation
• improve user messages
• additional and improved Tamarin models (see models)
• new toy example.

[HBD19]: L. Hirschi, D. Baelde, S. Delaune.
A method for unbounded verication of privacy-type properties.
Will appear in the Journal of Computer Security.
A copy can be found on ARXIV.

UKano v0.4

UKano v0.4 packaged with Proverif v1.97 enhanced for handling extended diff-equivalence (see [HBD18]).

Improvements from UKano v0.3 (based on the new revision of [HBD18]):

• add a different modeling of DAA sign and a different modeling of DAA-abstract sign.

[HBD18]: L. Hirschi, D. Baelde and S. Delaune.
A method for unbounded verification of privacy-type properties (journal paper under submission).
A copy can be found on ARXIV.

UKano v0.3

UKano v0.3 packaged with Proverif v1.97 enhanced for handling extended diff-equivalence (see [HBD17]).

Improvements from UKano v0.2 (based on new theoretical developments from [HBD17]):

• The class of allowed idealizations has been extended
• Frame Opacity is checked by using new encodings [HBD17] yieldings far better performance and allowing to capture the new class of idealizations
• The latter has been made possible by enhancing ProVerif 1.97 for handling extended diff-equivalence [HBD17]
• UKano now automatically generates sanity checks that verify the full executability of the protocol given as input
• New heuristics naming consistent with [HBD17]
• Case studies and benchmarks have been updated accordingly (better performance and less manual efforts are needed).

Fix various bugs w.r.t. idealization conformity check and heuristics for computing idealizations.

[HBD17]: L. Hirschi, D. Baelde and S. Delaune.
A method for unbounded verification of privacy-type properties (journal paper under submission).
A copy is available at http://www.lsv.fr/~hirschi/pdfs/UK_journal.pdf.

UKano v0.2

UKano v0.2 packaged with ProVerif v1.92.

Improvements from UKano v0.1 (based on new theoretical developments from [H17]):

• Detects whether the input protocol is in the shared case (i.e., some identity names are shared by the two roles) or not and adapt well-authentication verification accordingly.
• Verifies that guessed idealizations and idealizations given by the user are conform w.r.t. our generic definition [H17].
• Better heuristics to guess idealization that can be modified using options (more details in the corresponding section from the manual).
• UKano is now standalone and calls an executable proverif, parses its output and concludes accordingly.
• scope of protocols UKano can deal with is much larger. See the list of case studies in the corresponding section from the manual.

[H17]: L. Hirschi. PhD Thesis. Automated Verification of Privacy in Security Protocols: Back and Forth Between Theory & Practice. A copy will soon be distributed at http://projects.lsv.ens-cachan.fr/ukano/.

UKano v0.1

UKano v0.1 based on ProVerif 1.96.

UKano as distributed for the paper [HBD16]. It only deals with the shared case (i.e., some identity names are shared by the two roles) and only deals with a simple heuristics to guess idealization as described in [HBD16].

[HBD16]: L. Hirschi, D. Baelde and S. Delaune. A Method for Verifying Privacy-Type Properties : The Unbounded Case. In IEEE Symposium on Security and Privacy (Oakland), 2016. To appear. A copy can be found at http://projects.lsv.ens-cachan.fr/ukano/.