% TESTED FEATURES: channel assumtion "secure" does not imply ordering (as e.g. in TLS)!
% EXPECTED OUTCOME: Unsafe
specification ChannelSecureOrder_Unsafe
channel_model CCM

entity Environment
{
	symbols 
		a, b : agent;

	entity Alice(Actor, B : agent) {
		symbols
			Nonce : text;
		body {
			Nonce := fresh();
			Actor *->* B : Nonce.1;

			%this would enforce the order: B *->* Actor: ?; 

			Actor *->* B : Nonce.2;
		}
	}

	entity Bob(A, Actor : agent) {
		symbols
			Nonce : text;
			N: nat;
			sync: text;
		body {
			A *->* Actor : ?Nonce.?N;
			assert order1: N=1;

			Actor *->* A: sync;

			A *->* Actor : ?Nonce.?N;
			assert order2: N=2;
		}
	}

	body {
		new Alice(a, b);
		new Bob  (a, b);
	}
}