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.