From 6df4bc29a511bee2c0dcb8872a27d8e114c968d1 Mon Sep 17 00:00:00 2001
From: "Giammarco, Kristin M" <kmgiamma@nps.edu>
Date: Wed, 16 Jun 2021 22:55:47 +0000
Subject: [PATCH] Upload New File

---
 Example57_Authentication.mp | 56 +++++++++++++++++++++++++++++++++++++
 1 file changed, 56 insertions(+)
 create mode 100644 Example57_Authentication.mp

diff --git a/Example57_Authentication.mp b/Example57_Authentication.mp
new file mode 100644
index 0000000..c9b6910
--- /dev/null
+++ b/Example57_Authentication.mp
@@ -0,0 +1,56 @@
+/*******************************************************************************
+
+A Model for Simple Authentication
+
+A demonstration that shows how to reject unwanted behaviors with ENSURE 
+constraints.
+  
+  created by K.Giammarco on 05/16/2017
+  modified by K.Giammarco on 08/07/2017 for capitalization of state events
+  modified by K.Giammarco on 08/07/2017 for ENSURE constraints
+  
+********************************************************************************/
+
+SCHEMA Authentication
+
+/*-----------------------
+  USER BEHAVIORS
+-------------------------*/
+
+ROOT User: 	Provide_credentials
+			  (* CREDS_INVALID Reenter_credentials *)
+			 [ CREDS_VALID Access_system ];
+
+/*-----------------------
+  SYSTEM BEHAVIORS
+-------------------------*/
+
+ROOT System:	Verify_credentials
+				(+ ( CREDS_INVALID Deny_access |
+                    	CREDS_VALID Grant_access ) +)
+				[ Lock_account ]
+                ;
+
+/*-----------------------
+  INTERACTION CONSTRAINTS
+-------------------------*/
+
+User, System SHARE ALL CREDS_VALID, CREDS_INVALID;
+
+COORDINATE 	$a: Provide_credentials	FROM User,
+			$b: Verify_credentials	FROM System
+		DO ADD $a PRECEDES $b; OD;
+
+COORDINATE 	$a: Deny_access				FROM System,
+			$b: Reenter_credentials 	FROM User
+		DO ADD $a PRECEDES $b; OD; 
+
+COORDINATE 	$a: Grant_access		FROM System,
+			$b: Access_system		FROM User
+		DO ADD $a PRECEDES $b; OD; 
+
+ENSURE #CREDS_INVALID <= 3;
+
+ENSURE #Deny_access >= 3 <-> #Lock_account == 1;
+
+ENSURE #Grant_access >= 1 -> #Lock_account == 0;
\ No newline at end of file
-- 
GitLab