Correspondence assertions

%%%
%%% Asynchronous pi-calculus with correspondence assertions
%%%
%%% Author: Kevin Watkins
%%% Date: 19 March 2004
%%%
%%% Following Gordon & Jeffrey, "Typing correspondence assertions for
%%% communication protocols", TCS 300:1-3, pp. 379--409.
%%%
%%%   http://portal.acm.org/citation.cfm?id=795654&dl=ACM&coll=portal#
%%%
%%% See also Woo & Lam, "A semantic model for authentication
%%% protocols", IEEE Symp. on Security and Privacy, 1993,
%%% pp. 178--194.
%%%
%%%   http://www.cs.utexas.edu/users/lam/NRL/verify.html
%%%

%%
%% Labels
%%

label : type.
!= : label -> label -> type.
%infix none 0 !=.

%%
%% Processes (untyped, asynchronous, non-polyadic)
%%

pr : type.
ch : type.

out : ch -> ch -> pr.
in : ch -> (ch -> pr) -> pr.
choose : pr -> pr -> pr.
new : (ch -> pr) -> pr.
alt : pr -> pr -> pr.
repeat : pr -> pr.
stop : pr.

begin : label -> pr -> pr.
end : label -> pr -> pr.

%%
%% Executions
%%
%% Executions can stop at any time. (See exec_encap.)
%%

exec : pr -> type.
run : pr -> type.

ev_stop : run stop -o {}.
ev_alt : run (alt P Q) -o {^run P, ^run Q}.
ev_repeat : run (repeat P) -o {:run P}.
ev_choose1 : run (choose P Q) -o {^run P}.
ev_choose2 : run (choose P Q) -o {^run Q}.
ev_new : run (new [x] P x) -o {x, ^run (P x)}.
ev_sync : run (out X Y) -o run (in X [y] Q y) -o {^run (Q Y)}.

ev_begin : {L} run (begin L P) -o {^run P}.
ev_end : {L} run (end L P) -o {^run P}.

exec_encap : exec P <- (run P -o {^()}).

%%
%% Traces
%%
%% We capture bound channel names in a trace so that labels can
%% depend on channel names if necessary.
%%

tr : type.

tnil : tr.
tbegin : label -> tr -> tr.
tend : label -> tr -> tr.
tgen : (ch -> tr) -> tr.

%%
%% Abstraction
%%
%% We can stop abstracting at any time. Thus the set of traces
%% abstractable from an execution is prefix-closed. (See abst_nil.)
%%

abst : {^()} -> tr -> type.

abst_nil : abst _ tnil.

abst_stop : abst [=ev_stop^R; _^()=E; ^()] T
  <- abst [_^()=E; ^()] T.
abst_alt : abst [r1^,r2^=ev_alt^R; _^()=E^r1^r2; ^()] T
  <- ({r1} {r2} abst [_^()=E^r1^r2; ^()] T).
abst_repeat : abst [r1=ev_repeat^R; _^()=E r1; ^()] T
  <- ({r1} abst [_^()=E r1; ^()] T).
abst_choose1 : abst [r1^=ev_choose1^R; _^()=E^r1; ^()] T
  <- ({r1} abst [_^()=E^r1; ^()] T).
abst_choose2 : abst [r2^=ev_choose2^R; _^()=E^r2; ^()] T
  <- ({r2} abst [_^()=E^r2; ^()] T).
abst_new : abst [x,r1^=ev_new^R; _^()=E x^r1; ^()] (tgen [x] T x)
  <- ({x} {r1} abst [_^()=E x^r1; ^()] (T x)).
abst_sync : abst [r^=ev_sync^R1^R2; _^()=E^r; ^()] T
  <- ({r} abst [_^()=E^r; ^()] T).

abst_begin : abst [r1^=ev_begin L^R; _^()=E^r1; ^()] (tbegin L T)
  <- ({r1} abst [_^()=E^r1; ^()] T).
abst_end : abst [r1^=ev_end L^R; _^()=E^r1; ^()] (tend L T)
  <- ({r1} abst [_^()=E^r1; ^()] T).

%%
%% Invalid traces
%%
%% We say a trace is invalid iff it is not a correspondence.
%%

invalid : tr -> type.
remove : label -> tr -> tr -> type.

invalid_unmatched : invalid (tend _ _).

invalid_gen : invalid (tgen [x] T x)
  <- ({x} invalid (T x)).
invalid_begin : invalid (tbegin L T)
  <- remove L T T'
  <- invalid T'.

remove_match : remove L (tend L T) T.

