Writing SecPAL assertions in F#

I figured I would try to learn F# over this summer - and thought what better way to start than create a couple of SecPAL samples in F#. I thought this might help people that are interested in learning more about F#, or potentially F# users that are interested in learning more about how SecPAL can be used for access control scenarios. The sample below is simplified version of our classic multi-domain scenario (see here for a complete description). In short we have three parties: A resource guard that is responsible for protecting access to a resource, an STS that is trusted to issue claims about users, and a user that wants to access a file.

In order to support this scenario we have the following assertions:

When run the code will output a textual proof graph illustrating exactly what the chain of deductions were that lead to this authorization decision being approved. If you want to use our graphical proof graph viewer take a look at this post. You will have to add an audit policy but that is really straight forward.

The F# code for this scenario is included below. In the my next few blog posts I will show you how to modify this code to do some extra cool things... In the mean time let me know if you have any questions, or if there are any scenarios you would like me to demonstrate.

Thanks to Don Syme and Can Erton of the F-Sharp team for reviewing my code before I released it!

 // Title: Simple SecPAL security scenario (F#)
// Update the pointer below to your SecPAL DLL (The SecPAL .NET implementation is available from https://research.microsoft.com/projects/secpal) 
 #I "C:\Users\jahogg\Documents\Microsoft SecPal Research Release\Bin\Microsoft.Research.SecPal.dll"
#r "Microsoft.Research.SecPal.dll"

open Microsoft.Research.SecPal.Authorization 
open System.Security.Cryptography
open System.Collections.Generic
type SecPALAttribute = Microsoft.Research.SecPal.Authorization.Attribute

// Define the users within the simple scenario
let User = KeyHolderPrincipal(new RSACryptoServiceProvider(), "Jason")
let STS = KeyHolderPrincipal(new RSACryptoServiceProvider(), "STS")
let ResourceGuard = LocalAuthorityPrincipal("ResourceGuard") // ResouceGuard == LocalAuthority == LA

// Define Resource Access Policy 
//     LA says %p read file://public/ if %p possesses %a where %a match ".*@microsoft.com"                     
let claims = [Claim(fact=ActionFact(PrincipalVariable("p"),
                    constraint=AttributeMatchConstraint("a",AttributeType.rfc822Name, @".*@microsoft\.com"));
              // LA says STS canSay %p possesses %a where %a match ".*@microsoft.com"                     
                    constraint=AttributeMatchConstraint("a",AttributeType.rfc822Name, @".*@microsoft\.com")) ]

let policy = Policy(PrincipalIssuer(ResourceGuard), claims)
let policies = [ policy ]

// Create a Token to identify our User with 
//      STS says User possesses rfc822Name:"jahogg@microsoft.com"
let token = Token(issuer=PrincipalIssuer(STS),
                  claims=[ Claim(fact=PossessFact(User, 
                                                  new SecPALAttribute(AttributeType.rfc822Name,@"jason@microsoft.com")))]) 

let tokens = [ token ]

// Create our Authorization Query 
//        LA says Jason can read file://public/foo.txt?

let query = AuthorizationQuery
                        fact=ActionFact(User, ActionVerbs.read, 

// Perform our Authorization Query using the Authorization Engine        
let answers = AuthorizationEngine.MakeAuthorizationDecision(ResourceGuard, tokens, policies, query) 
// Determine if access was granted
let results = (if (answers.Count < 1) then "Denied" else "Authorized") 

// Print out the results
printf "The result is %s \n" results
printf "Answer count = %i \n\n" answers.Count

// Iterate over the Proofs
for answer in answers do
    // Output variable substitutions
    let subs = answer.Substitution 
    for sub in subs do
        System.Console.WriteLine ("Name " + sub.Key.Name + " = " + sub.Value.ToString());
    // Output proof graphs
    let proofs = answer.ProofGraphs 
    for proof in proofs do
        System.Console.Write("Expression = ")
        System.Console.WriteLine("Graph = ")

// Press any key to continue (Homer "Where's the any key?")