From 734e2e3363e47b6d8fc4b24f396d656488b2925a Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Robert=20K=C3=BCnnemann?= Date: Tue, 14 Jan 2025 20:51:24 +0100 Subject: [PATCH 1/3] Nix files (first attempt) --- .gitignore | 3 + .../Basic-access-control/BAC-2sessions.dps | 3 +- Makefile | 2 +- flake.lock | 207 ++++++++++++++++++ flake.nix | 26 +++ 5 files changed, 239 insertions(+), 2 deletions(-) create mode 100644 flake.lock create mode 100644 flake.nix diff --git a/.gitignore b/.gitignore index 3cd044d..125afb5 100644 --- a/.gitignore +++ b/.gitignore @@ -67,3 +67,6 @@ manager_deepsec /Examples/session_equivalence/tests/scratch.dps /documentation/files/* !/documentation/files/.content + +.envrc +.direnv diff --git a/Examples/trace_equivalence/Electronic_passport/Basic-access-control/BAC-2sessions.dps b/Examples/trace_equivalence/Electronic_passport/Basic-access-control/BAC-2sessions.dps index 2327475..7d2e1a1 100644 --- a/Examples/trace_equivalence/Electronic_passport/Basic-access-control/BAC-2sessions.dps +++ b/Examples/trace_equivalence/Electronic_passport/Basic-access-control/BAC-2sessions.dps @@ -5,6 +5,7 @@ fun mac/2. free c. free Error_6300. +free Error_6A80. free get_challenge. fun senc/2. @@ -40,7 +41,7 @@ let passport(k_e,k_m) = new k_t; let z = senc((n_t,xn_r,k_t),k_e) in out(c,(z,mac(z,k_m))) - ) else out(c,Error_6300) + ) else out(c,Error_6A80) else out(c,Error_6300) else out(c,Error_6300). diff --git a/Makefile b/Makefile index 6be2a01..da9c8be 100644 --- a/Makefile +++ b/Makefile @@ -79,7 +79,7 @@ config: # configures and compiles compil: - @ocamlbuild $(PACKAGES) main.$(EXTENSION) worker.$(EXTENSION) main_api.$(EXTENSION) + @ocamlbuild -use-ocamlfind $(PACKAGES) main.$(EXTENSION) worker.$(EXTENSION) main_api.$(EXTENSION) @mv _build/Source/main.$(EXTENSION) deepsec @mv _build/Source/main_api.$(EXTENSION) deepsec_api @mv _build/Source/distributed/worker.$(EXTENSION) deepsec_worker diff --git a/flake.lock b/flake.lock new file mode 100644 index 0000000..6a7fc1f --- /dev/null +++ b/flake.lock @@ -0,0 +1,207 @@ +{ + "nodes": { + "flake-compat": { + "flake": false, + "locked": { + "lastModified": 1696426674, + "narHash": "sha256-kvjfFW7WAETZlt09AgDn1MrtKzP7t90Vf7vypd3OL1U=", + "owner": "edolstra", + "repo": "flake-compat", + "rev": "0f9255e01c2351cc7d116c072cb317785dd33b33", + "type": "github" + }, + "original": { + "owner": "edolstra", + "repo": "flake-compat", + "type": "github" + } + }, + "flake-utils": { + "inputs": { + "systems": "systems" + }, + "locked": { + "lastModified": 1731533236, + "narHash": "sha256-l0KFg5HjrsfsO/JpG+r7fRrqm12kzFHyUHqHCVpMMbI=", + "owner": "numtide", + "repo": "flake-utils", + "rev": "11707dc2f618dd54ca8739b309ec4fc024de578b", + "type": "github" + }, + "original": { + "owner": "numtide", + "repo": "flake-utils", + "type": "github" + } + }, + "flake-utils_2": { + "inputs": { + "systems": "systems_2" + }, + "locked": { + "lastModified": 1726560853, + "narHash": "sha256-X6rJYSESBVr3hBoH0WbKE5KvhPU5bloyZ2L4K60/fPQ=", + "owner": "numtide", + "repo": "flake-utils", + "rev": "c1dfcf08411b08f6b8615f7d8971a2bfa81d5e8a", + "type": "github" + }, + "original": { + "owner": "numtide", + "repo": "flake-utils", + "type": "github" + } + }, + "mirage-opam-overlays": { + "flake": false, + "locked": { + "lastModified": 1710922379, + "narHash": "sha256-j4QREQDUf8oHOX7qg6wAOupgsNQoYlufxoPrgagD+pY=", + "owner": "dune-universe", + "repo": "mirage-opam-overlays", + "rev": "797cb363df3ff763c43c8fbec5cd44de2878757e", + "type": "github" + }, + "original": { + "owner": "dune-universe", + "repo": "mirage-opam-overlays", + "type": "github" + } + }, + "nixpkgs": { + "locked": { + "lastModified": 1730785428, + "narHash": "sha256-Zwl8YgTVJTEum+L+0zVAWvXAGbWAuXHax3KzuejaDyo=", + "owner": "nixos", + "repo": "nixpkgs", + "rev": "4aa36568d413aca0ea84a1684d2d46f55dbabad7", + "type": "github" + }, + "original": { + "owner": "nixos", + "ref": "nixos-unstable", + "repo": "nixpkgs", + "type": "github" + } + }, + "opam-nix": { + "inputs": { + "flake-compat": "flake-compat", + "flake-utils": "flake-utils_2", + "mirage-opam-overlays": "mirage-opam-overlays", + "nixpkgs": "nixpkgs", + "opam-overlays": "opam-overlays", + "opam-repository": "opam-repository", + "opam2json": "opam2json" + }, + "locked": { + "lastModified": 1735755465, + "narHash": "sha256-ajcHT7JaqHWHy7cd2STB4TuQzCRf7sEfTH0waklOMB4=", + "owner": "tweag", + "repo": "opam-nix", + "rev": "6e6a1ac0203c3595c1ffac129d9ac32d8f7989c1", + "type": "github" + }, + "original": { + "owner": "tweag", + "repo": "opam-nix", + "type": "github" + } + }, + "opam-overlays": { + "flake": false, + "locked": { + "lastModified": 1726822209, + "narHash": "sha256-bwM18ydNT9fYq91xfn4gmS21q322NYrKwfq0ldG9GYw=", + "owner": "dune-universe", + "repo": "opam-overlays", + "rev": "f2bec38beca4aea9e481f2fd3ee319c519124649", + "type": "github" + }, + "original": { + "owner": "dune-universe", + "repo": "opam-overlays", + "type": "github" + } + }, + "opam-repository": { + "flake": false, + "locked": { + "lastModified": 1732612513, + "narHash": "sha256-kju4NWEQo4xTxnKeBIsmqnyxIcCg6sNZYJ1FmG/gCDw=", + "owner": "ocaml", + "repo": "opam-repository", + "rev": "3d52b66b04788999a23f22f0d59c2dfc831c4f32", + "type": "github" + }, + "original": { + "owner": "ocaml", + "repo": "opam-repository", + "type": "github" + } + }, + "opam2json": { + "inputs": { + "nixpkgs": [ + "opam-nix", + "nixpkgs" + ] + }, + "locked": { + "lastModified": 1671540003, + "narHash": "sha256-5pXfbUfpVABtKbii6aaI2EdAZTjHJ2QntEf0QD2O5AM=", + "owner": "tweag", + "repo": "opam2json", + "rev": "819d291ea95e271b0e6027679de6abb4d4f7f680", + "type": "github" + }, + "original": { + "owner": "tweag", + "repo": "opam2json", + "type": "github" + } + }, + "root": { + "inputs": { + "flake-utils": "flake-utils", + "nixpkgs": [ + "opam-nix", + "nixpkgs" + ], + "opam-nix": "opam-nix" + } + }, + "systems": { + "locked": { + "lastModified": 1681028828, + "narHash": "sha256-Vy1rq5AaRuLzOxct8nz4T6wlgyUR7zLU309k9mBC768=", + "owner": "nix-systems", + "repo": "default", + "rev": "da67096a3b9bf56a91d16901293e51ba5b49a27e", + "type": "github" + }, + "original": { + "owner": "nix-systems", + "repo": "default", + "type": "github" + } + }, + "systems_2": { + "locked": { + "lastModified": 1681028828, + "narHash": "sha256-Vy1rq5AaRuLzOxct8nz4T6wlgyUR7zLU309k9mBC768=", + "owner": "nix-systems", + "repo": "default", + "rev": "da67096a3b9bf56a91d16901293e51ba5b49a27e", + "type": "github" + }, + "original": { + "owner": "nix-systems", + "repo": "default", + "type": "github" + } + } + }, + "root": "root", + "version": 7 +} diff --git a/flake.nix b/flake.nix new file mode 100644 index 0000000..5c1e83e --- /dev/null +++ b/flake.nix @@ -0,0 +1,26 @@ +{ + inputs = { + opam-nix.url = "github:tweag/opam-nix"; + flake-utils.url = "github:numtide/flake-utils"; + nixpkgs.follows = "opam-nix/nixpkgs"; + }; + outputs = { self, flake-utils, opam-nix, nixpkgs }@inputs: + # Don't forget to put the package name instead of `throw': + let + package = "deepsec"; + in flake-utils.lib.eachDefaultSystem (system: + let + pkgs = nixpkgs.legacyPackages.${system}; + on = opam-nix.lib.${system}; + scope = + on.buildOpamProject { } package ./. { ocaml-base-compiler = "*"; }; + overlay = final: prev: + { + # Your overrides go here + }; + in { + legacyPackages = scope.overrideScope overlay; + + packages.default = self.legacyPackages.${system}.${package}; + }); +} From 1235126dee8f6fb8aad5474056a2a86ab90f4186 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Robert=20K=C3=BCnnemann?= Date: Tue, 21 Jan 2025 09:49:22 +0100 Subject: [PATCH 2/3] Still trying with nix. --- flake.lock | 12 ++++++------ flake.nix | 16 +++++++++++++--- script/check | 2 +- script/cpu_linux_osx | 2 +- 4 files changed, 21 insertions(+), 11 deletions(-) diff --git a/flake.lock b/flake.lock index 6a7fc1f..9de8866 100644 --- a/flake.lock +++ b/flake.lock @@ -95,11 +95,11 @@ "opam2json": "opam2json" }, "locked": { - "lastModified": 1735755465, - "narHash": "sha256-ajcHT7JaqHWHy7cd2STB4TuQzCRf7sEfTH0waklOMB4=", + "lastModified": 1737010256, + "narHash": "sha256-aL8yJZsR/oV1YwhuRVm1iQBMa5Uob9Gw6LuON75+j0g=", "owner": "tweag", "repo": "opam-nix", - "rev": "6e6a1ac0203c3595c1ffac129d9ac32d8f7989c1", + "rev": "57aee6d0f3fb0b39bbaf1635b2d8b8cabcf39725", "type": "github" }, "original": { @@ -127,11 +127,11 @@ "opam-repository": { "flake": false, "locked": { - "lastModified": 1732612513, - "narHash": "sha256-kju4NWEQo4xTxnKeBIsmqnyxIcCg6sNZYJ1FmG/gCDw=", + "lastModified": 1736935757, + "narHash": "sha256-LNkGSkZJXJmxpUd+luDUIIV/1B5MZIBMTB1qZqypa4o=", "owner": "ocaml", "repo": "opam-repository", - "rev": "3d52b66b04788999a23f22f0d59c2dfc831c4f32", + "rev": "a8b00ead922e2049581ab16994586ed4ddbdb784", "type": "github" }, "original": { diff --git a/flake.nix b/flake.nix index 5c1e83e..a340a50 100644 --- a/flake.nix +++ b/flake.nix @@ -1,14 +1,24 @@ { + description = "DeepSec: Deciding Equivalence Properties in Security Protocols. + +Automated verification has become an essential part in the security evaluation of cryptographic protocols. Recently, there has been a considerable effort to lift the theory and tool support that existed for reachability properties to the more complex case of equivalence properties. **DeepSec** allows you to decide trace equivalence and session equivalence for a large variety of cryptographic primitives---those that can be represented by a subterm convergent destructor rewrite system. + "; + inputs = { opam-nix.url = "github:tweag/opam-nix"; flake-utils.url = "github:numtide/flake-utils"; nixpkgs.follows = "opam-nix/nixpkgs"; + # nixpkgs.url = "github:nixos/nixpkgs"; }; - outputs = { self, flake-utils, opam-nix, nixpkgs }@inputs: + + outputs = { self, flake-utils, opam-nix + , nixpkgs +}@inputs: # Don't forget to put the package name instead of `throw': let package = "deepsec"; - in flake-utils.lib.eachDefaultSystem (system: + in + flake-utils.lib.eachDefaultSystem (system: let pkgs = nixpkgs.legacyPackages.${system}; on = opam-nix.lib.${system}; @@ -21,6 +31,6 @@ in { legacyPackages = scope.overrideScope overlay; - packages.default = self.legacyPackages.${system}.${package}; + defaultPackage = self.legacyPackages.${system}.${package}; }); } diff --git a/script/check b/script/check index 140c7fc..e0b3258 100755 --- a/script/check +++ b/script/check @@ -1,4 +1,4 @@ -#! /bin/bash +#!/nix/store/rj7zvmif800bgg3sbznq6g5g438jx104-bash-5.2p37/bin/bash # checks requirements for DeepSec installation diff --git a/script/cpu_linux_osx b/script/cpu_linux_osx index 178688e..2556041 100755 --- a/script/cpu_linux_osx +++ b/script/cpu_linux_osx @@ -1,4 +1,4 @@ -#!/bin/sh +#!/nix/store/rj7zvmif800bgg3sbznq6g5g438jx104-bash-5.2p37/bin/sh # macOS: Use `sysctl -n hw.*cpu_max`, which returns the values of # interest directly. From bac3b74a879d38b70debff4ff5638674318f21fa Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Robert=20K=C3=BCnnemann?= Date: Mon, 3 Mar 2025 10:39:10 +0100 Subject: [PATCH 3/3] Some cleanup (accidentally changed example file) --- .../Electronic_passport/Basic-access-control/BAC-2sessions.dps | 3 +-- flake.nix | 1 + 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/Examples/trace_equivalence/Electronic_passport/Basic-access-control/BAC-2sessions.dps b/Examples/trace_equivalence/Electronic_passport/Basic-access-control/BAC-2sessions.dps index 7d2e1a1..2327475 100644 --- a/Examples/trace_equivalence/Electronic_passport/Basic-access-control/BAC-2sessions.dps +++ b/Examples/trace_equivalence/Electronic_passport/Basic-access-control/BAC-2sessions.dps @@ -5,7 +5,6 @@ fun mac/2. free c. free Error_6300. -free Error_6A80. free get_challenge. fun senc/2. @@ -41,7 +40,7 @@ let passport(k_e,k_m) = new k_t; let z = senc((n_t,xn_r,k_t),k_e) in out(c,(z,mac(z,k_m))) - ) else out(c,Error_6A80) + ) else out(c,Error_6300) else out(c,Error_6300) else out(c,Error_6300). diff --git a/flake.nix b/flake.nix index a340a50..029a7ac 100644 --- a/flake.nix +++ b/flake.nix @@ -32,5 +32,6 @@ Automated verification has become an essential part in the security evaluation o legacyPackages = scope.overrideScope overlay; defaultPackage = self.legacyPackages.${system}.${package}; + }); }