remove_nil : remove L tnil tnil.
remove_gen : remove L (tgen [x] T x) (tgen [x] T' x)
  <- ({x} remove L (T x) (T' x)).
remove_begin : remove L (tbegin L' T) (tbegin L' T')
  <- remove L T T'.
remove_end : remove L (tend L' T) (tend L' T')
  <- L != L'
  <- remove L T T'.

%%
%% Wrong executions
%%

wrong : exec P -> type.

wrong_if_invalid_abst : wrong (exec_encap [r^] [_^()=E^r; ^()])
  <- ({r} abst [_^()=E^r; ^()] T)
  <- invalid T.

%%
%% Unsafe programs
%%

unsafe : pr -> type.

unsafe_if_wrong_exec : {E:exec P} wrong E -> unsafe P.

%%
%% Static semantics
%% Frank Pfenning
%% Apr  6 2004
%%

% Represent multiset [L1,...,Ln]
% as [=latent L1; =latent L2; ... ; =latent Ln;] : {}
% all bindings commute to generate multiset equality

eff = {} : type.		% abbreviation to express intent
latent : label -> eff.

wfeff : eff -> type.            % wfeff E -- E is a well-formed effect
wff_eps : wfeff [].
wff_lat : wfeff [=latent L; =E;] <- wfeff [=E;]. 

tp : type.
name : tp.
chan : tp -> (ch -> eff) -> tp.

has : ch -> tp -> type.		% only hyps :has X T
effect : label -> type.		% only hyps ^effect L
good : pr -> type.		% only conc M:good P
wftp : tp -> type.              % only conc D:wftp T

wf_name : wftp name.
wf_chan : wftp (chan T [x] E x)
           <- wftp T
           <- ({x} has x T -> wfeff (E x)).

consume : eff -> type.          % consume E -- consume latent effects
assume : eff -> pr -> type.     % assume E P -- assume latent effects for P

% consume E and assume E P implicitly check well-formedness of E.
con_eps : consume []
           o- ().
con_join : consume [=latent L; =E;]
	    o- effect L
            o- consume [=E;].

ass_eps : assume [] P
	   o- good P.
ass_join : assume [=latent L; =E;] P
            o- (effect L -o assume [=E;] P).

gd_out : good (out X Y)
          <- has X (chan T [y] E y)
          <- has Y T
          o- consume (E Y).
gd_in : good (in X [y] P y)
         <- has X (chan T [y] E' y)
	 <- wftp T
         o- ({y:ch} has y T -> assume (E' y) (P y)).
gd_choose : good (choose P Q)
             o- (good P & good Q).
gd_new : good (new [x] P x)	% T should be part of syntax
          <- wftp T
          o- ({x:ch} has x T -> good (P x)).
gd_alt : good (alt P Q)
          o- good P
          o- good Q.
gd_repeat : good (repeat P)
	     <- good P		% no effects in P
	     o- ().
gd_stop : good (stop)
           o- ().

%%
%% An unsafe program
%%
%% This is the example of section 2 of the paper, in non-polyadic
%% form.
%%

out_and : ch -> ch -> pr -> pr = [X] [Y] [P] alt (out X Y) P.
ev_sync_and = [Rout_and^] [Rin^]
  [r1^,r2^=ev_alt^Rout_and;
   r3^=ev_sync^r1^Rin;
   ^r2,^r3]

prin : type.

ack_recvd : prin -> prin -> ch -> label.

receiver = [A] [B] [C]
  (in C [Msg]
  (in C [Ack]
  (begin (ack_recvd A B Msg)
  (out Ack Ack)))).

sender = [A] [B] [C]
  (new [Msg]
  (new [Ack]
  (out_and C Msg
  (out_and C Ack
  (in Ack [_]
  (end (ack_recvd A B Msg)
  (stop))))))).

alice : prin.
andrew : prin.
bob : prin.

alice!=andrew : ack_recvd alice _ _ != ack_recvd andrew _ _.

the_program =
  (new [C]
  (alt (sender alice bob C)
  (alt (sender andrew bob C)
  (alt (receiver alice bob C)
  (stop))))).

the_wrong_execution =
  (exec_encap [r^]
  [c,r^=ev_new^r;
   r_alice^,r^=ev_alt^r;
   r_andrew^,r^=ev_alt^r;
   r_bob^,r^=ev_alt^r;
   =ev_stop^r;

   msg,r_andrew^=ev_new^r_andrew;
   ack,r_andrew^=ev_new^r_andrew;

   r_andrew^,r_bob^=ev_sync_and^r_andrew^r_bob;
   r_andrew^,r_bob^=ev_sync_and^r_andrew^r_bob;

   r_bob^=ev_begin (ack_recvd alice bob msg)^r_bob;

   r_andrew^=ev_sync^r_bob^r_andrew;

   r_andrew^=ev_end (ack_recvd andrew bob msg)^r_andrew;
   =ev_stop^r_andrew;

   ^()  % absorb r_alice
   ]).

the_abstraction =
  (tgen [c]
  (tgen [msg]
  (tgen [ack]
  (tbegin (ack_recvd alice bob msg)
  (tend (ack_recvd andrew bob msg)
  (tnil)))))).

_ : invalid the_abstraction = ...  

_ : wrong the_wrong_execution = ...

_ : unsafe the_program = ...