diff --git a/proofs/authentication/README.md b/proofs/authentication/README.md
index c6cb98f..f2bd9f6 100644
--- a/proofs/authentication/README.md
+++ b/proofs/authentication/README.md
@@ -134,9 +134,9 @@
 
 5. RESULT not attacker(secretMessage[]) is true.
 
-6. RESULT event(termDialer(k, pkc, pks)) ==> event(acceptsAcceptor(k, pkc, pks)) is true.
+6. RESULT event(termDialer(k,publicKey(privKeyDialer[]),publicKey(privKeyAcceptor[]))) ==> event(acceptsAcceptor(k,publicKey(privKeyDialer[]),publicKey(privKeyAcceptor[]))) is true.
 
-7. RESULT event(acceptsAcceptor(k, pkc, pks)) ==> event(acceptsDialer(k, pkc, pks)) is true.
+7. RESULT event(acceptsAcceptor(k,publicKey(privKeyDialer[]),publicKey(privKeyAcceptor[]))) ==> event(acceptsDialer(k,publicKey(privKeyDialer[]),publicKey(privKeyAcceptor[]))) is true.
 ```
 
 The first two messages respectively state that the attacker learns the
diff --git a/proofs/authentication/protocol.pv b/proofs/authentication/protocol.pv
index 661666f..d7ed92b 100644
--- a/proofs/authentication/protocol.pv
+++ b/proofs/authentication/protocol.pv
@@ -31,15 +31,15 @@
     key and the public key of the dialer's and acceptor's blessings.
 
 (2) Channel Secrecy
-    A message sent from dialer to acceptor on the established
+    Any message sent from dialer to acceptor on the established
     encrypted channel is not revealed to the attacker.
 
 (3) Dialer Privacy
-    The dialer's public Key is never revealed to the attacker.
+    The dialer's public key is never revealed to the attacker.
 
 The acceptor reveals its blessing to any dialer that wants to talk to it,
-therefore the acceptor's public Key is not a secret. We verify that the
-acceptor's Public Key can be obtained by the attacker.
+therefore the acceptor's public key is not a secret. We verify that the
+acceptor's public key can be obtained by the attacker.
 ------------------------------------------------------------------------------*)
 
 set predicatesImplementable = nocheck.
@@ -96,7 +96,7 @@
 (* Type Conversion -----------------------------------------------------------*)
 fun keyToBitstring(SymmetricKey):bitstring [data].
 
-(* symmetricEncrypt(msg, key): Encrypt 'msg' using symmetric key 'key' *)
+(* symmetricEncrypt(msg, key): Authenticated encryption of 'msg' using symmetric key 'key' *)
 fun symmetricEncrypt(bitstring, SymmetricKey):bitstring.
 
 (* symmetricDecrypt(ciphertext, key): Decrypt 'ciphertext' using symmetric key 'key' *)
@@ -249,7 +249,7 @@
    ) then
    out(retCh, pubKey).
 
-(* dialHandshake process which takes as input the blessings and private key to
+(* Dialer process which takes as input the blessings and private key to
    be used during authentication, the expected public key of the acceptor
    (used for authorizing the acceptor's blessings). *)
 let dialHandshake(blessing:bitstring, privKey:bitstring, pubKeyExpected:bitstring) =
@@ -262,26 +262,23 @@
    new retCh2:channel;
    readRemoteAuth(aToDCh, key, remoteBnd, acceptorTag, retCh2) |
    in(retCh2, pubKeyAcceptor:bitstring);
-
-   (* Verify acceptor blessings and public key (peer authorization) *)
-   if (pubKeyAcceptor = pubKeyExpected) then
    event acceptsDialer(key, publicKeyBlessing(blessing), pubKeyAcceptor);
- 
+
    (* Send auth message *)
+   if (pubKeyAcceptor = pubKeyExpected) then
    let signedBinding = signedChannelBinding(privKey, dialerTag, localBnd) in
    out(dToACh, symmetricEncrypt(t(blessing, signedBinding), key));
 
-   (* Receive secret message. *)
-   in(aToDCh, secretMsg:bitstring);
-   let t(tag:bitstring, msg:bitstring) = symmetricDecrypt(secretMsg, key) in
+   (* Receive auth success confirmation. *)
+   in(aToDCh, msg:bitstring);
+   let t(tag:bitstring, pubKey:bitstring) = symmetricDecrypt(msg, key) in
    if tag = messageTag then
+   if pubKey = publicKeyBlessing(blessing) then
    event termDialer(key, publicKeyBlessing(blessing), pubKeyAcceptor).
 
 (* Acceptor process which takes as input the blessings and private key to
-   be used during authentication, and the expected public key of the
-   dialer (used for authorizing the dialer's blessings), , and a secret
-   message to be sent on the channel once authentication succeeds *)
-let acceptHandshake(blessing:bitstring, privKey:bitstring, pubKeyExpected:bitstring, secretMessage:bitstring) =
+   be used during authentication. *)
+let acceptHandshake(blessing:bitstring, privKey:bitstring) =
    (* Setup *)
    new retCh:channel;
    setup(aToDCh, dToACh, retCh) |
@@ -292,29 +289,24 @@
    let acceptorAuth = t(blessing, signedBinding) in
    out(aToDCh, symmetricEncrypt(acceptorAuth, key));
 
-   (* Receive auth mesage *)
+   (* Receive auth message *)
    new retCh2:channel;
    readRemoteAuth(dToACh, key, remoteBnd, dialerTag, retCh2) |
    in(retCh2, pubKeyDialer:bitstring);
-
-   (* Verify dialer blessings and public key (peer authorization) *)
-   if (pubKeyDialer = pubKeyExpected) then
    event acceptsAcceptor(key, pubKeyDialer, publicKeyBlessing(blessing));
 
-   (* Send secret message. *)
-   out(aToDCh, symmetricEncrypt(t(messageTag, secretMessage), key)).
+   (* Send auth success confirmation. *)
+   out(aToDCh, symmetricEncrypt(t(messageTag, pubKeyDialer), key)).
 
 (* Protocol Process *)
 let handshake(
     blessingDialer:bitstring,
     privKeyDialer:bitstring,
     blessingAcceptor:bitstring,
-    privKeyAcceptor:bitstring,
-    secretMessage:bitstring) =
-   let pubKeyDialer = publicKeyBlessing(blessingDialer) in
+    privKeyAcceptor:bitstring) =
    let pubKeyAcceptor = publicKeyBlessing(blessingAcceptor) in
    dialHandshake(blessingDialer, privKeyDialer, pubKeyAcceptor) |
-   acceptHandshake(blessingAcceptor, privKeyAcceptor, pubKeyDialer, secretMessage) .
+   acceptHandshake(blessingAcceptor, privKeyAcceptor) .
 
 (* Authentication Protocol Instance --------------------------------------------
    Instantiates the Vanadium authentication protocol for specific dialer and
@@ -324,30 +316,28 @@
 
 free privKeyDialer:bitstring [private].
 free privKeyAcceptor:bitstring [private].
-free secretMessage:bitstring [private].
 
 let handshakeInstance() =
     new rootPrivKey:bitstring;
     let rootBlessing = newSelfBlessing(rootPrivKey) in
     let blessingDialer = bless(publicKey(privKeyDialer), rootBlessing, rootPrivKey) in
     let blessingAcceptor = bless(publicKey(privKeyAcceptor), rootBlessing, rootPrivKey) in
-    handshake(blessingDialer, privKeyDialer, blessingAcceptor, privKeyAcceptor, secretMessage) .
+    handshake(blessingDialer, privKeyDialer, blessingAcceptor, privKeyAcceptor) .
 
 (* Authenticity *)
-query k:SymmetricKey, pkc:bitstring, pks:bitstring;
-   event(acceptsAcceptor(k, pkc, pks)) ==> event(acceptsDialer(k, pkc, pks)).
-   (* Desired ProVerif output: event(acceptsAcceptor(k,pkc,pks)) ==> event(acceptsDialer(k,pkc,pks)) is true *)
-query k:SymmetricKey, pkc:bitstring, pks:bitstring;
-   event(termDialer(k, pkc, pks)) ==> event(acceptsAcceptor(k, pkc, pks)).
-   (* Desired ProVerif output: event(termDialer(k,pkc,pks)) ==> event(acceptsAcceptor(k,pkc,pks)) is true *)
+query k:SymmetricKey;
+   event(acceptsAcceptor(k, publicKey(privKeyDialer), publicKey(privKeyAcceptor))) ==> event(acceptsDialer(k, publicKey(privKeyDialer), publicKey(privKeyAcceptor))).
+   (* Desired ProVerif output: event(acceptsAcceptor(k,publicKey(privKeyDialer[]),publicKey(privKeyAcceptor[]))) ==> event(acceptsDialer(k,publicKey(privKeyDialer[]),publicKey(privKeyAcceptor[]))) is true *)
+query k:SymmetricKey;
+   event(termDialer(k, publicKey(privKeyDialer), publicKey(privKeyAcceptor))) ==> event(acceptsAcceptor(k, publicKey(privKeyDialer), publicKey(privKeyAcceptor))).
+   (* Desired ProVerif output: event(termDialer(k,publicKey(privKeyDialer[]),publicKey(privKeyAcceptor[]))) ==> event(acceptsAcceptor(k,publicKey(privKeyDialer[]),publicKey(privKeyAcceptor[]))) is true *)
 
-(* Channel Secrecy *)
-query attacker(secretMessage).  (* Desired ProVerif output: not attacker(secretMessage) is true *)
+(* Channel Secrecy and Dialer Privacy*)
 query attacker(privKeyDialer).  (* Desired ProVerif output: not attacker(privKeyDialer) is true *)
 query attacker(privKeyAcceptor).  (* Desired ProVerif output: not attacker(privKeyAcceptor) is true *)
-
-(* Dialer Privacy *)
 query attacker(publicKey(privKeyDialer)).  (* Desired ProVerif output: not attacker(publicKey(privKeyDialer)) is true *)
-query attacker(publicKey(privKeyAcceptor)).  (* Desired ProVerif output: not attacker(publicKey(privKeyAcceptor)) is true *)
+
+(* Lack of Acceptor Privacy *)
+query attacker(publicKey(privKeyAcceptor)).  (* Desired ProVerif output: not attacker(publicKey(privKeyAcceptor)) is false *)
 
 process handshakeInstance()
\ No newline at end of file