From 0e15b7221f50246c88ada3e805e9a3fd1e40a434 Mon Sep 17 00:00:00 2001 From: Cas Cremers Date: Thu, 10 Jan 2008 16:10:21 +0100 Subject: [PATCH] Strange problem with concretization algorithm. Terence is selected, but it should not be. This is a bug and should be fixed. --- protocols/misc/tls/tls-paulson-avispa.spdl | 2 ++ 1 file changed, 2 insertions(+) diff --git a/protocols/misc/tls/tls-paulson-avispa.spdl b/protocols/misc/tls/tls-paulson-avispa.spdl index 5fc352d..19c11cc 100644 --- a/protocols/misc/tls/tls-paulson-avispa.spdl +++ b/protocols/misc/tls/tls-paulson-avispa.spdl @@ -15,7 +15,9 @@ secret unkeygen: Function; inversekeys(keygen, unkeygen); const pa,pb: Params; +const Alice,Bob: Agent; const Terence: Agent; +const Sally: Agent; const false,true: Bool;