src/HOL/Auth/CertifiedEmail.thy

 constdefs
   "response"    :: "agent => agent => nat => msg"
    "response S R q == Hash {|Agent S, Key (shrK R), Nonce q|}"
 
 
-consts  certified_mail   :: "event list set"
-inductive "certified_mail"
-  intros 
-
-Nil: --{*The empty trace*}
+inductive_set certified_mail :: "event list set"
+  where
+
+  Nil: --{*The empty trace*}
      "[] \<in> certified_mail"
 
-Fake: --{*The Spy may say anything he can say.  The sender field is correct,
+| Fake: --{*The Spy may say anything he can say.  The sender field is correct,
           but agents don't use that information.*}
       "[| evsf \<in> certified_mail; X \<in> synth(analz(spies evsf))|] 
        ==> Says Spy B X # evsf \<in> certified_mail"
 
-FakeSSL: --{*The Spy may open SSL sessions with TTP, who is the only agent
+| FakeSSL: --{*The Spy may open SSL sessions with TTP, who is the only agent
     equipped with the necessary credentials to serve as an SSL server.*}
 	 "[| evsfssl \<in> certified_mail; X \<in> synth(analz(spies evsfssl))|]
           ==> Notes TTP {|Agent Spy, Agent TTP, X|} # evsfssl \<in> certified_mail"
 
-CM1: --{*The sender approaches the recipient.  The message is a number.*}
+| CM1: --{*The sender approaches the recipient.  The message is a number.*}
  "[|evs1 \<in> certified_mail;
     Key K \<notin> used evs1;
     K \<in> symKeys;
     Nonce q \<notin> used evs1;
     hs = Hash{|Number cleartext, Nonce q, response S R q, Crypt K (Number m)|};
     S2TTP = Crypt(pubEK TTP) {|Agent S, Number BothAuth, Key K, Agent R, hs|}|]
   ==> Says S R {|Agent S, Agent TTP, Crypt K (Number m), Number BothAuth, 
 		 Number cleartext, Nonce q, S2TTP|} # evs1 
 	\<in> certified_mail"
 
-CM2: --{*The recipient records @{term S2TTP} while transmitting it and her
+| CM2: --{*The recipient records @{term S2TTP} while transmitting it and her
      password to @{term TTP} over an SSL channel.*}
  "[|evs2 \<in> certified_mail;
     Gets R {|Agent S, Agent TTP, em, Number BothAuth, Number cleartext, 
 	     Nonce q, S2TTP|} \<in> set evs2;
     TTP \<noteq> R;  
     hr = Hash {|Number cleartext, Nonce q, response S R q, em|} |]
   ==> 
    Notes TTP {|Agent R, Agent TTP, S2TTP, Key(RPwd R), hr|} # evs2
       \<in> certified_mail"
 
-CM3: --{*@{term TTP} simultaneously reveals the key to the recipient and gives
+| CM3: --{*@{term TTP} simultaneously reveals the key to the recipient and gives
          a receipt to the sender.  The SSL channel does not authenticate 
          the client (@{term R}), but @{term TTP} accepts the message only 
          if the given password is that of the claimed sender, @{term R}.
          He replies over the established SSL channel.*}
  "[|evs3 \<in> certified_mail;

   ==> 
    Notes R {|Agent TTP, Agent R, Key k, hr|} # 
    Gets S (Crypt (priSK TTP) S2TTP) # 
    Says TTP S (Crypt (priSK TTP) S2TTP) # evs3 \<in> certified_mail"
 
-Reception:
+| Reception:
  "[|evsr \<in> certified_mail; Says A B X \<in> set evsr|]
   ==> Gets B X#evsr \<in> certified_mail"
 
 
 declare Says_imp_knows_Spy [THEN analz.Inj, dest]