comparison src/ur/openid.urs @ 39:f6b3fbf10dac

Proper handling of known vs. to-be-chosen identifiers
author Adam Chlipala <adam@chlipala.net>
date Wed, 01 Jun 2011 07:51:55 -0400
parents 35bc4da563dd
children
comparison
equal deleted inserted replaced
38:8d23d76b5d48 39:f6b3fbf10dac
70 datatype association_mode = 70 datatype association_mode =
71 Stateless 71 Stateless
72 | Stateful of {AssociationType : association_type, 72 | Stateful of {AssociationType : association_type,
73 AssociationSessionType : association_session_type} 73 AssociationSessionType : association_session_type}
74 74
75 (* It is possible to request authentication in two different modes: *)
76
77 datatype authentication_mode =
78 ChooseIdentifier of string
79 (* The provider prompts the user to select his identity.
80 * The string argument should be a generic endpoint, e.g.,
81 * "https://www.google.com/accounts/o8/id". *)
82 | KnownIdentifier of string
83 (* Require authentication as this precise identifier. *)
84
75 (* An authentication attempt terminates in one of four ways. 85 (* An authentication attempt terminates in one of four ways.
76 * First, the user might get bored and surf away, never finishing the process. 86 * First, the user might get bored and surf away, never finishing the process.
77 * If so, your application will never be told explicitly. 87 * If so, your application will never be told explicitly.
78 * The other possibilities are captured by this datatype: *) 88 * The other possibilities are captured by this datatype: *)
79 89
108 (* Your preferences for statefulness and cryptography. 118 (* Your preferences for statefulness and cryptography.
109 * If the remote server doesn't support some kind of 119 * If the remote server doesn't support some kind of
110 * crypto that you ask for, the library automatically 120 * crypto that you ask for, the library automatically
111 * switches to a mode that the server advertises as 121 * switches to a mode that the server advertises as
112 * supported. *) 122 * supported. *)
113 Identifier : string, 123 Identifier : authentication_mode,
114 (* The URL that the user claims identifies him. 124 (* The URL that the user claims identifies him.
115 * It may also point to a generic authentication service 125 * It may also point to a generic authentication service
116 * that will take care of deciding the proper 126 * that will take care of deciding the proper
117 * username. *) 127 * username. *)
118 Realm : option string 128 Realm : option string