asm Autenticazione
import ../STDL/StandardLibrary
import ../STDL/LTLLibrary
import ../STDL/CTLLibrary

signature:
	// Domains
	abstract domain Utenti
	enum domain Stato = {ATTIVO | AUTENTICATO | BLOCCATO}
	domain Tentativi subsetof Integer
	domain Password subsetof Integer
	
	// Controlled Functions -> stato del sistema
	controlled stato: Utenti -> Stato
	controlled tentativi: Utenti -> Tentativi
	
	// Monitored Functions -> input dall'ambiente
	monitored richiestaAutenticazione: Boolean
	monitored utenteRichiedente: Utenti
	monitored passwordInserita: Password
	
	// Static Functions -> costanti e elementi dei domini astratti
	static password: Utenti -> Password
	static maxTentativi: Tentativi
	static utente1: Utenti
	static utente2: Utenti
	static utente3: Utenti

definitions:
	// Definizione dei domini
	domain Tentativi = {0:3}
	domain Password = {0:1000}
	
	// Definizione delle funzioni costanti
	function maxTentativi = 3
	function password($u in Utenti) = 
		switch $u
			case utente1: 100
			case utente2: 200
			case utente3: 300
		endswitch
	
	// Transition rules
	rule r_gestisciRichiesta($u in Utenti) =
		if stato($u) != AUTENTICATO then
			if tentativi($u) < maxTentativi then
				if passwordInserita = password($u) then
					stato($u) := AUTENTICATO
				else
					tentativi($u) := tentativi($u) + 1
				endif  
			else
				stato($u) := BLOCCATO
			endif
		endif
		
	// Proprietà
	// 1. Esiste uno stato in cui tutti gli utenti sono autenticati
	CTLSPEC ef((forall $u in Utenti with stato($u) = AUTENTICATO))
	
	// 2. Se un utente è bloccato, allora il suo numero di tentativi è pari al massimo
	LTLSPEC g((forall $u in Utenti with (stato($u) = BLOCCATO implies tentativi($u) = maxTentativi)))
	
	// 3. Se un utente è bloccato, allora rimane sempre bloccato in futuro
	CTLSPEC ag((forall $u in Utenti with (stato($u) = BLOCCATO implies ag(stato($u) = BLOCCATO))))
	
	// 4. Se utente1 ha raggiunto il numero massimo di tentativi e richiede autenticazione, allora viene bloccato
	LTLSPEC g((
		tentativi(utente1) = maxTentativi and
		richiestaAutenticazione and
		utenteRichiedente = utente1
	) implies x(stato(utente1) = BLOCCATO))
	
	// 5. Se utente1 non ha esaurito i tentativi disponibili ed effettua una richiesta di autenticazione corretta, allora nel passo successivo è autenticato e rimane sempre autenticato
	CTLSPEC ag((
		tentativi(utente1) < maxTentativi
		and passwordInserita = password(utente1)
		and richiestaAutenticazione
		and utenteRichiedente = utente1
	) 
	implies ax (ag (stato(utente1) = AUTENTICATO)))
	
	// 6. Per ogni utente, il numero di tentativi è sempre compreso tra 0 e il numero massimo di tentativi
	CTLSPEC ag((forall $u in Utenti with tentativi($u) >= 0 and tentativi($u)<=maxTentativi))
	
	// 7. Se un utente è bloccato, allora non può più passare allo stato autenticato
	CTLSPEC ag((forall $u in Utenti with stato($u) = BLOCCATO implies not ef(stato($u) = AUTENTICATO)))
	
	// 8. utente1 rimane attivo finché non si autentica oppure viene bloccato
	CTLSPEC aw(stato(utente1) = ATTIVO, stato(utente1) = BLOCCATO or stato(utente1) = AUTENTICATO)
		
	// Main rule -> entrypoint dell'esecuzione
	main rule r_Main = 
		if richiestaAutenticazione then
			r_gestisciRichiesta[utenteRichiedente]
		endif

default init s0:
	// Stato iniziale
	function stato($u in Utenti) = ATTIVO
	function tentativi($u in Utenti) = 0
