diff --git a/Example57_Authentication.mp b/Example57_Authentication.mp new file mode 100644 index 0000000000000000000000000000000000000000..c9b6910a2f419ed793249dc98cedc1ad1e6efb93 --- /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