(* Authentication example:
B -> A: {Na}pkA (Na fresh nonce)
A -> B: Na
When B receives Na, A must have been executed.

*)

(* In order to determine the proof, use interactive mode:
   set interactiveMode = true.
The proof is as follows: *)

proof {
(* We first guess the tested session of B *)
guess iB;
SArename na_1;
(* We apply IND-CCA2 of encryption only in the tested session. *)
crypto ind_cca2_partial(enc) rkA r_2 .;
insert after_nth 1 "event eA" "eAex <- true";
insert before "event eB" "find j <= NA suchthat defined(eAex[j]) then else event_abort bad";
replace at 1 "eB_1({[0-9]+}na_3)" "na_3[iB_tested]";
success;
success simplify;
global_dep_anal na_3;
success
}

param NA, NB.

type nonce [large,fixed].
type pkey [bounded].
type skey [bounded].
type keyseed [large,fixed].
type blocksize [fixed].

fun pad(nonce):blocksize [data].

(* Public-key encryption (CCA2) *)
proba Penc.
proba Penccoll.
expand IND_CCA2_public_key_enc(keyseed, pkey, skey, blocksize, bitstring, skgen, pkgen, enc, dec, injbot, Z, Penc, Penccoll).

const Zblocksize: blocksize.
equation forall x: blocksize; Z(x) = Zblocksize.

(* Queries and Events *)
event eA(nonce).
event eB(nonce).

query x:nonce; event(eB(x)) ==> event(eA(x)).
query x:nonce; inj-event(eB(x)) ==> inj-event(eA(x)).

(* Channels and Processes *)
channel c1, c2, c3, c4, c5, c6, c7, c8, c9, c10, c11, c12, c13, c14,
	c15, c16, c17, start, finish.

let processA(skA: skey) =
	in(c1, m: bitstring);
	let injbot(pad(na)) = dec(m, skA) in
	event eA(na);
	out(c2, na).

let processB(pkA: pkey) =
        in(c3, ());
	new na: nonce;
	out(c4, enc(pad(na), pkA));
	in(c5, =na);
	event eB(na).

process
	in(start, ());
	new rkA: keyseed;
	let pkA = pkgen(rkA) in
	let skA = skgen(rkA) in
	out(c15, pkA);
	((! iA <= NA processA(skA)) |
	 (! iB <= NB processB(pkA)))


(* EXPECTED
All queries proved.
0.104s (user 0.088s + system 0.016s), max rss 17220K
END *)