The files in this directory express two way secure message communication (SMC) out of ordinary SMC and the forwarding ideal functionality. This is a two party functionality letting the clients of the two parties securely exchange a pair of messages: first one from the first to the second, followed by one from the second to the first.
The supporting UC DSL and EasyCrypt code is in the subdirectory
supporting
. When compiling SMC2.uc
from the command line or in
Emacs in UC DSL mode, you will thus need to include the command line
option -I supporting
. But when running the UC DSL interpreter inside
Proof General, supporting
is automatically included in the load path
because of the setting for ucdsl-interpreter-mode
in
.dir-locals.el
.
Read and experiment with the interpretation script testing.uci to learn how to use the UC DSL interpreter.