From 4046566285c315a5c885c7cdcca8e972d52bb85c Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Th=C3=A9ophile=20Wallez?= Date: Fri, 29 Nov 2024 17:20:48 +0100 Subject: [PATCH] chore: update DY* --- flake.lock | 6 +++--- fstar/symbolic/MLS.Symbolic.MyMkRand.fst | 5 ++--- .../treesync/symbolic/MLS.TreeSync.Symbolic.AuthService.fst | 2 +- 3 files changed, 6 insertions(+), 7 deletions(-) diff --git a/flake.lock b/flake.lock index 85ab37d..a88f58a 100644 --- a/flake.lock +++ b/flake.lock @@ -36,11 +36,11 @@ ] }, "locked": { - "lastModified": 1731509593, - "narHash": "sha256-zQF1zZnXmLt+UgnMa9vK4QgQtrfG28EwAky/Dgac/s4=", + "lastModified": 1732872022, + "narHash": "sha256-NzxnEUE3HjEe152T+ttCBb+PbHHtMgHZ8GGrYcHkMV8=", "owner": "REPROSEC", "repo": "dolev-yao-star-extrinsic", - "rev": "27826bbb7745dac32317e783257e9098bcd3ff36", + "rev": "f3e40496fb1a3431323974baac3b46f316a78166", "type": "github" }, "original": { diff --git a/fstar/symbolic/MLS.Symbolic.MyMkRand.fst b/fstar/symbolic/MLS.Symbolic.MyMkRand.fst index 1c1a8b6..bfbc0f6 100644 --- a/fstar/symbolic/MLS.Symbolic.MyMkRand.fst +++ b/fstar/symbolic/MLS.Symbolic.MyMkRand.fst @@ -23,12 +23,11 @@ val my_mk_rand_trace_invariant: (ensures ( let (b, tr_out) = my_mk_rand usg lab len tr in trace_invariant tr_out /\ - 1 <= DY.Core.Trace.Base.length tr_out /\ - rand_generated_at tr_out (DY.Core.Trace.Base.length tr_out - 1) b + rand_just_generated tr_out b )) [SMTPat (my_mk_rand usg lab len tr); SMTPat (trace_invariant tr)] let my_mk_rand_trace_invariant #invs usg lab len tr = - let result = (Rand len (DY.Core.Trace.Base.length tr)) in + let result = (Rand len (trace_length tr)) in add_entry_invariant (RandGen usg (lab result) len) tr; reveal_opaque (`%my_mk_rand) (my_mk_rand) #pop-options diff --git a/fstar/treesync/symbolic/MLS.TreeSync.Symbolic.AuthService.fst b/fstar/treesync/symbolic/MLS.TreeSync.Symbolic.AuthService.fst index ef4de61..edadb17 100644 --- a/fstar/treesync/symbolic/MLS.TreeSync.Symbolic.AuthService.fst +++ b/fstar/treesync/symbolic/MLS.TreeSync.Symbolic.AuthService.fst @@ -29,7 +29,7 @@ let dy_asp #ci tr = { match credential_to_principal cred with | None -> False | Some who -> - token.time <= (DY.Core.Trace.Base.length tr) /\ + token.time `on_trace` tr /\ is_signature_key_vk (prefix tr token.time) who vk ); valid_successor = (fun (vk_old, cred_old) (vk_new, cred_new) ->